On the Metric Nature
of (Differential) Logical Relations

Our contributions can be summarized as follows:

• $\mathrm{■}$

  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;

• $\mathrm{■}$

  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;

• $\mathrm{■}$

  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.

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 }_{𝖠}\subseteq 𝖠\times 𝖠$, where $𝖠$ 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:

Typically, one wishes to establish a so-called fundamental lemma, stating that well-typed programs $x:𝖠⊢𝗍:𝖡$ preserve relations. This means that, for any choice of a family of logical relations ${\rho }_{𝖠}$ defined as above, one can prove

Notice that this is equivalent to the instance of reflexivity $(\lambda 𝗑.𝗍,\lambda 𝗑.𝗍)\in {\rho }_{𝖠\Rightarrow 𝖡}$.

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 }_{𝖠}$ and ${\rho }_{𝖡}$ are reflexive and transitive, then ${\rho }_{𝖠\times 𝖡}$ and ${\rho }_{𝖠\Rightarrow 𝖡}$ can be shown reflexive and transitive as well. The case of the function space crucially relies on the fact that all programs of type $𝖠\Rightarrow 𝖡$ must preserve relations (or, in other words, that the fundamental lemma holds): as we observed above, the reflexivity condition $(𝗍,𝗍)\in {\rho }_{𝖠\Rightarrow 𝖡}$ coincides with the fact that the function $𝗍$ is relation-preserving; transitivity, instead, can be proved by combining relation-preservation, the reflexivity of ${\rho }_{𝖠}$ and the transitivity of ${\rho }_{𝖡}$.

Any logical relation $\rho \subseteq 𝖠\times 𝖠$ induces an equivalence ${\equiv }_{\rho }$, called the observational equivalence, where $𝗍{\equiv }_{\rho }𝗎$ iff for all $𝗌\in 𝖠$, $(𝗌,𝗍)\in \rho$ iff $(𝗌,𝗎)\in \rho$. Intuitively, two terms $𝗍,𝗎$ 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 $𝗍{\Rightarrow }^{\ast }𝗏$ produced by terms, one can usually deduce that terms are indistinguishable from their associated values, that is $𝗍{\equiv }_{\rho }𝗏$. In the absence of symmetry, one obtains two observational preorders ${⊑}_{\rho }^l,{⊑}_{\rho }^r\subseteq 𝖠\times 𝖠$ defined by:

These preorders satisfy the following useful and easily provable properties:

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:

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:

Compared to ($\Rightarrow$ ‣ 2), (${\Rightarrow }^{\mathrm{q}}$) includes a second clause $(𝗍𝗌,𝗍{𝗌}^{\prime })\in {\rho }_{𝖡}$ relating the action of $𝗍$ on both $𝗌$ and ${𝗌}^{\prime }$. With this definition, one can easily check that if ${\rho }_{𝖠},{\rho }_{𝖡}$ are quasi-preorders, and the fundamental lemma holds, then ${\rho }_{𝖠\times 𝖡}$ and ${\rho }_{𝖠\Rightarrow 𝖡}$ are quasi-preorders as well.

We now have all elements to discuss what happens when extending logical relations to a quantitative setting. Rather than considering binary relations $\rho \subseteq 𝖠\times 𝖠$ expressing that a certain property holds for two terms $𝗌,𝗍$ or not, we will consider ternary relations $\rho \subseteq 𝖠\times {𝒬}_{𝖠}\times 𝖠$, where $(𝗌,a,𝗍)\in \rho$ indicates that a certain relation holds of $𝗌,𝗍$ to a certain extent, quantified via $a\in {𝒬}_{𝖠}$. Here ${𝒬}_{𝖠}$ 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 {𝒬}_o\times o$ on a ground type can be lifted to a family of binary relations ${\rho }_{𝖠}\subseteq 𝖠\times {𝒬}_{𝖠}\times 𝖠$ over simple types. First, we define, by induction, the quantales ${𝒬}_{𝖠\times 𝖡}={𝒬}_{𝖠}\times {𝒬}_{𝖡}$ and ${𝒬}_{𝖠\Rightarrow 𝖡}=𝖠\Rightarrow ({𝒬}_{𝖠}⇾{𝒬}_{𝖡})$, where ${𝒬}_{𝖠}⇾{𝒬}_{𝖡}$ is the quantale of monotone functions, and $𝖠\Rightarrow {𝒬}_{𝖠}⇾{𝒬}_{𝖡}$ is the quantale of functions from the set of closed terms of type $𝖠$ to ${𝒬}_{𝖠}⇾{𝒬}_{𝖡}$ equipped with the pointwise order. We then define the lifting of ${\rho }_o$ by:

