Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Metric Nature of (Differential) Logical Relations

Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone

TL;DR

The quasi-quasi-metric spaces arising from the interpretation of types are investigated, and it is proved that they satisfy variants of the strong transitivity condition and indistancy condition, as well as a weak form of the symmetry condition.

Abstract

Differential logical relations are methods to measure distances between higher-order programs where distances between functional programs are themselves \emph{functions}, relating errors in inputs with errors in outputs. This way, differential logical relations provide a more fine-grained and contextual information of program distances. This paper aims to clarify the metric nature of differential logical relations. We introduce the notion of quasi-quasi-metrics and observe that the cartesian closed category of quasi-quasi-metric spaces reflects the construction of differential logical relations in the literature. The cartesian closed structure induces a fundamental lemma, which can be seen as a compositional reasoning principle for program distances. Furthermore, we investigate the quasi-quasi-metric spaces arising from the interpretation of types, and we prove that they satisfy variants of the strong transitivity condition and indistancy condition, as well as a weak form of the symmetry condition. In the last part of this paper, we introduce a notion of differential prelogical relations arising as a quantitative counterpart of the framework of prelogical relations. Roughly speaking, differential prelogical relations are quasi-quasi-metrics on the collection of programs. The poset of differential prelogical relations has the finest differential prelogical relation presented as a formal quantitative equational theory, while the poset lacks a coarsest differential prelogical relation. The absence of a coarsest differential prelogical relation contrasts with the situations of typed lambda calculi, where the contextual equivalences serve as the coarsest program equivalences.

On the Metric Nature of (Differential) Logical Relations

TL;DR

The quasi-quasi-metric spaces arising from the interpretation of types are investigated, and it is proved that they satisfy variants of the strong transitivity condition and indistancy condition, as well as a weak form of the symmetry condition.

Abstract

Differential logical relations are methods to measure distances between higher-order programs where distances between functional programs are themselves \emph{functions}, relating errors in inputs with errors in outputs. This way, differential logical relations provide a more fine-grained and contextual information of program distances. This paper aims to clarify the metric nature of differential logical relations. We introduce the notion of quasi-quasi-metrics and observe that the cartesian closed category of quasi-quasi-metric spaces reflects the construction of differential logical relations in the literature. The cartesian closed structure induces a fundamental lemma, which can be seen as a compositional reasoning principle for program distances. Furthermore, we investigate the quasi-quasi-metric spaces arising from the interpretation of types, and we prove that they satisfy variants of the strong transitivity condition and indistancy condition, as well as a weak form of the symmetry condition. In the last part of this paper, we introduce a notion of differential prelogical relations arising as a quantitative counterpart of the framework of prelogical relations. Roughly speaking, differential prelogical relations are quasi-quasi-metrics on the collection of programs. The poset of differential prelogical relations has the finest differential prelogical relation presented as a formal quantitative equational theory, while the poset lacks a coarsest differential prelogical relation. The absence of a coarsest differential prelogical relation contrasts with the situations of typed lambda calculi, where the contextual equivalences serve as the coarsest program equivalences.
Paper Structure (29 sections, 20 theorems, 122 equations, 5 figures)

This paper contains 29 sections, 20 theorems, 122 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Outline of this Paper
  3. From Logical Relations to Differential Logical Relations
  4. Logical Relations
  5. Differential Logical Relations
  6. Weakening the Reflexivity Condition
  7. Quasi-Quasi-Metric
  8. Quantale and the Definition of Quasi-Quasi-Metric
  9. Quantale-Valued Relations
  10. Quasi-Metrics and Partial Quasi-Metrics
  11. Remarks on Transitivity Conditions
  12. The Category of Quasi-Quasi-Metric Spaces
  13. Cartesian Closed Structure
  14. Quasi-Quasi-Metric Semantics
  15. Target Calculus
  16. ...and 14 more sections

Key Result

Proposition 3.9

Let $r \subseteq X \times Q \times X$ be a closed $Q$-predicate. For any $x,y \in X$ and $a \in Q$, Furthermore, $\check{(-)}$ and $\hat{(-)}$ form a bijection between the set of $Q$-relations over $X$, and the set of closed $Q$-predicates over $X$.

Figures (5)

  • Figure 1: The Idea of Differential Logical Relations at Function Types
  • Figure 2: Typing Rules
  • Figure 3: Set Theoretic Interpretation
  • Figure 4: The Definition of Derivatives
  • Figure 5: Derivation Rules

Theorems & Definitions (62)

  • Remark 2.1
  • Definition 3.1
  • Example 3.2
  • Example 3.3
  • Definition 3.4
  • Definition 3.5
  • Example 3.6
  • Definition 3.7
  • Definition 3.8
  • Proposition 3.9
  • ...and 52 more