Skip to Main content Skip to Navigation
Conference papers

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

Abstract : 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 differen-tiability 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 λ-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 con-ditionals, and prove the soundness of the type system using open logical relations.
Document type :
Conference papers
Complete list of metadatas

Cited literature [59 references]  Display  Hide  Download

https://hal.inria.fr/hal-02991652
Contributor : Francesco Gavazzo <>
Submitted on : Friday, November 6, 2020 - 9:55:22 AM
Last modification on : Saturday, November 7, 2020 - 3:35:51 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02991652, version 1

Collections

Citation

Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo. On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem. Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Apr 2020, Dublin, Ireland. ⟨hal-02991652⟩

Share

Metrics

Record views

6

Files downloads

37