Notice that the definition of ${\rho }_{𝖠\Rightarrow 𝖡}$ closely imitates the clause (${\Rightarrow }^{\mathrm{q}}$) for quasi-preorders. Also observe that the quantale ${𝒬}_{𝖠\Rightarrow 𝖡}$ for the function type is itself a set of functions relating terms of type $𝖠$ and quantities in ${𝒬}_{𝖠}$ with quantities in ${𝒬}_{𝖡}$. 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:𝖠⊢𝗍:𝖡$ and choice of a family of differential logical relations ${\rho }_{𝖠}$ as above, there exists a map ${𝗍}^{\bullet }:𝖠\Rightarrow ({𝒬}_{𝖠}⇾{𝒬}_{𝖡})$ such that

The function ${𝗍}^{\bullet }$ behaves like some sort of derivative of $𝗍$: 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 $(𝒬,+,0,\le )$ of which $0$ is the minimum element. For a differential logical relation $\rho \subseteq 𝖠\times {𝒬}_{𝖠}\times 𝖠$, reflexivity, symmetry and transitivity translate into the following conditions:

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 𝖠\times {𝒬}_{𝖠}\times 𝖠$ gives rise to left and right observational quasi-metrics ${\rho }^l,{\rho }^r:𝖠\times 𝖠\to {𝒬}_{𝖠}$ satisfying properties analogous to those of Proposition 1.

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 reflexivity property is the fundamental lemma; yet, in the framework of differential logical relations, the fundamental lemma produces, for any term $𝗍:𝖠\Rightarrow 𝖡$, the “reflexivity” condition $(𝗍,{𝗍}^{\bullet },𝗍)\in {\rho }_{𝖠\Rightarrow 𝖡}$, which differs from standard reflexivity in that the distance is ${𝗍}^{\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 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 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.

Let us recall that a quantale $𝒬$ is a complete lattice $(𝒬,⊑)$ 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 $𝒬$ is integral (cf. [22], p. 148) when $1=\top$ and commutative when $\otimes$ is commutative. Suppose $𝒬$ is commutative. Given $x,y\in 𝒬$, their residual is defined as $x⊸y:=\bigvee \{z\in 𝒬\mid z\otimes x⊑y\}$ where $⊑$ is the partial order of $𝒬$. Notice that $z⊑x⊸y$ iff $z\otimes x⊑y$, and that $(x⊸y)\otimes x⊑y⊑x⊸(y\otimes x)$. A commutative quantale $𝒬$ is divisible [23] if for all $x,y\in 𝒬$, $x⊑y$ holds iff $y\otimes (y⊸x)=x$. Equivalently, $𝒬$ is divisible iff, whenever $x⊑y$, there exists $z$ such that $x=y\otimes z$. In the following we will use $𝒬$ to refer to a commutative, integral and divisible quantale.

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

The monoidal product $\otimes$ and the residuals $⊸,$ of $𝒬$-relations satisfy properties analogous to residuals in $𝒬$, e.g. $s\otimes (s⊸t)⊑t$, $(ts)\otimes s⊑t$. It is well-known that $𝒬$-relations form a category $𝒬\text{Rel}$ whose objects are sets and such that $𝒬\text{Rel}(X,Y)$ are the $𝒬$-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 ${\mathrm{𝟏}}_X(x,x)=1=\top$ and ${\mathrm{𝟏}}_X(x,y\ne x)=\perp$.

Finally, for any relation $s\in 𝒬\mathrm{𝐑𝐞𝐥}(X,X)$, define the relations ${\mathrm{\Delta }}_{1}s,{\mathrm{\Delta }}_{2}s\in 𝒬\mathrm{𝐑𝐞𝐥}(X,X)$ by ${\mathrm{\Delta }}_{1}s=s\circ \mathrm{\Delta }\circ {\pi }_1$ and ${\mathrm{\Delta }}_{2}s=s\circ \mathrm{\Delta }\circ {\pi }_2$, that is, ${\mathrm{\Delta }}_{1}s(x,y):=s(x,x)$, ${\mathrm{\Delta }}_{2}s(x,y)=s(y,y)$.

For a relation $s\in 𝒬\text{Rel}(X,X)$, reflexivity $s(x,x)=1$ and transitivity $s(x,z)\otimes s(z,y)⊑s(x,y)$ can be written more concisely as $s⊒{\mathrm{𝟏}}_X$ and $s\otimes s⊑s$. A relation $s$ satisfying both such properties is called a quasi-(pseudo)metric (or a hemi-metric) over $X$ (with values in $𝒬$). 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 $𝒬$-relations:

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

Qq-metrics correspond to $𝒬$-relations $s\in 𝒬\mathrm{𝐑𝐞𝐥}(X,X)$ satisfying transitivity $s\otimes s⊑s$ and quasi-reflexivity $s⊑{\mathrm{\Delta }}_{1}s$ (i.e. $s(x,y)⊑s(x,x)$). From transitivity, we deduce that, for a qq-metric $s$, both $s^l,s^r⊒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:

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)⊒p(x,y)$. However, unlike the qq-metrics just discussed, PQMs satisfy a stronger transitivity condition. When $𝒬=[0,+\mathrm{\infty }]$ is the Lawvere quantale, this condition reads as

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

