On The Metric Nature of (Differential) Logical Relations

TL;DR

This paper investigates the metric properties of differential logical relations, revealing their connections to quasi-metrics and partial metrics, and introduces new compositional reasoning principles for program differences.

Contribution

It clarifies the metric nature of differential logical relations, relating them to quasi-metrics and partial metrics, and derives new reasoning principles for program differences.

Findings

Differential logical relations do not generally form metric spaces.

Distance functions from these relations can be related to quasi-metrics and partial metrics.

New compositional reasoning principles for program differences are established.

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.