On the Metric Nature of (Differential) Logical Relations

TL;DR

This paper explores the metric properties of differential logical relations, introducing quasi-quasi-metrics and their categorical structure to better understand program distances and their compositional reasoning.

Contribution

It clarifies the metric nature of differential logical relations, introduces quasi-quasi-metrics, and develops a framework for differential prelogical relations as a quantitative extension.

Findings

Quasi-quasi-metrics reflect differential logical relations categorically.

Type interpretations satisfy strong transitivity and indistancy conditions.

The poset of differential prelogical relations has no coarsest element.

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.