Define the relations ${\mathrm{\Theta }}_s^l,{\mathrm{\Theta }}_s^r\in 𝒬\mathrm{𝐑𝐞𝐥}(X,X)$ by ${\mathrm{\Theta }}_s^l(x,y)=s(y,y)⊸s(x,y)$ and ${\mathrm{\Theta }}_s^r(x,y)=s(x,x)⊸s(x,y)$. A PQM can be thus more concisely be defined as a relation $s\in 𝒬\mathrm{𝐑𝐞𝐥}(X,X)$ satisfying $s⊑{\mathrm{\Delta }}_{1}s$ and $s\otimes {\mathrm{\Theta }}_s^r⊑s$. Notice that strong transitivity $s\otimes {\mathrm{\Theta }}_s^r⊑s$ looks similar to the right transitivity $s\otimes q_s^r⊑s$. Indeed, the following result relates the relations ${\mathrm{\Theta }}_s^c$ and $s^c$:

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 ${\mathrm{\Theta }}_s^r(x,y)=s(x,x)⊸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)⊑p(x,y)$). Nevertheless, we will show in Section 7 how one can capture PQMs via a suitable family of logical relations.

While in the previous section we discussed $𝒬$-relations, that is, binary relations valued in a quantale $𝒬$, the theory of differential logical relations is expressed in terms of ternary relations $\rho \subseteq X\times 𝒬\times X$. In fact, any such relation $\rho \subseteq X\times 𝒬\times X$ induces a $𝒬$-relation $\widehat{\rho }\in 𝒬\mathrm{𝐑𝐞𝐥}(X,X)$ defined by

