# On the Metric Nature of (Differential) Logical Relations

Ugo Dal Lago ☐

University of Bologna, Italy
INRIA Sophia Antipolis, France

Naohiko Hoshino ☐

Sojo University, Kumamoto, Japan

Paolo Pistone ☐

Université Claude Bernard Lyon 1, France

## 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.

**2012 ACM Subject Classification** Theory of computation → Program semantics; Theory of computation → Equational logic and rewriting

**Keywords and phrases** Differential Logical Relations, Quantales, Quasi-Metrics, Partial Metrics

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2025.15

## 1 Introduction

Program equivalence is a crucial concept in program semantics, and ensures that different implementations of a program produce *exactly* the same results under the same conditions, i.e., in any environment. This concept is fundamental in program verification, code optimization, and for enabling reliable refactoring: by proving that two programs are equivalent, developers and compiler designers can confidently replace one with the other, knowing that the behavior and outcomes will remain consistent. In this respect, guaranteeing that the underlying notion of program equality is a *congruence* is of paramount importance.

In the research communities mentioned above, however, it is known that comparing programs through a notion of equivalence without providing the possibility of measuring the *distance* between non-equivalent programs makes it impossible to validate many interesting and useful program transformations [28]. All this has generated interest around the concepts of program metrics and more generally around the study of techniques through which to quantitatively compare non-equivalent programs, so as, e.g., to validate those program transformations which do not introduce too much of an error [31, 27].

What corresponds, in a quantitative context, to the concept of congruence? Once differences are measured by some (pseudo-)metric, a natural answer to this question is to require that any language construct does not increase distances, that is, that they are *non-expansive*. Along with this, the standard properties of (pseudo-)metrics, like the triangle

<figure><img src="image_1.png" /></figure>

© Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone;
licensed under Creative Commons License CC-BY 4.0

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025).

Editor: Maribel Fernández; Article No. 15; pp. 15:1–15:22

<figure><img src="image_2.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
15:2 On the Metric Nature of (Differential) Logical Relations

inequality $d(x, z) + d(z, y) \geq d(x, y)$, provide general principles that are very useful in metric reasoning, replacing standard qualitative principles (e.g., in this case, transitivity $\eqqeqg\eqqeq$) and quantitative principles (e.g., in this case, inequality $d(x, z) \wedge d(z, y) \vdash d(x, y)$).

Still, as already observed in many occasions [11, 9], the restriction to language constructs that are non-expansive with respect to some purely numerical metric turns out too severe in practice. On the one hand, the literature focusing on higher-order languages has mostly restricted its attention to linear or graded languages [31, 2], due to well-known difficulties in constructing metric models for full “simply-typed” languages [12]. On the other hand, even if one restricts to a linear language, the usual metrics defined over functional types are hardly useful in practice, as they assign distances to functions $f, g$ via a comparison of their values in the worst case: for instance, as shown in [11], the two maps $\lambda x.x, \lambda x.\sin(x) : \mathbf{Real} \to \mathbf{Real}$, although behaving very closely around 0, are typically assigned the distance $\infty$, since their values grow arbitrarily far from each other in the worst case.

The differential logical relations [11, 9, 29, 10] have been introduced as a solution to the aforementioned problems. In this setting, which natively works for unrestricted higher-order languages, the distance between two programs is not necessarily given as a single number: for instance, two programs of functional type are far apart according to a function itself, which measures how the error in the output depends on the error in the input, but also on the value of the input itself. This way the notion of distance becomes sufficiently expressive, at the same time guaranteeing the possibility of compositional reasoning. This paradigm also scales to languages with duplication, recursion [9] and works even in presence of effects [10].

In the literature on program metrics, it has become common to consider metrics valued on arbitrary *quantales* [22, 36]. This means that, as for the differential logical relations, the distance between two points needs not be a non-negative real, but can belong to any suitable algebra of “quantities”. This has led to the study of different classes of quantale-valued metrics, each characterized by a particular formulation of the triangular law. Among this, *quasi-metrics* [19] and *partial metrics* [4, 23] have been explored for the study of domains, even for higher-order languages [17, 26]. While the first obey the usual triangular inequality, or transitivity, the second obey a stronger transitivity condition, also taking into account the replacement of standard reflexivity $d(x, x) = 0$ by a weaker *quasi-reflexivity* condition $d(x, x) \le d(x, y)$, implying that a point need not be at distance zero from itself.

A natural question is thus: do the distances between programs that are obtained via differential logical relations constitute some form of (quantale-valued) metric? In particular, what forms do transitivity and reflexivity do these relations support? The original paper [11] defined symmetric differential logical relations and gave a very weak form of triangle inequality. Subsequent works, relating to the more natural asymmetric case, have either ignored the metric question [9, 10] or shown that the distances produced must violate both the reflexivity of quasi-metric and the strong transitivity of partial metrics [17, 29].

This paper aims at providing a bridge between current methods for higher-order program differences and the well-established literature on quantale-valued metrics. More specifically, we show that the distances produced by differential logical relations, that we call *quasi-quasi-metrics* (or *qq-metric*), satisfy the *quasi-reflexivity* of partial metrics and the standard transitivity of quasi-metrics. Such metrics thus sit somehow *in between* quasi-metrics and partial metrics. We will establish precise connections between all those. We also exploit these results to deduce some new principles of compositional reasoning about program differences arising from the different forms of transitivity at play. Finally, we introduce a deductive system, inspired from the quantitative equational theories of Mardare et al. [27], to derive upper bounds on differences between programs.
**Contributions.** Our contributions can be summarized as follows:

- We introduce a new class of quantale-valued metrics, called qq-metrics. We show that each such metric gives rise to two observational quasi-metrics over programs, and can be seen as a relaxation of partial quasi-metrics [24]. This is in Section 3;

- we establish the equivalence of the cartesian closed structure of qq-metrics with the standard definition of differential logical relations. We also show that observational quasi-metrics as well as partial quasi-metrics can be captured by suitable families of logical relations. We exploit all such definitions to deduce some new compositional reasoning principles for program differences. This spans through Sections 4-7;

- finally, we introduce an equational theory for program differences via a syntactic presentation of differential logical relations and we formulate two conjectures about the comparison of the different notions of program distances introduced. This is in Sections 8 and 9.

We give proof details in appendices.

## 2 From Logical Relations to Differential Logical Relations

In this section we recall how differential logical relations can be seen as a quantitative generalization of standard logical relations, at the same time highlighting the metric counterparts of qualitative notions like equivalences and preorders. Moreover, we introduce quasi-quasi-metrics as the metric counterpart of quasi-reflexive and transitive relations. For simplicity, we identify lambda terms using the standard $\beta$-equalities throughout this section.

**Logical Relations.** The theory of logical relations is well-known and has been exploited in various directions to establish qualitative properties of type systems, like e.g. termination [18], bisimulation [33] or parametricity [30, 21]. The idea is to start from some basic binary relation $\rho_o \subseteq o \times o$ over the terms of some ground type $o$. The relation $\rho_o$ can then be *lifted* to a family of binary relations $\rho_A \subseteq A \times A$, where $A$ varies over all simple types constructed starting from $o$ (indeed, one may consider recursive [14], polymorphic [32, 30] or monadic [20] types as well, but we here limit our discussion to simple types). The lifting is defined inductively by:

$$ (t, t') \in \rho_{A \times B} \iff (fst(t), fst(t')) \in \rho_A \text{ and } (snd(t), snd(t')) \in \rho_B, \quad (\wedge) $$

$$ (t, t') \in \rho_{A \to B} \iff (\forall s, s' \in A) (s, s') \in \rho_A \Rightarrow (ts, t's') \in \rho_B. \quad (\Rightarrow) $$

Typically, one wishes to establish a so-called *fundamental lemma*, stating that well-typed programs $x : A \vdash t : B$ *preserve relations*. This means that, for any choice of a family of logical relations $\rho_A$ defined as above, one can prove

$$ (\forall s, s' \in A) (s, s') \in \rho_A \Rightarrow (t[s/x], t[s'/x]) \in \rho_B. \quad (\text{Fundamental Lemma}) $$

Notice that this is equivalent to the instance of *reflexivity* $(\lambda x.t, \lambda x.t) \in \rho_{A \to B}$.

Of particular interest are the *equivalence relations* (that is, those which are reflexive, symmetric and transitive) and the *preorders* (that is, the reflexive and transitive ones). We here focus on the latter, as we will not consider symmetry in this paper (see Remark 3). A fundamental observation is that the logical relation lifting preserves preorders (and indeed, equivalences): if $\rho_A$ and $\rho_B$ are reflexive and transitive, then $\rho_{A \times B}$ and $\rho_{A \to B}$ can be shown reflexive and transitive as well. The case of the function space crucially relies on the fact that all programs of type $A \Rightarrow B$ must preserve relations (or, in other words, that the fundamental lemma holds): as we observed above, the *reflexivity condition* $(t, t) \in \rho_{A \to B}$ coincides with the fact that the function $t$ is relation-preserving; transitivity, instead, can be proved by combining relation-preservation, the *reflexivity* of $\rho_A$ and the *transitivity* of $\rho_B$.
15:4 On the Metric Nature of (Differential) Logical Relations

Any logical relation $\rho \subseteq A \times A$ induces an equivalence $\equiv_\rho$, called the *observational equivalence*, where $t \equiv_\rho u$ iff for all $s \in A$, $(s, t) \in \rho$ iff $(s, u) \in \rho$. Intuitively, two terms $t, u$ are equivalent if the relation $\rho$ cannot distinguish them. For example, if the definition of $\rho_o$ on basic types only depends on the values $t \Rightarrow^* v$ produced by terms, one can usually deduce that terms are indistinguishable from their associated values, that is $t \equiv_\rho v$. In the absence of symmetry, one obtains two *observational preorders* $\sqsubseteq_\rho^l, \sqsubseteq_\rho^r \subseteq A \times A$ defined by:

$$s \sqsubseteq_{\rho}^{l} t \iff (\forall u \in A) (t, u) \in \rho \Rightarrow (s, u) \in \rho,$$

$$s \sqsubseteq_{\rho}^{r} t \iff (\forall u \in A) (u, s) \in \rho \Rightarrow (u, t) \in \rho.$$

These preorders satisfy the following useful and easily provable properties:

**Proposition 1.** For any binary relation $\rho \subseteq A \times A$ and $c \in \{l, r\}$,

(i.) $\sqsubseteq_\rho^c \supseteq \rho$ iff $\rho$ is transitive;

(ii.) $\sqsubseteq_\rho^c \subseteq \rho$ iff $\rho$ is reflexive;

(iii.) $\sqsubseteq_\rho^c = \rho$ iff $\rho$ is a preorder;

(iv.) The following hold:

$$(\forall s, t, u \in A) s \sqsubseteq_{\rho}^{l} t \wedge (t, u) \in \rho \Rightarrow (s, u) \in \rho, \quad \text{(left transitivity)}$$

$$(\forall s, t, u \in A) (s, t) \in \rho \wedge t \sqsubseteq_{\rho}^{r} u \Rightarrow (s, u) \in \rho. \quad \text{(right transitivity)}$$

The reason why we delve into these basic properties of preorders is that we will soon explore their (less trivial!) quantitative counterparts, that arise naturally in the theory of differential logical relations. In particular, the left and right transitivity conditions will correspond to stronger variants of the triangular inequality for metric spaces.

Beyond preorders, we are interested in the following weaker notion:

**Definition 2 (Quasi-Preorder).** A relation $\leq \subseteq A \times A$ is called a quasi-preorder if it is transitive and (left-)quasi-reflexive, that is, $t \leq u \Rightarrow t \leq t$.

Quasi-preorders are obtained by weakening the reflexivity condition of preorders: intuitively, only the points which are smaller than someone are smaller than themselves. One can easily develop a theory of logical relations for quasi-preorders. The sole delicate point is that, in order to let such relations lift to function spaces, one has to slightly modify the relation lifting as follows:

$$(t, t') \in \rho_{A \Rightarrow B} \iff (\forall s, s' \in A) (s, s') \in \rho_A \Rightarrow (ts, t's') \in \rho_B \wedge (ts, t's') \in \rho_B. \quad (\Rightarrow^q)$$

Compared to $(\Rightarrow)$, $(\Rightarrow^q)$ includes a second clause $(ts, t's') \in \rho_B$ relating the action of $t$ on both $s$ and $s'$. With this definition, one can easily check that if $\rho_A, \rho_B$ are quasi-preorders, and the fundamental lemma holds, then $\rho_{A \times B}$ and $\rho_{A \Rightarrow B}$ are quasi-preorders as well.

**Differential Logical Relations.** We now have all elements to discuss what happens when extending logical relations to a quantitative setting. Rather than considering binary relations $\rho \subseteq A \times A$ expressing that a certain property holds for two terms $s, t$ or not, we will consider ternary relations $\rho \subseteq A \times Q_A \times A$, where $(s, a, t) \in \rho$ indicates that a certain relation holds of $s, t$ to a certain extent, quantified via $a \in Q_A$. Here $Q_A$ is a quantale, an algebraic structure (recalled in the next section) that captures several properties of quantities as expressed by e.g. non-negative real numbers.

In fact, just like for standard logical relations, a differential logical relation $\rho_o \subseteq o \times Q_o \times o$ on a ground type can be *lifted* to a family of binary relations $\rho_A \subseteq A \times Q_A \times A$ over simple types. First, we define, by induction, the quantales $Q_{A \times B} = Q_A \times Q_B$ and $Q_{A \Rightarrow B} = A \Rightarrow (Q_A \Rightarrow Q_B)$,
where $Q_A \to Q_B$ is the quantale of monotone functions, and $A \Rightarrow Q_A \to Q_B$ is the quantale of functions from the set of closed terms of type A to $Q_A \to Q_B$ equipped with the pointwise order. We then define the lifting of $\rho_o$ by:

$$((t, u), (a, b), (t', u')) \in \rho_{A \times B} \iff (t, a, t') \in \rho_A \text{ and } (u, b, u') \in \rho_A,$$ 
$$ (t, f, t') \in \rho_{A \to B} \iff (\forall s, s' \in A, \forall a \in Q_A) \text{ if } (s, a, s') \in \rho_A, \text{ then} $$ 
$$ (ts, f(s)(a), ts') \in \rho_B \text{ and } (ts, f(s)(a), t's') \in \rho_B.$$

Notice that the definition of $\rho_{A \to B}$ closely imitates the clause ($\Rightarrow^q$) for quasi-preorders. Also observe that the quantale $Q_{A \to B}$ for the function type is itself a set of functions relating terms of type A and quantities in $Q_A$ with quantities in $Q_B$. As we show in Section 5, this definition gives rise to an interpretation of the simply typed $\lambda$-calculus where a fundamental lemma holds under the following form: for all terms $x : A \vdash t : B$ and choice of a family of differential logical relations $\rho_A$ as above, there exists a map $t^\bullet : A \Rightarrow (Q_A \to Q_B)$ such that

$$(\forall s, s' \in A, \forall a \in Q_A) (s, a, s') \in \rho_A \Rightarrow (ts, t^\bullet(s)(a), ts') \in \rho_B. \quad (\text{fundamental lemma})$$

The function $t^\bullet$ behaves like some sort of *derivative* of $t$: it relates errors in input with errors in output. This connection is investigated in more detail in [9, 29].

So far, everything works just as in the standard, qualitative, case. However, the quantitative setting is well visible when we consider the corresponding notions of equivalences and preorders. Recall that an (integral) quantale is, in particular, an ordered monoid $(Q, +, 0, \leq)$ of which $0$ is the minimum element. For a differential logical relation $\rho \subseteq A \times Q_A \times A$, convexity, symmetry and transitivity translate into the following conditions:

$$(\forall t \in A) (t, 0, t) \in \rho, \qquad (\text{reflexivity})$$

$$(\forall t, u \in A, \forall a \in Q_A) (t, a, u) \in \rho \Rightarrow (u, a, t) \in \rho, \qquad (\text{symmetry})$$

$$(\forall s, t, u \in A, \forall a, b \in Q_A) (s, a, t) \in \rho \wedge (t, b, u) \in \rho \Rightarrow (s, a + b, u) \in \rho. \qquad (\text{transitivity})$$

It is clear then that equivalence relations translate, in the quantitative setting, into some kind of metric space. Similarly, the quantitative counterpart of preorders are the so-called *quasi-metric spaces* [19], essentially, metrics without a symmetry condition, indeed a very well-studied class of metrics. In particular, we will show that, similarly to preorders, any ternary relation $\rho \subseteq A \times Q_A \times A$ gives rise to left and right *observational quasi-metrics* $\rho^l, \rho^r : A \times A \to Q_A$ satisfying properties analogous to those of Proposition 1.

**Remark 3.** While in the original definition [11] differential logical relations were symmetric, symmetry was abandoned in all subsequent works. The first reason is that several interesting notions of program difference, like e.g. those arising from *incremental computing* [9, 6, 1], are not symmetric. A second reason is that the cartesian closure is problematic in presence of both quasi-reflexivity and symmetry [29].

There is, however, an important point on which differential logical relations differ from standard logical relations: while the former lift preorders well to all simple types, their quantitative counterpart, the quasi-metrics, are *not* preserved by the higher-order lifting of differential logical relations. Indeed, we observed that an essential ingredient in the lifting of the convexity property is the fundamental lemma; yet, in the framework of differential logical relations, the fundamental lemma produces, for any term $t : A \Rightarrow B$, the “reflexivity” condition $(t, t^\bullet, t) \in \rho_{A \to B}$, which differs from standard convexity in that the distance is $t^\bullet$ and *not* the minimum element $0$. This means that the metric structure arising from differential logical relation cannot be that of standard (quasi-)metric spaces. Rather, it must
15:6 On the Metric Nature of (Differential) Logical Relations

be something close to the *partial* metric spaces [4, 23], that is, metric spaces in which the condition $d(x, x) = 0$ is replaced by the quasi-reflexivity condition $d(x, x) \le d(x, y)$. We will discuss the connections with partial metric spaces in the next sections.

By replacing reflexivity with quasi-reflexivity, we obtain the quantitative counterpart of quasi-preorders, that we call *qq-metrics* (being “quasi” both in the sense of quasi-metrics, i.e. the rejection of symmetry, and of quasi-preorders, i.e. the weakening of convexity).

**Definition 4.** For a set $X$ and a quantale $Q$, a relation $\rho \subseteq X \times Q \times X$ is called quasi-quasi-metric (or more concisely qq-metric) if it is transitive and satisfies the condition

$$ (\forall x, y \in X, \forall a \in Q) (x, a, y) \in \rho \Rightarrow (x, a, x) \in \rho. \qquad (\text{quasi-reflexivity}) $$

As shown in Section 4, the qq-metrics capture the properties of distances which are preserved by differential logical relations: indeed, the argument showing that the quasi-preorders lift to all simple types scales well to the quantitative setting, showing that a qq-metric on the base types gives rise to qq-metrics on all simple types.

The obvious question, however, is: what are these qq-metrics? How are they related to the more standard quasi-metrics and partial metrics? This is what we are going to do in the following section.

3 Quasi-Quasi-Metric Spaces

In this section we use the language of quantale-valued relations to explore the connections between the qq-metrics introduced in the previous section and the more well-established notions of quasi-metric and partial quasi-metric spaces.

**Quantale-Valued Relations.** Let us recall that a quantale $Q$ is a complete lattice $(Q, \sqsubseteq)$ endowed with a continuous monoidal operation $\otimes$, with unit 1. Here, $\otimes$ being continuous means that both $x \otimes (-)$ and $(-) \otimes x$ preserve arbitrary suprema for all $x \in Q$. A quantale $Q$ is integral (cf. [22], p. 148) when $1 = \top$ and commutative when $\otimes$ is commutative. Suppose $Q$ is commutative. Given $x, y \in Q$, their *residual* is defined as $x \to y := \bigvee \{z \in Q \mid z \otimes x \sqsubseteq y\}$ where $\sqsubseteq$ is the partial order of $Q$. Notice that $z \sqsubseteq x \to y$ iff $z \otimes x \sqsubseteq y$, and that $(x \to y) \otimes x \sqsubseteq y \sqsubseteq x \to (y \otimes x)$. A commutative quantale $Q$ is divisible [23] if for all $x, y \in Q$, $x \sqsubseteq y$ holds iff $y \otimes (y \to x) = x$. Equivalently, $Q$ is divisible iff, whenever $x \sqsubseteq y$, there exists $z$ such that $x = y \otimes z$. In the following we will use $Q$ to refer to a commutative, integral and divisible quantale.

**Example 5.** The *Lawvere quantale* is formed by the non-negative extended reals $[0, +\infty]$ with the *reversed* order $x \sqsubseteq y := x \ge y$, and with addition as monoidal operation. Notice that the ordering of quantales is *reversed* with respect to usual metric intuitions: the “0” element is the $\top$, joins correspond to taking infs, etc.

Given a quantale $Q$ and sets $X, Y$, a $Q$-relation over $X, Y$ is a map $s: X \times Y \to Q$, which can be visualized as a matrix with values in $Q$. For $Q$-relations $s, t: X \times Y \to Q$, we write $s \sqsubseteq t$ when $s(x, y) \sqsubseteq t(x, y)$ for all $x \in X$ and $y \in Y$. Given $Q$-relations $s: X \times Y \to Q$, $t: Y \times Z \to Q$ and $u: X \times Z \to Q$, $w: Z \times Y \to Q$, we define the $Q$-relations $s \otimes t: X \times Z \to Q$ and $u \otimes w: Z \times Y \to Q$ and $s \otimes u: X \times Z \to Q$ via the two operations:

$$ (s \otimes t)(x, z) = \bigvee_{y \in Y} s(x, y) \otimes t(y, z), $$

$$ (u \to s)(z, y) = \bigwedge_{x \in X} u(x, z) \to s(x, y), \qquad (s \to w)(x, z) = \bigwedge_{y \in Y} w(z, y) \to s(x, y). $$
The monoidal product $\otimes$ and the residuals $\ominus, \oplus$ of $\mathcal{Q}$-relations satisfy properties analogous to residuals in $\mathcal{Q}$, e.g. $s \otimes (s \ominus t) \subseteq t$, $(t \ominus s) \otimes s \subseteq t$. It is well-known that $\mathcal{Q}$-relations form a category $\mathcal{QRel}$ whose objects are sets and such that $\mathcal{QRel}(X, Y)$ are the $\mathcal{Q}$-relations from $X$ to $Y$. The operation $s \otimes t$ is the composition operator of this category, while the identities are the relations defined as $\mathbf{1}_X(x, x) = 1 = \top$ and $\mathbf{1}_X(x, y \neq x) = \bot$.

Finally, for any relation $s \in \mathcal{QRel}(X, X)$, define the relations $\Delta_1 s, \Delta_2 s \in \mathcal{QRel}(X, X)$ by $\Delta_1 s = s \circ \Delta \circ \pi_1$ and $\Delta_2 s = s \circ \Delta \circ \pi_2$, that is, $\Delta_1 s(x, y) := s(x, x)$, $\Delta_2 s(x, y) = s(y, y)$.

**Qq- and Quasi-Metric Spaces.** For a relation $s \in \mathcal{QRel}(X, X)$, reflexivity $s(x, x) = 1$ and transitivity $s(x, z) \otimes s(z, y) \subseteq s(x, y)$ can be written more concisely as $s \supseteq \mathbf{1}_X$ and $s \otimes s \subseteq s$. A relation $s$ satisfying both such properties is called a quasi-(pseudo)metric (or a hemi-metric) over $X$ (with values in $\mathcal{Q}$). The “pseudo” prefix stands for the fact that the usual separation property $s(x, y) = 1 \Rightarrow x = y$ needs not hold. As we do not investigate separation here, all metric notions discussed in the rest of the paper are to be understood as implicitly “pseudo”.

The following construction generalizes the observational preorders to $\mathcal{Q}$-relations:

**Proposition 6.** For all $s \in \mathcal{QRel}(X, X)$, the relations $s^l := s \ominus s, s^r := s \oplus s \in \mathcal{QRel}(X, X)$ are quasi-metrics and, for $c \in \{l, r\}$, the following hold:

(i.) $s^c \supseteq s$ iff $s$ is transitive;

(ii.) $s^c \subseteq s$ iff $s$ is reflexive;

(iii.) $s^c = s$ iff $s$ is a quasi-metric;

(iv.) $s^l \otimes s \subseteq s$ and $s \otimes s^r \subseteq s$, that is, the following hold:

$$ (\forall x, y, z \in X) \quad s^l(x, z) \otimes s(z, y) \subseteq s(x, y), \qquad \text{(left transitivity)} $$

$$ (\forall x, y, z \in X) \quad s(x, z) \otimes s^r(z, y) \subseteq s(x, y). \qquad \text{(right transitivity)} $$

We call the quasi-metrics $s^l, s^r$ the left and right observational quasi-metric of $s$.

Qq-metrics correspond to $\mathcal{Q}$-relations $s \in \mathcal{QRel}(X, X)$ satisfying transitivity $s \otimes s \subseteq s$ and quasi-reflexivity $s \subseteq \Delta_1 s$ (i.e. $s(x, y) \subseteq s(x, x)$). From transitivity, we deduce that, for a qq-metric $s$, both $s^l, s^r \supseteq s$ hold, that is, the observational quasi-metrics yield tighter distances than $s$. This implies that left and right transitivity read as stronger forms of the triangular inequality. In particular, the following alternative characterization of qq-metrics holds:

**Proposition 7.** For any quasi-reflexive $s \in \mathcal{QRel}(X, X)$, $s$ is a qq-metric iff there exists a quasi-metric $q \supseteq s$ such that either $s \otimes q \subseteq s$ or $q \otimes s \subseteq s$ holds. Furthermore, when $s$ is a qq-metric, both $s^l$ and $s^r$ are quasi-metrics.

**Qq- and Partial Metric Spaces.** Let us now discuss the connection with partial metric spaces. We here consider the non-symmetric variant of the partial metric spaces from [4], called partial quasi-metric spaces (PQM) [24]. As we anticipated, these are metrics $p$ for which the usual reflexivity condition $p(x, x) = 1$ is replaced by the weaker quasi-reflexivity condition $p(x, x) \supseteq p(x, y)$. However, unlike the qq-metrics just discussed, PQMs satisfy a stronger transitivity condition. When $\mathcal{Q} = [0, +\infty]$ is the Lawvere quantale, this condition reads as

$$ p(x, z) + p(z, y) - p(z, z) \supseteq p(x, y). \qquad \text{(strong transitivity in } [0, +\infty]\text{)} $$
15:8 On the Metric Nature of (Differential) Logical Relations

The idea is that the self-distance of the central term z is “subtracted”. For a general quantale Q, this becomes:

$$p(x, z) \otimes (p(z, z) \to p(z, y)) \subseteq p(x, y). \qquad (\text{strong transitivity})$$

Define the relations $\Theta_s^l, \Theta_s^r \in \mathcal{QRel}(X, X)$ by $\Theta_s^l(x, y) = s(y, y) \to s(x, y)$ and $\Theta_s^r(x, y) = s(x, x) \to s(x, y)$. A PQM can be thus more concisely be defined as a relation $s \in \mathcal{QRel}(X, X)$ satisfying $s \subseteq \Delta_1 s$ and $s \otimes \Theta_s^r \subseteq s$. Notice that strong transitivity $s \otimes \Theta_s^r \subseteq s$ looks similar to the right transitivity $s \otimes q_s^r \subseteq s$. Indeed, the following result relates the relations $\Theta_s^c$ and $s^c$:

**Proposition 8.** For all $s \in \mathcal{QRel}(X, X)$ and $c \in \{l, r\}$, $s^c \subseteq \Theta_s^c$. Moreover, if $s$ is quasi-reflexive, $\Theta_s^c \subseteq s^c$ holds iff $\Theta_s^c$ is a quasi-metric iff $s$ is a partial quasi-metric.

The result above suggests that the partial quasi-metrics can be seen as limit cases of the qq-metrics, namely those for which the quasi-metric $s^r(x, y)$ can be written under the simpler form $\Theta_s^r(x, y) = s(x, x) \to s(x, y)$.

Unfortunately, while the standard definition of differential logical relations preserves qq-metrics, it does not preserve partial quasi-metrics: [17, 29] show that the function space constructions lifts PQMs into PQMs only when the monoidal product of the underlying quantales is *idempotent* (one talks in this case of a partial *ultra*-metric, since strong transitivity becomes $p(x, z) \wedge p(z, y) \subseteq p(x, y)$). Nevertheless, we will show in Section 7 how one can capture PQMs via a suitable family of logical relations.

4 Differential Logical Relations as Qq-Metrics

In this section we provide a semantic presentation of differential logical relations by defining a cartesian closed category of qq-metrics, this way highlighting the close correspondence between these two notions.

**From Q-Relations to Ternary Relations.** While in the previous section we discussed Q- relations, that is, binary relations valued in a quantale Q, the theory of differential logical relations is expressed in terms of ternary relations $\rho \subseteq X \times Q \times X$. In fact, any such relation $\rho \subseteq X \times Q \times X$ induces a Q-relation $\hat{\rho} \in \mathcal{QRel}(X, X)$ defined by

$$\hat{\rho}(x, y) = \bigvee \{a \in Q \mid (x, a, y) \in \rho\}.$$

Intuitively, $\hat{\rho}(x, y)$ is the smallest (recall the inversion of the order) distance between x and y. This correspondence can be made more precise as follows: a ternary relation $\rho \subseteq X \times Q \times X$ be said to be Q-closed when the following hold:

- $(x, a, y) \in \rho$ and $a' \subseteq a$ implies $(x, a', y) \in \rho$;

- if $(x, a_i, y) \in \rho$, for all $i \in I$, then $(x, \bigvee_{i \in I} a_i, y) \in \rho$.

We will use Q-closedness to derive results in Section 6.

In Appendix A (Lemma 21), we show that the map $\rho \mapsto \hat{\rho}$ defines a bijection between the Q-closed relations $\rho \subseteq X \times Q \times X$ and $\mathcal{QRel}(X, X)$. In the sequel, we will identify metrics with their corresponding Q-closed relations.

**A Cartesian Closed Category of Qq-Metrics.** We now define a category of qq-metrics. Let us recall notations from Section 2. For sets A and B, we denote the set of functions from A to B by $A \Rightarrow B$; for quantales Q and $\mathcal{R}$, we denote the set of monotone functions from Q to $\mathcal{R}$ by $Q \to \mathcal{R}$. Below, we write $f \cdot x$ for the application of $f: A \to B$ to $x \in A$, and we suppose that $(-) \cdot (-)$ is left-associative, i.e., $f \cdot x \cdot y$ is an abbreviation of $(f \cdot x) \cdot y$.
The category **Qqm** of qq-metrics is defined as follows:

- objects are triples $X = (Q_X, |X|, \rho_X)$ consisting of a quantale $Q_X$, a set $|X|$ and a qq-metric $\rho_X \subseteq |X| \times Q_X \times |X|$;

- morphisms from $X$ to $Y$ are triples $(f, a, f')$ consisting of functions $f, f': |X| \to |Y|$ and $a: |X| \to (Q_X \to Q_Y)$ such that for all $(x, b, x') \in \rho_X$, we have $(f \cdot x, a \cdot x \cdot b, f' \cdot x') \in \rho_Y$ and $(f \cdot x, a \cdot x \cdot b, f \cdot x') \in \rho_Y$.

The identity morphism on an object $X$ is $(\mathrm{id}_X, i_X, \mathrm{id}_X)$ consisting of the identity function $\mathrm{id}_X$ on $|X|$ and a function $i_X: |X| \to (Q_X \to Q_Y)$ given by $i_X \cdot x \cdot a = a$. The composition of $(f, a, f'): X \to Y$ and $(g, b, g'): Y \to Z$ is $(g \circ f, c, g' \circ f')$ where $c: |X| \to (Q_X \to Q_Z)$ is given by $c \cdot x = (b \cdot (f \cdot x)) \circ (a \cdot x)$.

**► Proposition 9.** *The category Qqm is cartesian closed.*

The cartesian closed structure closely matches the construction of differential logical relations in Section 2. The terminal object $\top$ is $(\{*\}, \{*\}, \rho_\top)$ where $\rho_\top = \{(*, *, *)\}$, and the product of $X$ and $Y$ is $X \times Y = (Q_X \times Q_Y, |X| \times |Y|, \rho_{X \times Y})$, where $\rho_{X \times Y}$ is given by

$$((x, y), (a, b), (x', y')) \in \rho_{X \times Y} \iff (x, a, x') \in \rho_X \text{ and } (y, b, y') \in \rho_Y.$$

The exponential $X \Rightarrow Y$ is given by $(|X| \Rightarrow (Q_X \to Q_Y), |X| \Rightarrow |Y|, \rho_{X \Rightarrow Y})$ where

$$(f, a, f') \in \rho_{X \Rightarrow Y} \iff \text{for all } (x, b, x') \in \rho_X \text{ and } g \in \{f, f'\}, (f \cdot x, a \cdot x \cdot b, g \cdot x') \in \rho_Y.$$

Here, the quantale structure of $Q_{X \times Y}$ and $Q_{X \Rightarrow Y}$ are given by the pointwise manner. We give details of the cartesian closed structure in Appendix B.

**► Example 10.** We define an object $R \in \mathbf{Qqm}$ to be $(\mathbb{R}, [0, +\infty], \rho_R)$, where

$$(x, a, x') \in \rho_R \iff |x - x'| \geq a.$$

Observe that the distance $\hat{\rho}_R: \mathbb{R} \times \mathbb{R} \to [0, +\infty)$ is just the Euclidean distance $\hat{\rho}_R(x, y) = |y - x|$. For functions $f, g: \mathbb{R} \to \mathbb{R}$, an element $a \in Q_{R \Rightarrow R}$ satisfies $(f, a, g) \in \rho_{R \Rightarrow R}$ if and only if we have $a \cdot x \cdot b \subseteq \bigwedge_{|x-y| \geq b} |f \cdot x - g \cdot y|$, i.e., $a$ bounds gaps between outputs of $f$ and $g$. In particular, we have $(f, \top, f) \in \rho_{R \Rightarrow R}$ if and only if $f$ is a constant function. We note that the largest element $\top \in Q_{R \Rightarrow R}$ is given by $\top \cdot x \cdot b = 0$.

# 5 The Fundamental Lemma

In this section we establish the fundamental lemma of differential logical relations for a simply typed lambda calculus $\Lambda_{\mathrm{Real}}$, by relying on the cartesian closed category **Qqm** of qq-metrics. We then apply this result to measure differences between functions.

**Syntax and Set-theoretic Semantics.** Our language $\Lambda_{\mathrm{Real}}$ comprises a type of real numbers and first order functions on $\mathbb{R}$. Let $\mathrm{Var}$ be a countably infinite set of variables. We define types and terms as follows:

(type) A, B := Real | A × B | A ⇒ B,

(term) t, s := x ∈ Var | r | φ(t₁, ..., tₙ) | t s | λx: A.t | <t, s> | fst(t) | snd(s).

Here, $r$ varies over $\mathbb{R}$, and $\phi$ varies over the set of multi-arity functions on $\mathbb{R}$, namely, $\phi$ is a function from $\mathbb{R}^n$ to $\mathbb{R}$ for some $n \in \mathbb{N}$. We call $n$ the *arity* of $\phi$, and we denote the *arity* of $\phi$ by $\mathrm{ar}(\phi)$. We adopt the standard typing rules given in Figure 1. Below, we denote the set of types by **Type** and the set of closed terms of type A by $\mathbf{T}_A$.
15:10 On the Metric Nature of (Differential) Logical Relations

<figure><img src="image_3.png" /><figcaption>Figure 1 Typing Rules.</figcaption></figure>

We denote the standard set theoretic interpretation of $\Lambda_{\text{Real}}$ by $\langle - \rangle$. (See [25] for example.)
To be concrete, the interpretation $\langle \mathbf{A} \rangle$ of a type $\mathbf{A}$ is a set inductively defined by

$$ \langle \text{Real} \rangle = \mathbb{R}, \quad \langle \mathbf{A} \times \mathbf{B} \rangle = \langle \mathbf{A} \rangle \times \langle \mathbf{B} \rangle, \quad \langle \mathbf{A} \Rightarrow \mathbf{B} \rangle = \langle \mathbf{A} \rangle \Rightarrow \langle \mathbf{B} \rangle; $$

and we interpret a term $x_1 : A_1, \dots, x_n : A_n \vdash t : B$ as a function $\langle t \rangle$ from $(\langle A_1 \rangle) \times \dots \times (\langle A_n \rangle)$ to $(\langle B \rangle)$. We give the definition of $\langle t \rangle$ in Appendix C.

**The Fundamental Lemma.** We inductively define a qq-metric space $\llbracket \mathbf{A} \rrbracket$ by

$$ \llbracket \text{Real} \rrbracket = R, \quad \llbracket \mathbf{A} \times \mathbf{B} \rrbracket = \llbracket \mathbf{A} \rrbracket \times \llbracket \mathbf{B} \rrbracket, \quad \llbracket \mathbf{A} \Rightarrow \mathbf{B} \rrbracket = \llbracket \mathbf{A} \rrbracket \Rightarrow \llbracket \mathbf{B} \rrbracket. $$

Here, $R$ is the qq-metric given in Example 10. Below, we simply denote the structure of an object $\llbracket \mathbf{A} \rrbracket$ by $(\mathcal{Q}_{\mathbf{A}}, |\mathbf{A}|, \rho_{\mathbf{A}})$. It is straightforward to check that for every type $\mathbf{A}$, we have $|\mathbf{A}| = \langle \mathbf{A} \rangle$. The qq-metrics $\llbracket \mathbf{A} \rrbracket$ are the categorical interpretation of types $\mathbf{A}$, and the following fundamental lemma is derived from the categorical interpretation of $\Lambda_{\text{Real}}$-terms in **Qqm**.

**▶ Theorem 11 (Fundamental Lemma).** Let $\Gamma = (x_1 : A_1, \dots, x_n : A_n)$ be a typing context.
For every term $\Gamma \vdash t : A$, and for every $(x, a, x') \in \rho_{A_1 \times \dots \times A_n}$, we have

$$ \langle \langle t \rangle \mid x, \langle t \rangle \mid x \cdot a, \langle t \rangle \mid x' \rangle \in \rho_A $$

where we inductively define $\langle \langle t \rangle \rangle \in \mathcal{Q}_{A_1 \times \dots \times A_n \Rightarrow \mathbf{B}}$ as follows:

- We define $\langle x_i \rangle \cdot (x_1, \dots, x_n) \cdot (a_1, \dots, a_n)$ to be $a_i$.

- We define $\langle \Gamma \rangle \cdot x \cdot a$ to be $\mathbf{0}$.

- We define $\langle \phi(t_1, \dots, t_n) \rangle \cdot x \cdot a$ to be $\phi^d(\langle t_1 \rangle \cdot x, \dots, \langle t_n \rangle \cdot x, \langle t_1 \rangle \cdot x \cdot a, \dots, \langle t_n \rangle \cdot x \cdot a)$
  where we define $\phi^d: \mathbb{R}^n \times [0, +\infty]^n \to [0, +\infty]$ by

$$ \phi^d(y_1, \dots, y_n, b_1, \dots, b_n) = \bigwedge_{|y_1 - z_1| \ge b_1} \dots \bigwedge_{|y_n - z_n| \ge b_n} |\phi(y_1, \dots, y_n) - \phi(z_1, \dots, z_n)|. $$

- We define $\langle t s \rangle \cdot x \cdot a$ to be $\langle t \rangle \cdot x \cdot a \cdot (\langle s \rangle \cdot x) \cdot (\langle s \rangle \cdot x \cdot a)$.

- We define $\langle \lambda x : A. t \rangle \cdot (x_1, \dots, x_n) \cdot (a_1, \dots, a_n) \cdot y \cdot b$ to be $\langle t \rangle \cdot (x_1, \dots, x_n, y) \cdot (a_1, \dots, a_n, b)$.

- We define $\langle \langle t, s \rangle \rangle \cdot x \cdot a$ to be $(\langle t \rangle \cdot x \cdot a, \langle s \rangle \cdot x \cdot a)$.

- We define $\langle \text{fst}(t) \rangle \cdot x \cdot a$ to be the first component of $\langle t \rangle \cdot x \cdot a$.

- We define $\langle \text{snd}(t) \rangle \cdot x \cdot a$ to be the second component of $\langle t \rangle \cdot x \cdot a$.

The fundamental lemma is a way to compositionally reason about distances.

**▶ Example 12.** Let us fix a positive real number $\epsilon$. We define $D_{\epsilon}: (\mathbb{R} \Rightarrow \mathbb{R}) \to (\mathbb{R} \Rightarrow \mathbb{R})$ by

$$ D_{\epsilon} = \langle \lambda f : \text{Real} \Rightarrow \text{Real} \cdot \lambda x : \text{Real} \cdot \text{df}_{\epsilon}(f(\text{ad}_{\epsilon}(x)), f(x)) \rangle $$
where $df_\epsilon(x, y) = \frac{x-y}{\epsilon}$ and $ad_\epsilon(x) = x + \epsilon$. For $f: \mathbb{R} \to \mathbb{R}$ and $x \in \mathbb{R}$, $D_\epsilon \cdot f \cdot x$ calculates an approximation of the derivative of $f$ at $x$:

$$D_{\epsilon} \cdot f \cdot x = \frac{f(x + \epsilon) - f(x)}{\epsilon}.$$

By the fundamental lemma, we obtain $(D_\epsilon, E_\epsilon, D_\epsilon) \in \rho_{(R \Rightarrow R) \Rightarrow (R \Rightarrow R)}$ where $E_\epsilon$ is a function from $|R \Rightarrow R|$ to $Q_{R \Rightarrow R} \to Q_{R \Rightarrow R}$ given by

$$E_{\epsilon} \cdot f \cdot a = \lambda x : \mathbb{R}. \lambda b : [0, +\infty]. \frac{a \cdot (x + \epsilon) \cdot b + a \cdot x \cdot b}{\epsilon}.$$

We note that $E_\epsilon$ depends on our choice of term denoting $D_\epsilon$. In Example 15, we will observe that $(\mathrm{id}_R, a, \sin)$ is an element of $\rho_{R \Rightarrow R}$ where $\mathrm{id}_R$ is the identity function on $\mathbb{R}$, and $a \in Q_{R \Rightarrow R}$ is given by $a \cdot x \cdot b = |x - \sin(x)| + b$. By applying $(D_\epsilon, E_\epsilon, D_\epsilon)$ to $(\mathrm{id}_R, a, \sin)$, we obtain $(D_\epsilon \cdot \mathrm{id}_R, a', D_\epsilon \cdot \sin) \in \rho_R$ where

$$a' \cdot x \cdot b = \frac{|x + \epsilon - \sin(x + \epsilon)| + |x - \sin(x)| + 2b}{\epsilon}.$$

From this, we see that the distance between $D_\epsilon \cdot \mathrm{id}_R \cdot 0$ and $D_\epsilon \cdot \sin \cdot 0$ is bounded by $\frac{|\epsilon - \sin(\epsilon)|}{\epsilon}$. We note that $a'$ is not the exact distance between $D_\epsilon \cdot \mathrm{id}_R$ and $D_\epsilon \cdot \sin$. For example, while $|D_{0.1} \cdot \mathrm{id}_R \cdot 0 - D_{0.1} \cdot \sin \cdot 0.1| \approx 0.01$, we have $a' \cdot 0 \cdot 0.1 \approx 2$. This gap stems in the fact that $(D_\epsilon, E_\epsilon, D_\epsilon)$ takes all functions into account and cannot exploit continuity of specific functions.

# 6 Quasi-Metric Logical Relations

As described in Section 3, any qq-metric gives rise to left and right observational quasi-metrics. In this section, we introduce a class of logical relations $\gamma_A$ that capture the left observational quasi-metric associated to $\rho_A$. We will then show how such relations can be used to derive over-approximations of distances between functions.

For a type A, we define $\gamma_A \subseteq |A| \times Q_A \times |A|$ by induction on A as follows:

$$\begin{align*}
(x, a, x') &\in \gamma_{\mathrm{Real}} &\iff |x - x'| &\ni a, \\
(f, a, f') &\in \gamma_{A \Rightarrow B} &\iff &\text{for all } (x, b, x') \in \rho_A, (f \cdot x, a \cdot x \cdot b, f' \cdot x) \in \gamma_B, \text{ and} \\
((x, y), (a, b), (x', y')) &\in \gamma_{A \times B} &\iff &\text{for all } (f', b, f') \in \rho_{A \Rightarrow B}, (f, a \otimes b, f) \in \rho_{A \Rightarrow B}, \\
((x, y), (a, b), (x', y')) &\in \gamma_{A \times B} &\iff &\text{for all } (x, a, x') \in \gamma_A \text{ and } (y, b, y') \in \gamma_B.
\end{align*}$$

We give some explanation on the definition of $\gamma_{A \Rightarrow B}$. The definition consists of two conditions. The first condition means that, if $(f, a, f')$ is an element of $\gamma_{A \Rightarrow B}$, then the distance $a \cdot x \cdot b$ over-approximates the distance between $f$ and $f'$ at the same point $x$ (rather than on distinct points, as is the case for the relation $\rho_{A \Rightarrow B}$). The second condition means that $a$ also over-approximates the gap between the self-distance of $f'$ and the self-distance of $f$.

Recall that $\rho_A^l$ is the quasi-metric representing the left observational quasi-metrics associated with the qq-metric $\rho_A$. In Appendix D, we give some auxiliary lemmas and proofs for Proposition 13 and Theorem 14.

**Proposition 13.** For every type A, we have $\rho_A^l = \gamma_A$.

We can use Proposition 13 to over-approximate $\rho$-distances in terms of $\gamma$-distances and the left observational quasi-metric. Let us sketch our idea. First, thanks to Proposition 13 and Proposition 6, we can exploit left-transitivity to pass from a $\gamma$-distance between $t$ and $s$ and a self-$\rho$-distance of $s$ to a $\rho$-distance between $t$ and $s$:

$$((|t|, a), (|s|)) \in \gamma_A \text{ and } ((|s|, b), (|s|)) \in \rho_A \implies ((|t|, a \otimes b), (|s|)) \in \rho_A. \quad (\text{left transitivity})$$
15:12 On the Metric Nature of (Differential) Logical Relations

Second, thanks to the fundamental lemma, we can always obtain a $\rho$-distance by summing a
$\gamma$-distance with the self-distance $\|\cdot\|$:

$$
((|t|), a, (|s|)) \in \gamma_A \implies ((|t|), a \otimes \|s\|, (|s|)) \in \rho_A. \quad (\rho \supseteq \gamma \otimes \text{self-}\rho)
$$

The following result exploits this last idea to bound the distance between two functions $f$ and $g$ by summing the “vertical distance” between $f$ and $g$ (that is, the distance of $f(x)$ and $g(x)$ for some fixed $x$) with an approximation of the self-distances of $f$ and $g$:

► **Theorem 14.** Let $A$ be a type. For any $f, f' \in |A| \Rightarrow \text{Real}|$ and any $a, a' \in Q_{A \Rightarrow \text{Real}}$, if

$|f \cdot x - f' \cdot x| \supseteq a \cdot x \cdot b$ for all $(x, b, x') \in \rho_A$; and

$ (f, a', f) \in \rho_{A \Rightarrow \text{Real}} \text{ and } (f', a', f') \in \rho_{A \Rightarrow \text{Real}}, $
then $ (f, a \otimes a', f') \in \rho_{A \Rightarrow \text{Real}} $.

**Example 15.** Let $\mathrm{id}_{\mathbb{R}}$ be the identity function on $\mathbb{R}$. By the fundamental lemma with a simple calculation, we obtain $(\mathrm{id}_{\mathbb{R}}, a', \mathrm{id}_{\mathbb{R}}) \in \rho_{R \Rightarrow R}$ and $(\sin, a', \sin) \in \rho_{R \Rightarrow R}$ where $a' \cdot x \cdot b = b$. By Theorem 14, $a \in Q_{R \Rightarrow R}$ given by $a \cdot x \cdot b = |x - \sin(x)|$ satisfies $(\mathrm{id}_{\mathbb{R}}, a \otimes a', \sin) \in \rho_{R \Rightarrow R}$. To be concrete, $(a \otimes a') \cdot x \cdot b = |x - \sin(x)| + b$, which means that the distance between $x$ and $\sin(y)$ is small when $x$ and $y$ are close to 0.

► **Remark 16.** Due to asymmetry in the definition of the exponential $X \Rightarrow Y$ in $\mathbf{Qqm}$, it is not clear how to capture the right observational quasi-metrics in a similar manner. However, we will see that right observational quasi-metrics can be captured by partial metric logical relations introduced in the next section.

7 Partial Metric Logical Relations

As discussed in Section 3, the qq-metrics $\rho_A$ are not, in general, partial metrics. In this
section we introduce a family of differential logical relations ($\eta_A$)$_{A \in \text{Types}}$ that defines a class of
partial quasi-metrics over $\Lambda_{\text{Real}}$. The fundamental (indeed, the only) difference with respect
to the family $\rho_A$ is, as it may be expected, in the case of the function type.

For any type A, we define $\eta_A \subseteq |A| \times Q_A \times |A|$ by induction on A as follows:

$$
(x, a, x') \in \eta_{\mathbb{R}al} \iff |x - x'| \supseteq a,
$$

$$
\begin{align*}
(f, a, f') \in \eta_{A \Rightarrow B} &\iff \text{there are } a_1, a_2 \in Q_{A \Rightarrow B} \text{ such that } a_1 \otimes a_2 \supseteq a \text{ and} \\
&\phantom{\iff \text{there are }} \text{for all } (x, b, x') \in \eta_A, (f \cdot x, a_1 \cdot x \cdot b, f \cdot x') \in \eta_B \text{ and}
\end{align*}
$$

$$
(f \cdot x', a_2 \cdot x \cdot b, f' \cdot x') \in \eta_B,
$$

$$
((x, y), (a, b), (x', y')) \in \eta_{A \times B} \iff (x, a, x') \in \eta_A \text{ and } (y, b, y') \in \eta_B.
$$

The idea of the definition of η_A⇒B is that if (f, a, f') ∈ η_A⇒B, then a must be larger than or equal to the sum of the self-distance of f and of the “vertical” distances between f and f'. The following result shows that the relations η_A define partial quasi-metrics on all types.

For $(f, a, f') \in \eta_{A \Rightarrow B}$, we call a pair $a_1, a_2 \in Q_{A \Rightarrow B}$ satisfying the condition in the definition of $(f, a, f') \in \eta_{A \Rightarrow B}$ a decomposition of $(f, a, f') \in \eta_{A \Rightarrow B}$.

► **Proposition 17.** For all types A:

- For any type A, the relation $\rho_A$ is $\mathbb{Q}$-closed. In particular, for all $(x, a, x') \in \eta_A$, the set of decompositions of $(x, a, x') \in \eta_A$ is a complete lattice.

- If $(x, a, x') \in \eta_A$, then $(x, a, x) \in \eta_A$.

- If $(x, a, z) \in \eta_A$ and $(z, b, y) \in \eta_A$, then there exists $c_1, c_2 \in Q_A$ such that $a \otimes b \subseteq c_1 \otimes c_2$, $(z, c_1, z) \in \eta_A$ and $(x, c_2, y) \in \eta_A$. In particular, $(x, a \otimes (c_1 \to b), y) \in \eta_A$.
$$
\begin{array}{l}
x^{\bullet} = \dot{x} \qquad \underline{t}^{\bullet} = \underline{0} \qquad (ts)^{\bullet} = t^{\bullet}ss^{\bullet} \qquad (\lambda x : A. t)^{\bullet} = \lambda x : A. \lambda \dot{x} : A^{\bullet} . t^{\bullet} \qquad \langle t, s \rangle^{\bullet} = \langle t^{\bullet}, s^{\bullet} \rangle \\
\\
(fst(t))^{\bullet} = fst(t^{\bullet}) \qquad (snd(t))^{\bullet} = snd(t^{\bullet}) \qquad (\phi(t_1, \dots, t_n))^{\bullet} = \phi^d(t_1, \dots, t_n, t_1^{\bullet}, \dots, t_n^{\bullet})
\end{array}
$$

Figure 2 Derivative of Term.

By adapting the definition of $\gamma_A$ from Section 6, we can capture the left observational quasi-metrics $\rho_A^l$ associated with the partial quasi-metrics $\eta_A$. Moreover, by Proposition 8, the right observational quasi-metric $\rho_A^r$ satisfies $(x, \hat{\eta}_A(x, x) \dashv a, y) \in \rho_A^r \iff (x, a, y) \in \eta_A$. Thanks to this, we can capture this quasi-metrics via the logical relations $\delta_A \subseteq |A| \times Q_A \times |A|$ defined by induction on $A$, letting the base and product case being defined as for $\gamma_A$, and the function case being as follows:

$$ (f, a, f') \in \delta_{A \Rightarrow B} \iff \text{for all } (f, b, f) \in \eta_{A \Rightarrow B}, (f, a \otimes b, f') \in \eta_{A \Rightarrow B}. $$

**Proposition 18.** For every type $A$, we have $\rho_A^r = \delta_A$.

## 8 A Quantitative Equational Theory

The goal of this section is to introduce an equational theory to formally deduce differences between programs. To this end, we first give a syntactic presentation of differential logical relations internally to the language of $\Lambda_{\text{Real}}$, and then introduce a deductive system to deduce program differences.

While our idea is inspired by the quantitative equational theories of Mardare et al. [27], it differs in two respects: first, distances need not be real numbers, but are presented as arbitrary $\Lambda_{\text{Real}}$-programs; second, non-expansiveness is replaced by the condition corresponding to the fundamental lemma of differential logical relations.

**Preparation.** Before we go into construction, we prepare some syntactic counter parts of constructions in the fundamental lemma for $\mathbf{Qqm}$. We first inductively define a type $A^\bullet$ by

$$ \text{Real}^{\bullet} = \text{Real}, \quad (A \Rightarrow B)^{\bullet} = A \Rightarrow A^{\bullet} \Rightarrow B^{\bullet}, \quad (A \times B)^{\bullet} = A^{\bullet} \times B^{\bullet}. $$

This is a syntactic counter part of quantales $Q_A$. The reason that we define $\text{Real}^\bullet$ to be $\text{Real}$ even though $\text{Real}^\bullet$ should be a type of non-negative extended real numbers is to keep the syntax of $\Lambda_{\text{Real}}$ simple. It is possible to extend $\Lambda_{\text{Real}}$ with a type $\text{Real}^{\circ} \supseteq \emptyset$ of non-negative extended real numbers and types $A \to B$ of monotone functions. We next give a syntactic counter part of $\{\|t\|\}$. For this purpose, we suppose that there is a partition $\text{Var} = \text{Var}_0 \cup \text{Var}_1$, i.e., there are mutually disjoint subsets $\text{Var}_0, \text{Var}_1 \subseteq \text{Var}$ such that $\text{Var}$ is equal to $\text{Var}_0 \cup \text{Var}_1$. Furthermore, we suppose that there is a bijection $(-): \text{Var}_0 \to \text{Var}_1$. In the sequel, we denote variables in $\text{Var}_1$ by dotted symbols $\dot{x}, \dot{y}, \dot{z}, \dots$, and we denote variables in $\text{Var}_0$ by $x, y, z, \dots$. Based on this convention, for a typing context $\Gamma = (x_1 : A_1, \dots, x_n : A_n)$, we define a typing context $\Gamma^\bullet$ by $\Gamma^\bullet = (\dot{x}_1 : A_1^\bullet, \dots, \dot{x}_n : A_n^\bullet)$. Now, for a term $\Gamma \vdash t : A$, we define a term $\Gamma, \Gamma^\bullet \vdash t^\bullet : A$, which we call the *derivative* of $t$, in Figure 2. The definition of $t^\bullet$ corresponds to the definition of $\{\|t\|\}$, and we can find the same construction in [9].

**Syntactic Differential Logical Relations.** By adopting the structure of $\mathbf{Qqm}$, we define a type-indexed family $\{\delta_A^\circ \subseteq T_A \times T_{A^\bullet} \times T_A\}_{A \in \text{Type}}$ of ternary predicates as follows:
15:14 On the Metric Nature of (Differential) Logical Relations

$$
(t, a, t') \in \delta_{\text{Real}}^{\text{log}} \iff \text{there are } r, r' \in \mathbb{R} \text{ and } s \in [0, +\infty] \text{ such that } |r - r'| \ge s \text{ and} \\
\qquad \vdash t = r : \text{Real and } \vdash a = s : \text{Real and } \vdash t' = r' : \text{Real,}
$$

$$
\begin{align*}
(t, a, t') \in \delta_{A \Rightarrow B}^{\text{log}} &\iff \text{for any } (s, b, s') \in \delta_A^{\text{log}}, (ts, asb, t's') \in \delta_B^{\text{log}} \text{ and } (ts, asb, ts') \in \delta_B^{\text{log}}, \\
(t, a, t') \in \delta_{A \times B}^{\text{log}} &\iff (fst(t), fst(a), fst(t')) \in \delta_A^{\text{log}} \text{ and } (snd(t), snd(a), snd(t')) \in \delta_B^{\text{log}}
\end{align*}
$$

where we write $\Gamma \vdash t = s : A$ when the equality between $\Gamma \vdash t : A$ and $\Gamma \vdash s : A$ is derivable
from the standard equational theory consisting of $\beta\eta$-equalities extended with the following
axiom for every multi-arity function $\phi$:

$$
\Gamma \vdash \phi(\underline{r_1}, \dots, \underline{r_{\mathrm{ar}(\phi)}}) = \underline{\phi(r_1, \dots, r_{\mathrm{ar}(\phi)})} : \mathrm{Real}.
$$

Although $\mathbf{T}_A$ is not a quantale in general, we can show that $\delta_A^{\text{log}}$ satisfies “left quasi-reflexivity”,
“transitivity” and a fundamental lemma in the following form.

► **Proposition 19.** Let A be a type.

■ If (t, a, t') ∈ δ<sub>A</sub><sup>log</sup>, then (t, a, t) ∈ δ<sub>A</sub><sup>log</sup>.

■ If (t, a, t') ∈ δ<sub>A</sub><sup>log</sup> and (t', a', t'') ∈ δ<sub>A</sub><sup>log</sup>, then (t, add<sub>A</sub> a a', t'') ∈ δ<sub>A</sub><sup>log</sup> where add<sub>Real</sub> ∈ T<sub>Real⇒Real⇒Real</sub> is the binary addition, and add<sub>A</sub> ∈ T<sub>A⇒A⇒A</sub> for arbitrary type A is inductively given by

$$
\mathrm{add}_{A \Rightarrow B} = \lambda xy : A \Rightarrow B. \lambda z : A. \mathrm{add}_B (xz) (yz),
$$

$$
\mathrm{add}_{A \times B} = \lambda xy : A \times B. \langle \mathrm{add}_A \mathrm{fst}(x) \mathrm{fst}(y), \mathrm{add}_B \mathrm{snd}(x) \mathrm{snd}(y) \rangle.
$$

■ For any term x₁ : A₁, ..., xₙ : Aₙ ⊢ t : A, and for any family {⟨sᵢ, aᵢ, s'ᵢ⟩ ∈ δ<sub>Aᵢ</sub><sup>log</sup>}₁≤i≤n,

$$
(t[s_1/x_1, \dots, s_n/x_n], t^*[s_1/x_1, \dots, s_n/x_n, a_1/\dot{x}_1, \dots, a_n/\dot{x}_n], t'[s'_1/x_1, \dots, s'_n/x_n]) \in \delta_A^{\text{log}}.
$$

■ If (t, a, t') ∈ δ<sub>A</sub><sup>log</sup> and ⊢ t = s : A and ⊢ a = b : A• and ⊢ t' = s' : A, then (s, b, s') ∈ δ<sub>A</sub><sup>log</sup>.

**Equational Metric.** We introduce a formal system to infer $\delta^{\text{log}}$-distances between terms.
For terms $\Gamma \vdash t : A$ and $\Gamma, \Gamma' \vdash a : A$ and $\Gamma \vdash t' : A$, we write $\Gamma \vdash (t, a, t') : A$ when we
can derive this judgment from the rules given in Figure 3 where in the derivation rule for
an $n$-ary function $\phi$ on $\mathbb{R}$, $D(\phi)$ is a set of $2n$-ary functions on $\mathbb{R}$ given by $\psi \in D(\phi)$ if and
only if for all triples of reals $(r_i, r'_i, s_i)_{1 \le i \le n}$, if $|r_i - r'_i| \le s_i$ for any $i \in \{1, \dots, n\}$, then
$|\phi(r_1, \dots, r_n) - \phi(r'_1, \dots, r'_n)| \le \psi(r_1, \dots, r_n, s_1, \dots, s_n)$. The last rule in Figure 3 makes the
judgement compatible with the equational theory for terms. Then, we define a type-indexed
ternary predicate $\{\delta_A^{\text{eq}} \subseteq \mathbf{T}_A \times \mathbf{T}_A \cdot \times \mathbf{T}_A\}_{A \in \text{Type}}$ by

$$
(t, a, t') \in \delta_A^{\text{eq}} \iff \vdash (t, a, t') : A.
$$

We note that quasi-reflexivity and transitivity for arbitrary A follows from left quasi-reflexivity
and transitivity for Real. We can also show that $\delta^{\text{eq}}$ is subsumed by $\delta^{\text{log}}$. We can check the
following proposition by induction on types.

► **Proposition 20.** Let A be a type.

■ If (t, a, t') ∈ δ<sub>A</sub><sup>eq</sup>, then (t, a, t) ∈ δ<sub>A</sub><sup>eq</sup>.

■ If (t, a, t') ∈ δ<sub>A</sub><sup>eq</sup> and (t', a', t'') ∈ δ<sub>A</sub><sup>eq</sup>, then (t, add<sub>A</sub> a a', t'') ∈ δ<sub>A</sub><sup>eq</sup>.

■ For any term x₁ : A₁, ..., xₙ : Aₙ ⊢ t : A, and for any family {⟨sᵢ, aᵢ, s'ᵢ⟩ ∈ δ<sub>Aᵢ</sub><sup>eq</sup>}₁≤i≤n,

$$
(t[s_1/x_1, \dots, s_n/x_n], t^*[s_1/x_1, \dots, s_n/x_n, a_1/\dot{x}_1, \dots, a_n/\dot{x}_n], t'[s'_1/x_1, \dots, s'_n/x_n]) \in \delta_A^{\text{eq}}.
$$

■ If (t, a, t') ∈ δ<sub>A</sub><sup>eq</sup>, then (t, a, t') ∈ δ<sub>A</sub><sup>log</sup>.
<figure><img src="image_4.png" /><figcaption>Figure 3 Derivation Rules.</figcaption></figure>

## 9 A Lattice of Qq-Metrics?

We conclude our presentation with a few open questions about the relations holding between the different notions of program difference introduced in this paper. It is well-known that different notions of program equivalence for a given language can be compared, with one equivalence being *coarser* than another one when it identifies *more* programs than the other. Under this ordering, program equivalences do indeed form a complete lattice, with observational equivalences usually being the coarsest ones, and those arising from syntactic equational theories being the finest ones.

In the last sections we have introduced various notions of program differences, all defined in terms of some form of differential logical relations. Could it be possible to compare such program differences similarly to what can be done for program equivalences? Notably, the following two natural questions can be raised:

- Does the type indexed family $\delta^{\log}$ give rise to the “coarsest family of qq-metrics”?

- Does the type indexed family $\delta^{\text{eq}}$ give rise to the “finest family of qq-metrics”?

We note that, although such differences are defined over $T_{A\bullet}$, which is not a quantale, we can easily associate $\delta^{\log}$ and $\delta^{\text{eq}}$ with qq-metrics valued on the quantale $\mathcal{P}T_{A\bullet}$ of subsets of $T_{A\bullet}$, letting e.g. $(t, a, t') \in \delta_A^{\log} \iff$ for all $a \in a$, $(t, a, t') \in \delta_A^{\log}$, and similarly for $\delta_A^{\text{eq}}$.

Unfortunately, it is not straightforward to tackle these questions because of two main obstacles. First, while two qq-metrics valued over the same quantale can be easily compared, it is not clear how to compare two qq-metrics defined over *different* quantales. Second, while in the case of logical relations, the argument that logical equivalence is the coarsest one relies on the notion of *observational equivalence*, it is not clear how to define a similar notion of *observational qq-metric* for $\Lambda_{\text{Real}}$: since differences between programs describe relationships between differences of inputs and differences of outputs, when we measure differences between programs, we should observe differences between outputs of programs with respect to different contexts. Therefore, we should define a notion of difference between contexts *before* we define observational qq-metric for $\Lambda_{\text{Real}}$. How can we define differences between contexts?

## 10 Related Work

Differential logical relations for a simply typed language were introduced in [11], and later extended to languages with monads [10], and related to incremental computing [9]. Moreover, a unified framework for operationally-based logical relations, subsuming differential logical
15:16 On the Metric Nature of (Differential) Logical Relations

relations, was introduced in [7]. The connections with metric spaces and partial metric spaces have been explored already in [17, 29], on the one hand providing a series of negative results that motivate the present work, and on the other hand producing a class of metric and partial metric models based on a different relational construction.

The literature on the interpretation of linear or graded lambda-calculi in the category of metric spaces and non-expansive functions is ample [31, 15, 2, 16, 13]. A related approach is that of quantitative algebraic theories [27], which aims at capturing metrics over algebras via an equational presentation. These have been extended both to quantale-valued metrics [8] and to the simply typed (i.e. non graded) languages [12], although in the last case the non-expansivity condition makes the construction of interesting algebras rather challenging.

The literature on partial metric spaces is vast, as well. Introduced by Matthews [4], they have been largely explored for the metrization of domain theory [5, 34, 35] and, more recently, of λ-theories [26]. An elegant categorical description of partial metrics via the quantaloid of *diagonals* is introduced in [23]. As this construction is obviously related to the notion of quasi-reflexivity here considered, it would be interesting to look for analogous categorical descriptions of the qq-metrics here introduced.

11 Conclusion

In this paper we have explored the connections between the notions of program distance arising from differential logical relations and those defined via quasi-metrics and partial quasi-metrics. As discussed in Section 9, our results suggest natural and important questions concerning the comparison of all the notions of distance considered in this paper. At the same time, our results provide a conceptual bridge that could be used to exploit methods and results from the vast area of research on quantale-valued relations [22, 36] for the study of program distances in higher-order programming languages. For instance, natural directions are the characterization of limits and, more generally, of topological properties via logical relations, as suggested by recent work [3], although in a qualitative setting.

While we here focused on non-symmetric differential logical relations, understanding the metric structure of the symmetric case, as in [11], would be interesting as well. Notice that this would require to abandon quasi-reflexivity, cf. Remark 3.

Finally, while in this paper we only considered simple types, the notion of qq-metric is robust enough to account for other constructions like e.g. monadic types as in [10]. It is thus natural to explore the application of methods arising from quasi-metrics or partial quasi-metrics for the study of languages with effects like e.g. probabilistic choice.

References

1. Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, and C.-H. Luke Ong. Fixing incremental computation. In Luís Caires, editor, *Proc. of ESOP 2019*, pages 525–552. Springer, 2019.

2. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In *Proc. of POPL 2017*, pages 545–556. ACM, 2017. doi:10.1145/3009837.3009890.

3. Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, and Francesco Gavazzo. On Feller continuity and full abstraction. *Proc. ACM Program. Lang.*, 6(ICFP), August 2022. doi:10.1145/3547651.

4. Michael Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial metric spaces. *American Mathematical Monthly*, 116:708–718, October 2009. doi:10.4169/193009709X460831.
5 Michael A. Bukatin and Joshua S. Scott. Towards computing distances between programs via Scott domains. In Sergei Adian and Anil Nerode, editors, Proc. of LFCS 1997, pages 33–43. Springer, 1997. doi:10.1007/3-540-63045-7_4.

6 Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation. In Proc. of PLDI 2014, pages 145–155. ACM, 2014. doi:10.1145/2594291.2594304.

7 Francesco Dagnino and Francesco Gavazzo. A fibrational tale of operational logical relations: Pure, effectful and differential. Logical Methods in Computer Science, 20(2), April 2024. doi:10.46298/lmcs-20(2:1)2024.

8 Fredrik Dahlqvist and Renato Neves. A complete v-equational system for graded lambda-calculus. In Marie Kerjean and Paul Blain Levy, editors, Proc. of MFPS XXXIX, volume 3 of EPTICS, 2023. doi:10.46298/ENTICS.12299.

9 Ugo Dal Lago and Francesco Gavazzo. Differential logical relations, Part II increments and derivatives. Theoretical Computer Science, 895:34–47, 2021. doi:10.1016/J.TCS.2021.09.027.

10 Ugo Dal Lago and Francesco Gavazzo. Effectful program distancing. Proc. ACM Program. Lang., 6(POPL), January 2022. doi:10.1145/3498680.

11 Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In Proc. of ICALP 2019, volume 132 of LIPIcs, pages 111:1–111:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPICS.ICALP.2019.111.

12 Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In Proc. of FSCD 2022, volume 228 of LIPIcs, pages 4:1–4:18, Dagstuhl, Germany, 2022. doi:10.4230/LIPIcs.FSCD.2022.4.

13 Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In Proc. of FSCD 2023, volume 260 of LIPIcs, pages 20:1–20:19, Dagstuhl, Germany, 2023. doi:10.4230/LIPIcs.FSCD.2023.20.

14 Derek Dreyer, Amal Ahmed, and Lars Birkedal. Logical step-indexed logical relations. In Proc. of LICS 2009, pages 71–80. IEEE, 2009. doi:10.1109/LICS.2009.34.

15 Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. SIGPLAN Not., 48(1):357–370, January 2013. doi:10.1145/2480359.2429113.

16 Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Proc. of LICS 2018, pages 452–461. ACM, 2018. doi:10.1145/3209108.3209149.

17 Guillaume Geoffroy and Paolo Pistone. A partial metric semantics of higher-order types and approximate program transformations. In Proc. of CSL 2021, volume 183 of LIPIcs, pages 35:1–35:18, 2021. doi:10.4230/LIPIcs.CSL.2021.23.

18 Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

19 Jean Goubault-Larrecq. Non-Hausdorff Topology and Domain Theory: Selected Topics in Point-Set Topology. New Mathematical Monographs. Cambridge University Press, 2013.

20 Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. In Proc. of CSL 2002, pages 553–568. Springer, 2002. doi:10.1007/3-540-45793-3_37.

21 Claudio Hermida, Uday S. Reddy, and Edmund P. Robinson. Logical relations and parametricity - A Reynolds programme for category theory and programming languages. In Proc. of WACT 2013, volume 303 of ENTCS, pages 149–180. Elsevier, 2014. doi:10.1016/J.ENTCS.2014.02.008.

22 Dirk Hofmann, Gavin J Seal, and W Tholen. Monoidal Topology: a Categorical Approach to Order, Metric and Topology. Cambridge University Press, New York, 2014.

23 Dirk Hofmann and Isar Stubbe. Topology from enrichment: the curious case of partial metrics. Cahiers de Topologie et Géométrie Différentielle Catégorique, LIX, 4:307–353, 2018.
15:18 On the Metric Nature of (Differential) Logical Relations

24 H.-P.A. Künzi, H. Pajoohesh, and M.P. Schellekens. Partial quasi-metrics. *Theoretical Computer Science*, 365(3):237-246, 2006. doi:10.1016/j.tcs.2006.07.050.

25 Roy L.Crole. *Categories for Types*. Cambridge University Press, 1993.

26 Valentin Maestracci and Paolo Pistone. The Lambda Calculus Is Quantifiable. In *Proc. of CSL 2025*, volume 326 of *LIPIcs*, pages 34:1–34:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.CSL.2025.34.

27 Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In *Proc. of LICS 2016*. IEEE Computer Society, 2016.

28 Sparsh Mittal. A survey of techniques for approximate computing. *ACM Comput. Surv.*, 48(4), March 2016. doi:10.1145/2893356.

29 Paolo Pistone. On generalized metric spaces for the simply typed lambda-calculus. In *Proc. of LICS 2021*, pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470696.

30 Gordon Plotkin and Martin Abadi. A logic for parametric polymorphism. In *Proc. of TLCA 1993*, volume 664 of *LNCS*, pages 361–375. Springer, 1993. doi:10.1007/BFB0037118.

31 Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger. *Proc. of ICFP 2010*, pages 157–168, 2010.

32 John C. Reynolds. Types, abstraction and parametric polymorphism. In R.E.A. Mason, editor, *Information Processing '83*, pages 513–523. North-Holland, 1983.

33 Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Logical bisimulations and functional languages. In Farhad Arbab and Marjan Sirjani, editors, *Proc. of FSEN 2007*, pages 364–379. Springer, 2007. doi:10.1007/978-3-540-75698-9_24.

34 Michel P. Schellekens. A characterization of partial metrizability: domains are quantifiable. *Theoretical Computer Science*, 305(1-3):409–432, 2003. doi:10.1016/S0304-3975(02)00705-3.

35 Michael B. Smyth. The constructive maximal point space and partial metrizability. *Ann. Pure Appl. Log.*, 137(1-3):360–379, 2006. doi:10.1016/j.apal.2005.05.032.

36 Isar Stubbe. An introduction to quantaloid-enriched categories. *Fuzzy Sets and Systems*, 256:95–116, 2014. doi:10.1016/j.fss.2013.08.009.

**A Proofs for Section 3**

**Proof of Proposition 7.** Suppose there exists a quasi-metric $q \sqsupseteq s$ such that $s \otimes q \subseteq s$ holds. Then $s \otimes s \subseteq s \otimes q \subseteq s$, so $s$ is transitive. A similar argument works if $q$ is such that $q \otimes s \subseteq s$. Conversely, if $s$ is a qq-metric it is enough to let $q := s^r$ and use Proposition 6 (iv). ◀

**Proof of Proposition 8.** We only argue for $c = r$, the other case being similar. From $s^r(x, y) = \bigwedge_z s(z, x) \to s(z, y) \subseteq s(x, x) \to s(x, y) = (\Theta_s^r)(x, y)$ we deduce that $s^r \subseteq \Theta_s^r$. The converse direction $s^r \supseteq \Theta_s^r$ corresponds to showing that $s(z, x) \otimes (s(x, x) \to s(x, y)) \subseteq s(z, y)$, which holds iff $s$ is a partial quasi-metric. We have thus shown that $s$ is a PQM iff $\Theta_s^r = s^r$. This also implies that, if $s$ is a PWM, $\Theta_s^r$ is a quasi-metric. Finally, suppose $\Theta_s^r$ is a quasi-metric. By quasi-reflexivity, and the divisibility of $Q$, we have that $s(x, z) = s(x, x) \otimes (s(x, x) \to s(x, z))$. We then have $s(x, z) \otimes (s(z, z) \to s(z, y)) = s(x, x) \otimes (s(x, x) \to s(x, z)) \otimes (s(z, z) \to s(z, y)) \subseteq s(x, y)$, so $s$ is a partial quasi-metric. ◀

**Lemma 21.** The map $\rho \mapsto \hat{\rho}$ defines a bijection between the $Q$-closed relations $\rho \subseteq X \times Q \times X$ and $Q\text{Rel}(X, X)$.

**Proof.** Let $\rho, \tau$ be closed and let $\hat{\rho}(x, y) = \hat{\tau}(x, y)$. Observe that, for all $x, y \in X$, by $Q$-closure we have $(x, \hat{\rho}(x, y), y) \in \rho$. Suppose now that $(x, a, y) \in \tau$, then $a \subseteq \hat{\tau}(x, y) = \hat{\rho}(x, y)$, and from $(x, \hat{\rho}(x, y), y) \in \rho$ and $a \supseteq \hat{\rho}(x, y)$ we deduce $(x, a, y) \in \rho$. By a similar argument we can also prove that $(x, a, y) \in \rho$ implies $(x, a, y) \in \tau$, so in the end $\rho = \tau$. We conclude then that the map $\rho \mapsto \hat{\rho}$ is injective. For surjectivity, observe that any $s \in Q\text{Rel}(X, X)$ induces a relation $(x, a, y) \in \rho^s$ iff $a \subseteq s(x, y)$, so that $s = \hat{\rho}^s$. ◀
$$ (\|x_i\|) \cdot (x_1, \dots, x_n) = x_i, $$

$$ (\|r\|) \cdot (x_1, \dots, x_n) = r, $$

$$ (\|\phi(t_1, \dots, t_{\mathrm{ar}(\phi)})\|) \cdot (x_1, \dots, x_n) = \phi((\|t_1\|) \cdot (x_1, \dots, x_n), \dots, (\|t_{\mathrm{ar}(\phi)}\|) \cdot (x_1, \dots, x_n)), $$

$$ (\|t s\|) \cdot (x_1, \dots, x_n) = (\|t\|) \cdot (x_1, \dots, x_n) \cdot ((\|s\|) \cdot (x_1, \dots, x_n)), $$

$$ (\|\lambda x : A. t\|) \cdot (x_1, \dots, x_n) \cdot y = (\|t\|) \cdot (x_1, \dots, x_n, y), $$

$$ (\|fst(t)\|) \cdot (x_1, \dots, x_n) = \text{the first component of } (\|t\|) \cdot (x_1, \dots, x_n), $$

$$ (\|snd(t)\|) \cdot (x_1, \dots, x_n) = \text{the second component of } (\|t\|) \cdot (x_1, \dots, x_n), $$

$$ (\|\langle t, s \rangle\|) \cdot (x_1, \dots, x_n) = ((\|t\|) \cdot (x_1, \dots, x_n), (\|s\|) \cdot (x_1, \dots, x_n)). $$

**Figure 4** Set Theoretic Denotation of Terms.

## B Details of Cartesian Closed Structure

The first projection from $X \times Y$ to $Y$ is given by $(\mathrm{proj}_{X,Y}, \varpi_{X,Y}, \mathrm{proj}_{X,Y})$ consisting of the first projection $\mathrm{proj}_{X,Y}: |X| \times |Y| \to |X|$ and $\varpi_{X,Y}: |X| \times |Y| \to (Q_X \times Q_Y \to Q_X)$ given by $\varpi_{X,Y} \cdot (x, y) \cdot (a, b) = a$. The second projection is given in the same manner. The tupling of $(f, a, f') : Z \to X$ and $(g, b, g') : Z \to Y$ is $(\langle f, g \rangle, \langle a, b \rangle, \langle f', g' \rangle)$ where $\langle f, g \rangle : |Z| \to |X| \times |Y|$ and $\langle a, b \rangle : |Z| \to (Q_Z \to Q_X \times Q_Y)$ are the tupling of $f, g$ and $a, b$ respectively, that is, $\langle f, g \rangle \cdot z$ is defined to be $(f \cdot z, g \cdot z)$, and $\langle a, b \rangle \cdot z \cdot c$ is defined to be $(a \cdot z \cdot c, a \cdot z \cdot c)$. The currying of $(f, a, f') : Z \times X \to Y$ is $(f^\wedge, a^\wedge, f'^\wedge)$ where $f^\wedge : |Z| \to (|X| \Rightarrow |Y|)$ and $f'^\wedge : |Z| \to (|X| \Rightarrow |Y|)$ are the currying of $f : |Z| \times |X| \to |Y|$ and $f' : |Z| \times |X| \to |Y|$, and $a^\wedge : |Z| \to (Q_Z \to Q_{X \to Y})$ is the currying of $a : |Z| \times |X| \to (Q_{Z \times X} \to Q_Y)$, namely, $a^\wedge \cdot z \cdot a \cdot x \cdot b$ is defined to be $a \cdot (z, x) \cdot (a, b)$. The evaluation morphism $(\mathrm{eval}_{X,Y}, \varepsilon_{X,Y}, \mathrm{eval}_{X,Y}) : (X \Rightarrow Y) \times X \to Y$ consists of the evaluation function $\mathrm{eval}_{X,Y} : (|X| \Rightarrow |Y|) \times |X| \to |Y|$ and $\varepsilon_{X,Y}$ is given by $\varepsilon_{X,Y} \cdot (a, b) \cdot (f, x) = a \cdot x \cdot b$.

## C Definitions and Proofs for Section 5

In Figure 4, we define the function $(\|t\|)$ by induction on the type derivation of $t$.

**Proof of Theorem 11.** The triple $((\|t\|), \|t\|, (\|t\|))$ is the interpretation of $\Gamma \vdash t : A$ in the cartesian closed category **Qqm** where we interpret $\Gamma \vdash \phi(t_1, \dots, t_n)$ by

$$ [[A_1]] \times \dots \times [[A_n]] \xrightarrow{\langle [[t_1]], \dots, [[t_n]] \rangle} R \times \dots \times R \xrightarrow{(\phi, \phi^d, \phi)} R. $$

The statement follows from that $((\|t\|), \|t\|, (\|t\|))$ is a morphism from $[[A_1]] \times \dots \times [[A_n]]$ to $[[A]]$ in **Qqm**.

## D Proofs for Section 6

Let us introduce a notation. For a type $A$ and $x \in |A|$, we write $[x] \in Q_A$ for $\hat{\rho}_A(x, x)$, i.e., $[x]$ is equal to $\sup\{a \in Q_A \mid (x, a, x) \in \rho_A\}$. Since $\rho_A$ is closed under supremum, for any $x \in |A|$, we have $(x, [x], x) \in \rho_A$.

**Lemma 22.** For every type $A$ and for every $x, x' \in |A|$, if $(x, [x], x') \in \rho_A$, then $x = x'$.
15:20 On the Metric Nature of (Differential) Logical Relations

**Proof.** By induction on A. It is straightforward to check the case Real and the case A × B.
For the case A ⇒ B, if $(f, [f], f') \in \rho_{A \Rightarrow B}$, then for any $x \in |A|$, we have

$$ (f \cdot x, [f] \cdot x \cdot [x], f' \cdot x) \in \rho_A. $$

Here, by the induction hypothesis,

$$ \begin{aligned} [f] \cdot x \cdot [x] &= \sup\{a \in Q_B \mid \text{for all } (x, [x], x') \in \rho_A, (f \cdot x, a, f \cdot x') \in \rho_B\} \\ &= \sup\{a \in Q_B \mid (f \cdot x, a, f \cdot x) \in \rho_B\} = [f \cdot x]. \end{aligned} $$

Hence, $f' \cdot x = f \cdot x$.

► Lemma 23. For any type A and B, if $f \in |A \Rightarrow B|$ and $x \in |A|$, then $[f] \cdot x \cdot [x] = [f \cdot x]$.

**Proof.** This is shown in the proof of Lemma 22.

► Lemma 24. For every type A, if $(x, a \otimes [x'], x') \in \rho_A$, then $(x, a, x') \in \gamma_A$.

**Proof.** By induction on A. The only non-trivial case is $A \Rightarrow B$. If $(f, a \otimes [f'], f') \in \rho_{A \Rightarrow B}$, then for any $(x, b, x') \in \rho_A$, since $(x, b \lor [x], x) \in \rho_A$, we obtain

$$ (f \cdot x, (a \cdot x \cdot (b \lor [x])) \otimes ([f'] \cdot x \cdot (b \lor [x])), f' \cdot x) \in \rho_B. $$

It follows from monotonicity of a and Lemma 23 that we have

$$ (f \cdot x, (a \cdot x \cdot b) \otimes ([f'] \cdot x \cdot [x]), f' \cdot x) = (f \cdot x, (a \cdot x \cdot b) \otimes [f' \cdot x], f' \cdot x) \in \rho_B. $$

By the induction hypothesis, we conclude $(f \cdot x, a \cdot x \cdot b, f' \cdot x) \in \gamma_B$. For any $(f', b, f') \in \rho_{A \Rightarrow B}$, since $b \subseteq [f']$, it follows from $(f, a \otimes [f'], f') \in \rho_{A \Rightarrow B}$ that $(f, a \otimes b, f') \in \rho_{A \Rightarrow B}$. By left-quasi-reflexivity, we obtain $(f, a \otimes b, f) \in \rho_{A \Rightarrow B}$.

**Proof of Proposition 13.** We first show that $\gamma_A$ is a subset of $\rho_A'$ by induction on A. It is straightforward to check the case Real and the case A × B. We check the case A ⇒ B. Let $(f, a, f')$ be an element of $\gamma_{A \Rightarrow B}$, and let $(f', a', f'')$ be an element of $\rho_{A \Rightarrow B}$. We show that $(f, a \otimes a', f'')$ is an element of $\rho_{A \Rightarrow B}$. For any $(x, b, x') \in \rho_A$, since $(x, b, x) \in \rho_A$, we have

$$ (f \cdot x, a \cdot x \cdot b, f' \cdot x) \in \gamma_B, \quad (f' \cdot x, a' \cdot x \cdot b, f'' \cdot x') \in \rho_B. $$

Hence, by the induction hypothesis, we see that $(f \cdot x, (a \otimes a') \cdot x \cdot b, f'' \cdot x')$ is an element of $\rho_B$. It remains to check that $(f \cdot x, (a \otimes a') \cdot x \cdot b, f \cdot x')$ is an element of $\rho_B$. Since $(f', a', f'') \in \rho_{A \Rightarrow B}$, we have $(f', a', f') \in \rho_{A \Rightarrow B}$. Then, by the definition of $\gamma_{A \Rightarrow B}$, we obtain $(f, a \otimes a', f) \in \rho_{A \Rightarrow B}$. Hence, $(f \cdot x, (a \otimes a') \cdot x \cdot b, f \cdot x')$ is an element of $\rho_B$. We next show that $\rho_A'$ is a subset of $\gamma_A$. Again, it is straightforward to check the case Real and the case A × B. We check the case A ⇒ B. Let $(f, a, f')$ be an element of $\rho_{A \Rightarrow B}$, and let $(x, b, x')$ be an element of $\rho_A$. Since $(f, a \otimes [f'], f') \in \rho_{A \Rightarrow B}$ and $(x, [x], x) \in \rho_A$, we obtain

$$ (f \cdot x, (a \cdot x \cdot [x]) \otimes ([f'] \cdot x \cdot [x]), f' \cdot x) = (f \cdot x, (a \cdot x \cdot [x]) \otimes [f' \cdot x], f' \cdot x) \in \rho_B $$

Hence, by Lemma 24, $(f \cdot x, a \cdot x \cdot [x], f' \cdot x)$ is an element of $\rho_B$. Since a is monotone, for any $(x, b, x') \in \rho_A$, we have $(f \cdot x, a \cdot x \cdot b, f' \cdot x) \in \rho_B$. If $(f', b, f') \in \rho_{A \Rightarrow B}$, then by the definition of $\rho_{A \Rightarrow B}$, we obtain $(f, a \otimes b, f) \in \rho_{A \Rightarrow B}$.
**Proof of Theorem 14.** By the definition of $\gamma_{A\Rightarrow Real}$, we obtain

$$ (f, a \otimes ([f'] \to [f]), f') \in \gamma_{A\Rightarrow Real}. $$

Therefore, it follows from Proposition 13 that

$$ (f, a \otimes ([f'] \to [f]) \otimes [f'], f') \in \rho_{A\Rightarrow Real}. $$

Since $(f, a', f) \in \rho_{A\Rightarrow Real}$ and $(f', a', f') \in \rho_{A\Rightarrow Real}$, we have $a' \subseteq ([f'] \to [f]) \otimes [f']$. Hence, $(f, a \otimes a', f') \in \rho_{A\Rightarrow Real}$. ◀

## E Proofs and Observations for Section 7

**Proof of Proposition 17.** We can check the first clause and the second clause by induction on A. We only prove the third, more delicate, statement. By induction on A, we show that there is a map $\varphi_A: Q_A \times Q_A \Rightarrow Q_A \times Q_A$ such that if $(x, a, z) \in \eta_A$ and $(z, b, y) \in \eta_A$, then $(c_1, c_2) = \varphi_A(a, b)$ satisfies the required conditions. For the base case, we define $\varphi_{Real}(a, b) = (0, a + b)$. For the case $A = (B \Rightarrow C)$, let $(a_1, a_2) \in Q_{B\Rightarrow C} \times Q_{B\Rightarrow C}$ and $(b_1, b_2) \in Q_{B\Rightarrow C} \times Q_{B\Rightarrow C}$ be the greatest decompositions of a and b, respectively. We define $\varphi_{B\Rightarrow C}(a, b)$ by

$$ \varphi_{B\Rightarrow C}(a, b) = (a_1 \otimes k, b_1 \otimes l) $$

where $(k \cdot w \cdot d, l \cdot w \cdot d) = \varphi_C(a_2 \cdot w \cdot d, b_2 \cdot w \cdot d)$. Below, we write $(c_1, c_2)$ for $\varphi_{B\Rightarrow C}(a, b)$. Let us check that $\varphi_{B\Rightarrow C}$ is a witness.

■ We first show that $(z, c_1, z) \in \eta_{B\Rightarrow C}$. For any $(w, d, w') \in \eta_B$, we have

$$ (x \cdot w', a_2 \cdot w \cdot d, z \cdot w') \in \eta_C, \qquad (1) $$

$$ (z \cdot w, b_1 \cdot w \cdot d, z \cdot w') \in \eta_C, \qquad (2) $$

$$ (z \cdot w', b_2 \cdot w \cdot d, y \cdot w') \in \eta_C. \qquad (3) $$

Then, by applying the induction hypothesis to (1) and (3), we obtain

$$ (z \cdot w', k \cdot w \cdot d, z \cdot w') \in \eta_C. \qquad (4) $$

By (2) and (4), we obtain $(z, c_1, z) \in \eta_{B\Rightarrow C}$.

■ We next show that $(x, c_2, y) \in \eta_{B\Rightarrow C}$. For any $(w, d, w') \in \eta_B$, we have

$$ (x \cdot w, a_1 \cdot w \cdot d, x \cdot w') \in \eta_C, \qquad (5) $$

$$ (x \cdot w', a_2 \cdot w \cdot d, z \cdot w') \in \eta_C, \qquad (6) $$

$$ (z \cdot w', b_2 \cdot w \cdot d, y \cdot w') \in \eta_C. \qquad (7) $$

By applying the induction hypothesis to (6) and (7), we obtain

$$ (x \cdot w', l \cdot w \cdot d, y \cdot w') \in \eta_C. \qquad (8) $$

By (5) and (8), we obtain $(x, c_2, y) \in \eta_{B\Rightarrow C}$.

■ Finally, we have

$$ \begin{align*} (c_1 \cdot w \cdot d) \otimes (c_2 \cdot w \cdot d) &= (a_1 \cdot w \cdot d) \otimes (k \cdot w \cdot d) \otimes (b_1 \cdot w \cdot d) \otimes (l \cdot w \cdot d) \\ &\supseteq (a_1 \cdot w \cdot d) \otimes (a_2 \cdot w \cdot d) \otimes (b_1 \cdot w \cdot d) \otimes (b_2 \cdot w \cdot e) \\ &\supseteq (a \cdot w \cdot d) \otimes (b \cdot w \cdot d). \end{align*} $$

<figure><img src="image_5.png" /></figure>
15:22 On the Metric Nature of (Differential) Logical Relations

**Proof of Proposition 18.** The only interesting case is that of a function type A = B ⇒ C. By Proposition 8, $(f, a, f') \in \rho_A^r$ holds iff for all $a \sqsubseteq \hat{q}_A^r(f, f') = \hat{q}_A^r(f, f) \sim \hat{q}_A^r(f, f')$, which is in turn equivalent to $a \otimes \hat{q}_A^r(f, f) \sqsubseteq \hat{q}_A^r(f, f')$. This implies then that $(f, a, f') \in \rho_A^r$ iff for all $(f, b, f) \in \rho_A^r$ (i.e. for all $b \sqsubseteq \hat{q}_A^r(f, f))$, $(f, a \otimes b, f') \in \rho_A^r$ (i.e. $a \otimes b \sqsubseteq \hat{q}_A^r(f, f'))$, that is, iff $(f, a, f') \in \delta_A$. ◀

F Proofs for Section 8

**Proof of Proposition 19.** We prove the statement by induction on A. We only check the case A ⇒ B. It is straightforward to derive “left-quasi-reflexivity” from the definition of $\delta_{A \Rightarrow B}^{\log}$. This is why we modify the definition of differential logical relation given in [11]. For transitivity, we shall show that for any $(t, a, t') \in \delta_A^{\log}$, $(t', a', t'') \in \delta_A^{\log}$ and $(s, b, s') \in \delta_A^{\log}$, we have $(ts, (a+a')bs, t''s') \in \delta_B^{\log}$. By the induction hypothesis, we obtain $(s, b, s) \in \delta_A^{\log}$. Therefore,

$$ (ts, abs, t's) \in \delta_B^{\log}, \quad (t's, a'bs, t''s') \in \delta_B^{\log}. $$

Then, by transitivity of $\delta_B^{\log}$, we obtain $(ts, (a+a')bs, t''s') \in \delta_B^{\log}$. We can prove the fundamental lemma by induction on the derivation of $\Gamma \vdash t : B$. ◀