On The Metric Nature of (Differential) Logical Relations
Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone
TL;DR
The paper addresses the challenge of comparing higher-order programs with a metric that captures how input errors map to output errors. It introduces quasi^2-metrics as a bridge between quasi-metrics and partial metrics, and shows how such distances give rise to two observational quasi-metrics and relate to partial quasi-metrics, enabling compositional reasoning about program differences. It also relates these metric notions to a deductive system and to a syntactic presentation of differential logical relations, culminating in two conjectures about comparing the introduced notions. The work advances the theory of quantale-valued metrics for higher-order languages, providing new principled tools for reasoning about program differences and a framework for combining relational and metric perspectives.
Abstract
Differential logical relations are a method to measure distances between higher-order programs. They differ from standard methods based on program metrics in that differences between functional programs are themselves functions, relating errors in input with errors in output, this way providing a more fine grained, contextual, information. The aim of this paper is to clarify the metric nature of differential logical relations. While previous work has shown that these do not give rise, in general, to (quasi-)metric spaces nor to partial metric spaces, we show that the distance functions arising from such relations, that we call quasi-quasi-metrics, can be related to both quasi-metrics and partial metrics, the latter being also captured by suitable relational definitions. Moreover, we exploit such connections to deduce some new compositional reasoning principles for program differences.