Intuitively, $\widehat{\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 𝒬\times X$ be said to be $𝒬$-closed when the following hold:

• $\mathrm{■}$

  $(x,a,y)\in \rho$ and $a^{\prime }⊑a$ implies $(x,a^{\prime },y)\in \rho$;

• $\mathrm{■}$

  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 $𝒬$-closedness to derive results in Section 6.

In Appendix A (Lemma 21), we show that the map $\rho \mapsto \widehat{\rho }$ defines a bijection between the $𝒬$-closed relations $\rho \subseteq X\times 𝒬\times X$ and $𝒬\mathrm{𝐑𝐞𝐥}(X,X)$. In the sequel, we will identify metrics with their corresponding $𝒬$-closed relations.

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 $𝒬$ and $ℛ$, we denote the set of monotone functions from $𝒬$ to $ℛ$ by $𝒬⇾ℛ$. 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 $\mathrm{𝐐𝐪𝐦}$ of qq-metrics is defined as follows:

• $\mathrm{■}$

  objects are triples $X=({𝒬}_X,|X|,{\rho }_X)$ consisting of a quantale ${𝒬}_X$, a set $|X|$ and a qq-metric ${\rho }_X\subseteq |X|\times {𝒬}_X\times |X|$;

• $\mathrm{■}$

  morphisms from $X$ to $Y$ are triples $(f,a,f^{\prime })$ consisting of functions $f,f^{\prime }:|X|\to |Y|$ and $a:|X|\to ({𝒬}_X⇾{𝒬}_Y)$ such that for all $(x,b,x^{\prime })\in {\rho }_X$, we have $(f\cdot x,a\cdot x\cdot b,f^{\prime }\cdot x^{\prime })\in {\rho }_Y$ and $(f\cdot x,a\cdot x\cdot b,f\cdot x^{\prime })\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 ({𝒬}_X⇾{𝒬}_X)$ given by $i_X\cdot x\cdot a=a$. The composition of $(f,a,f^{\prime }):X\to Y$ and $(g,b,g^{\prime }):Y\to Z$ is $(g\circ f,c,g^{\prime }\circ f^{\prime })$ where $c:|X|\to ({𝒬}_X⇾{𝒬}_Z)$ is given by $c\cdot x=(b\cdot (f\cdot x))\circ (a\cdot x)$.

The cartesian closed structure closely matches the construction of differential logical relations in Section 2. The terminal object $\top$ is $(\{\ast \},\{\ast \},{\rho }_{\top })$ where ${\rho }_{\top }=\{(\ast ,\ast ,\ast )\}$, and the product of $X$ and $Y$ is $X\times Y=({𝒬}_X\times {𝒬}_Y,|X|\times |Y|,{\rho }_{X\times Y})$, where ${\rho }_{X\times Y}$ is given by

The exponential $X\Rightarrow Y$ is given by $(|X|\Rightarrow ({𝒬}_X⇾{𝒬}_Y),|X|\Rightarrow |Y|,{\rho }_{X\Rightarrow Y})$ where

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

Our language ${\mathrm{\Lambda }}_{\mathrm{𝖱𝖾𝖺𝗅}}$ comprises a type of real numbers and first order functions on $ℝ$. Let $\mathrm{𝖵𝖺𝗋}$ be a countably infinite set of variables. We define types and terms as follows:

Here, $r$ varies over $ℝ$, and $\varphi$ varies over the set of multi-arity functions on $ℝ$, namely, $\varphi$ is a function from ${ℝ}^n$ to $ℝ$ for some $n\in \mathbb{N}$. We call $n$ the arity of $\varphi$, and we denote the arity of $\varphi$ by $\mathrm{ar}(\varphi )$. We adopt the standard typing rules given in Figure 1. Below, we denote the set of types by $\mathrm{𝐓𝐲𝐩𝐞}$ and the set of closed terms of type $𝖠$ by ${𝐓}_{𝖠}$.

We denote the standard set theoretic interpretation of ${\mathrm{\Lambda }}_{\mathrm{𝖱𝖾𝖺𝗅}}$ by $⦇-⦈$. (See [25] for example.) To be concrete, the interpretation $⦇𝖠⦈$ of a type $𝖠$ is a set inductively defined by

and we interpret a term ${𝗑}_1:{𝖠}_1,\mathrm{\dots },{𝗑}_n:{𝖠}_n⊢𝗍:𝖡$ as a function $⦇𝗍⦈$ from $⦇{𝖠}_1⦈\times \mathrm{\cdots }\times ⦇{𝖠}_n⦈$ to $⦇𝖡⦈$. We give the definition of $⦇𝗍⦈$ in Appendix C.

We inductively define a qq-metric space $⟦𝖠⟧$ by

Here, $R$ is the qq-metric given in Example 10. Below, we simply denote the structure of an object $⟦𝖠⟧$ by $({𝒬}_{𝖠},|𝖠|,{\rho }_{𝖠})$. It is straightforward to check that for every type $𝖠$, we have $|𝖠|=⦇𝖠⦈$. The qq-metrics $⟦𝖠⟧$ are the categorical interpretation of types $𝖠$, and the following fundamental lemma is derived from the categorical interpretation of ${\mathrm{\Lambda }}_{\mathrm{𝖱𝖾𝖺𝗅}}$-terms in $\mathrm{𝐐𝐪𝐦}$.

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