Cargando…

On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem

Logical relations are one among the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance...

Descripción completa

Detalles Bibliográficos
Autores principales: Barthe, Gilles, Crubillé, Raphaëlle, Lago, Ugo Dal, Gavazzo, Francesco
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7702265/
http://dx.doi.org/10.1007/978-3-030-44914-8_3
_version_ 1783616580049960960
author Barthe, Gilles
Crubillé, Raphaëlle
Lago, Ugo Dal
Gavazzo, Francesco
author_facet Barthe, Gilles
Crubillé, Raphaëlle
Lago, Ugo Dal
Gavazzo, Francesco
author_sort Barthe, Gilles
collection PubMed
description Logical relations are one among the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we study a generalization of the concept of a logical relation, called open logical relation, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed [Formula: see text] -calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any collection of real-valued first-order functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations.
format Online
Article
Text
id pubmed-7702265
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-77022652020-12-01 On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem Barthe, Gilles Crubillé, Raphaëlle Lago, Ugo Dal Gavazzo, Francesco Programming Languages and Systems Article Logical relations are one among the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we study a generalization of the concept of a logical relation, called open logical relation, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed [Formula: see text] -calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any collection of real-valued first-order functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations. 2020-04-18 /pmc/articles/PMC7702265/ http://dx.doi.org/10.1007/978-3-030-44914-8_3 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Barthe, Gilles
Crubillé, Raphaëlle
Lago, Ugo Dal
Gavazzo, Francesco
On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
title On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
title_full On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
title_fullStr On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
title_full_unstemmed On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
title_short On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
title_sort on the versatility of open logical relations: continuity, automatic differentiation, and a containment theorem
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7702265/
http://dx.doi.org/10.1007/978-3-030-44914-8_3
work_keys_str_mv AT barthegilles ontheversatilityofopenlogicalrelationscontinuityautomaticdifferentiationandacontainmenttheorem
AT crubilleraphaelle ontheversatilityofopenlogicalrelationscontinuityautomaticdifferentiationandacontainmenttheorem
AT lagougodal ontheversatilityofopenlogicalrelationscontinuityautomaticdifferentiationandacontainmenttheorem
AT gavazzofrancesco ontheversatilityofopenlogicalrelationscontinuityautomaticdifferentiationandacontainmenttheorem