Ugo Dal

Francesco Gavazzo
email: francesco.gavazzo@gmail.com

Akira Yoshimizu
email: akiray@bp.iij4u.or.jp

Differential Logical Relations Part I: The Simply-Typed Case

Keywords: 2012 ACM Subject Classification Computability → Lambda calculus; Logic → Equational Logic and Rewriting Keywords and phrases Logical Relations λ-Calculus Program Equivalence Semantics, Digital Object Identifier 10, 4230/LIPIcs, ICALP, 2019, XXX

We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between terms not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity, i.e. the type, of the compared terms. We exemplify this concept in the simply-typed lambda-calculus, and show a form of soundness theorem. We also see how ordinary logical relations and metric relations can be seen as instances of differential logical relations. Finally, we show that differential logical relations can be organised in a cartesian closed category, contrarily to metric relations, which are well-known not to have such a structure, but only that of a monoidal closed category.

Introduction

Modern software systems tend to be heterogeneous and complex, and this is reflected in the analysis methodologies we use to tame their complexity. Indeed, in many cases the only way to go is to make use of compositional kinds of analysis, in which parts of a large system can be analysed in isolation, without having to care about the rest of the system, the environment. As an example, one could consider a component A and replace it with another (e.g. more efficient) component B without looking at the context C in which A and B are supposed to operate, see Figure 1. Of course, for this program transformation to be safe, A should be equivalent to B or, at least, B should be a refinement of A.

Program equivalences and refinements, indeed, are the cruxes of program semantics, and have been investigated in many different programming paradigms. When programs have an interactive behaviour, like in concurrent or higher-order languages, even defining a notion of program equivalence is not trivial, while coming out with handy methodologies for proving concrete programs to be equivalent can be quite challenging, and has been one of the major research topics in programming language theory, stimulating the development of techniques like logical relations [START_REF] Plotkin | Lambda-definability and logical relations[END_REF][START_REF] Mitchell | Foundations for Programming Languages[END_REF], applicative bisimilarity [START_REF] Abramsky | The lazy lambda calculus[END_REF], and to some extent denotational semantics [26,[START_REF] Scott | Toward a mathematical semantics for computer languages[END_REF] itself.

B C A ⇓ C Figure 1 Repla- cing A with B.
Coming back to our example, may we say anything about the case in which A and B are not equivalent, although behaving very similarly? Is there anything classic program semantics can say about this situation?

Actually, the answer is negative: the program transformation turning such an A into B cannot be justified, simply because there is no guarantee about what the possible negative effects that turning A into B could have on the overall system formed by C and A. There are, however, many cases in which program transformations like the one we just described are indeed of interest, and thus desirable. Many examples can be, for instance, drawn from the field of approximate computing [START_REF] Mittal | A survey of techniques for approximate computing[END_REF], in which equivalence-breaking program transformations are considered as beneficial provided the overall behaviour of the program is not affected too much by the transformation, while its intensional behaviour, e.g. its performance, is significantly improved.

One partial solution to the problem above consists in considering program metrics rather than program equivalences. This way, any pair of programs are dubbed being at a certain numerical distance rather than being merely equivalent (or not). This, for example, can be useful in the context of differential privacy [START_REF] Reed | Distance makes the types grow stronger: a calculus for differential privacy[END_REF][START_REF] Barthe | Programming language techniques for differential privacy[END_REF][START_REF] Xu | Metrics for differential privacy in concurrent systems[END_REF] and has also been studied in the realms of domain theory [START_REF] De Amorim | A semantic account of metric preservation[END_REF][START_REF] Baier | Denotational semantics in the CPO and metric approach[END_REF][START_REF] De Bakker | Denotational semantics of concurrency[END_REF][START_REF] Escardo | A metric model of pcf[END_REF][START_REF] Arnold | Metric interpretations of infinite trees and semantics of non deterministic recursive programs[END_REF] (see also [START_REF] Van Breugel | An introduction to metric semantics: operational and denotational models for programming and specification languages[END_REF] for an introduction to the subject) and coinduction [START_REF] Van Breugel | Towards quantitative verification of probabilistic transition systems[END_REF][START_REF] Van Breugel | A behavioural pseudometric for probabilistic transition systems[END_REF][START_REF] Desharnais | Metrics for labelled markov processes[END_REF][START_REF] Chatzikokolakis | Generalized bisimulation metrics[END_REF]. The common denominator among all these approaches is that on the one hand, the notion of a congruence, crucial for compositional reasoning, is replaced by the one of a Lipschitz-continuous map: any context should not amplify (too much) the distance between any pair of terms, when it is fed with either the former or the latter:

δ(C[M ], C[N ]) ≤ c • δ(M , N ).
This enforces compositionality, and naturally leads us to consider metric spaces and Lipschitz functions as the underlying category. As is well known, this is not a cartesian closed category, and thus does not form a model of typed λ-calculi, unless one adopts linear type systems, or type systems in which the number of uses of each variable is kept track of, like FUZZ [START_REF] Reed | Distance makes the types grow stronger: a calculus for differential privacy[END_REF]. This somehow limits the compositionality of the metric approach [START_REF] De Amorim | A semantic account of metric preservation[END_REF][START_REF] Gavazzo | Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances[END_REF].

Even if one considers affine calculi, there are program transformations which are intrinsically unjustifiable in the metric approach. Consider the following two programs of type

REAL → REAL M SIN := λx.sin(x) M ID := λx.x.
The two terms compute two very different functions on the real numbers, namely the sine trigonometric function and the identity on R, respectively. The euclidean distance | sin x -x | is unbounded when x ranges over R. As a consequence, comparing M SIN and M ID using the so-called sup metric1 as it is usually done in metric logical relations [START_REF] Reed | Distance makes the types grow stronger: a calculus for differential privacy[END_REF][START_REF] De Amorim | A semantic account of metric preservation[END_REF] and applicative distances [START_REF] Gavazzo | Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances[END_REF][START_REF] Crubillé | Metric reasoning about λ-terms: The affine case[END_REF], we see that their distance is infinite, and that the program transformation turning M SIN into M ID cannot be justified this way, for very good reasons. As highlighted by Westbrook and Chaudhuri [START_REF] Westbrook | A semantics for approximate program transformations[END_REF], this is not the end of the story, at least if the environment in which M SIN and M ID operate feed either of them only with real numbers close to 0. If this is the case, M SIN can be substituted with M ID without affecting too much the overall behaviour of the system.

The key insight by Westbrook and Chaudhuri is that justifying program transformations like the one above requires taking the difference δ(M SIN , M ID ) between M SIN and M ID not merely as a number, but as a more structured object. What they suggest is to take δ(M SIN , M ID ) as yet another program, which however describes the difference between M SIN and M ID :

δ(M SIN , M ID ) := λx.λε.| sin x -x| + ε.
This reflects the fact that the distance between M SIN and M ID , namely the discrepancy between their output, depends not only on the discrepancy on the input, namely on ε, but also on the input itself, namely on x. It both x and ε are close to 0, δ(M SIN , M ID ) is itself close to 0.

In this paper, we develop Westbrook and Chaudhuri's ideas, and turn them into a framework of differential logical relations. We will do all this in a simply-typed λ-calculus with real numbers as the only base type. Starting from such a minimal calculus has at least two advantages: on the one hand one can talk about meaningful examples like the one above, and on the other hand the induced metatheory is simple enough to highlight the key concepts.

The contributions of this paper can be summarised as follows:

After introducing our calculus ST λ R , we define differential logical relations inductively on types, as ternary relations between pairs of programs and differences. The latter are mere set theoretic entities here, and the nature of differences between terms depends on terms' types.

We prove a soundness theorem for differential logical relations, which allows us to justify compositional reasoning about terms' differences. We also prove a finite difference theorem, which stipulates that the distance between two simply-typed λ-terms is finite if mild conditions hold on the underlying set of function symbols.

We give embeddings of logical and metric relations into differential logical relations. This witnesses that the latter are a generalisation of the former two.

Finally, we show that generalised metric domains, the mathematical structure underlying differential logical relations, form a cartesian closed category, contrarily to the category of metric spaces, which is well known not to have the same property.

Due to space constraints, many details have to be omitted, but can be found in an Extended Version of this work [START_REF] Dal Lago | Differential logical relations, Part I: The simply-typed case (extended version)[END_REF].

A Simply-Typed λ-Calculus with Real Numbers

In this section, we introduce a simply-typed λ-calculus in which the only base type is the one of real numbers, and constructs for iteration and conditional are natively available.

The choice of this language as the reference calculus in this paper has been made for the sake of simplicity, allowing us to concentrate on the most crucial aspects, at the same time guaranteeing a minimal expressive power.

I C A L P 2 0 1 9 Γ π2 : τ × ρ → ρ Γ M : τ Γ N : τ Γ iflz M else N : REAL → τ Γ M : τ → τ Γ N : τ Γ iter M base N : REAL → τ

Terms and Types

ST λ R is a typed λ-calculus, so its definition starts by giving the language of types, which is defined as follows:

τ , ρ ::

= REAL τ → ρ τ × ρ.
The expression

τ n stands for τ × • • • × τ n times
. The set of terms is defined as follows:

M , N ::= x r f n λx.M M N M , N π 1 | π 2 iflz M else N iter M

Call-by-Value Operational Semantics

A static semantics is of course not enough to give meaning to a paradigmatic programming language, the dynamic aspects being captured only once an operational semantics is defined. The latter turns out to be very natural. Values are defined as follows:

V , W ::= r f n λx.M M , N π 1 π 2 iflz M else N iter M base N
The set of closed values of type τ is CV (τ ) ⊆ CT (τ ), and the evaluation of M ∈ CT (τ ) produces a value V ∈ CV (τ ), as formalised by the rules in Figure 3, through the judgment

M ⇓ V . We write M ⇓ if M ⇓ V is derivable for some V .
The absence of full recursion has the nice consequence of guaranteeing a form of termination: Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu XXX:5

Theorem 1. The calculus ST λ R is terminating: if • M : τ then M ⇓.
V ⇓ V M ⇓ fn N ⇓ L1, . . . , Ln L i ⇓ r i M N ⇓ f (r1, . . . , rn) M ⇓ λx.L N ⇓ V L{V /x} ⇓ W M N ⇓ W M ⇓ π1 N ⇓ L, P L ⇓ V M N ⇓ V M ⇓ π2 N ⇓ L, P P ⇓ V M N ⇓ V M ⇓ iflz L else P N ⇓ r r < 0 L ⇓ V M N ⇓ V M ⇓ iflz L else P N ⇓ r r ≥ 0 P ⇓ V M N ⇓ V M ⇓ iter L base P N ⇓ r r < 0 P ⇓ V M N ⇓ V M ⇓ iter L base P N ⇓ r r ≥ 0 L((iter L base P )(pred 1 (r)) ⇓ V M N ⇓ V Figure 3 Operational semantics for ST λ R .

Context Equivalence

A context C is
C such that ∅ C[Γ • : τ ] : REAL it holds that NF (C[M ]) = NF (C[N ]).
Context equivalence is the largest adequate congruence, and is thus considered as the coarsest "reasonable" equivalence between terms. It can also be turned into a pseudometric [START_REF] Crubillé | Metric reasoning about λ-terms: The general case[END_REF][START_REF] Crubillé | Metric reasoning about λ-terms: The affine case[END_REF] called context distance -by stipulating that

δ(M , N ) = sup ∅ C[Γ •:τ ]:REAL |NF (C[M ]) -NF (C[M ])|.
The obtained notion of distance, however, is bound to trivialise [START_REF] Crubillé | Metric reasoning about λ-terms: The general case[END_REF], given that ST λ R is not affine. Trivialisation of context distance highlights an important limit of the metric approach to program difference which, ultimately, can be identified with the fact that program distances are sensitive to interactions with the environment. Our notion of a differential logical relation tackles such a problem from a different perspective, namely refining the concept of program distance which is not just a number, but is now able to take into account interactions with the environment.

Set-Theoretic Semantics

Before introducing differential logical relations, it is useful to remark that we can give ST λ R a standard set-theoretic semantics. To any type τ we associate the set τ , the latter being defined by induction on the structure of τ as follows:

REAL = R; τ → ρ = τ → ρ ; τ × ρ = τ × ρ .
This way, any closed term M ∈ CT (τ ) is interpreted as an element M of τ in a natural way (see, e.g. [START_REF] Mitchell | Foundations for Programming Languages[END_REF]). Up to now, everything we have said about ST λ R is absolutely standard, and only serves to set the stage for the next sections.

Making Logical Relations Differential

Logical relations can be seen as one of the many ways of defining when two programs are to be considered equivalent. Their definition is type driven, i.e., they can be seen as a family I C A L P 2 0 1 9 XXX:6 Differential Logical Relations {δ τ } τ of binary relations indexed by types such that δ τ ⊆ CT (τ ) × CT (τ ). This section is devoted to showing how all this can be made into differential logical relations.

The first thing that needs to be discussed is how to define the space of differences between programs. These are just boolean values in logical relations, become real numbers in ordinary metrics, and is type-dependent itself. A function • that assigns a set to each type is defined as follows:

REAL = R ∞ ≥0 ; τ → ρ = τ × τ → ρ ; τ × ρ = τ × ρ ;
where R ∞ ≥0 = R ≥0 ∪ {∞}. The set τ is said to be the difference space for the type τ and is meant to model the outcome of comparisons between closed programs of type τ . As an example, when τ is REAL → REAL, we have that

τ = R × R ∞ ≥0 → R ∞ ≥0
. This is the type of the function δ(M , N ) we used to compare the two programs described in the Introduction.

Now, which structure could we endow τ with? First of all, we can define a partial order ≤ τ over τ for each type τ as follows:

r ≤ REAL s if r ≤ s as the usual order over R ∞ ≥0 ; f ≤ τ →ρ g if ∀x ∈ τ .∀t ∈ τ .f (x, t) ≤ ρ g(x, t); (t, u) ≤ τ ×ρ (s, r) if t ≤ τ s and u ≤ ρ r.
This order has least upper bounds and greater lower bounds, thanks to the nice structure of

R ∞ ≥0 :
Proposition 3. For each type τ , ( τ , ≤ τ ) forms a complete lattice.

The fact that τ has a nice order-theoretic structure is not the end of the story. For every type τ , we define a binary operation * τ as follows:

r * REAL s = r + s if r, s ∈ R ≥0 ; (f * τ →ρ g)(V , t) = f (V , t) * ρ g(V , t); r * REAL s = ∞ if r = ∞ ∨ s = ∞; (t, s) * τ ×ρ (u, r) = (t * τ u, s * ρ r).
This is precisely what it is needed to turn τ into a quantale 2 [START_REF] Rosenthal | Quantales and their applications[END_REF].

Proposition 4. For each type τ , τ forms a commutative unital non-idempotent quantale.

The fact that τ is a quantale means that it has, e.g., the right structure to be the codomain of generalised metrics [START_REF] Lawvere | Metric spaces, generalized logic, and closed categories[END_REF][START_REF] Hofmann | Monoidal Topology. A Categorical Approach to Order, Metric, and Topology[END_REF]. Actually, a more general structure is needed for our purposes, namely the one of a generalised metric domain, which will be thoroughly discussed in Section 6 below. For the moment, let us concentrate our attention to programs:

Definition 5 (Differential Logical Relations). We define a differential logical relation {δ τ ⊆ Λ τ × τ × Λ τ } τ as a set of ternary relations indexed by types satisfying

δ REAL (M , r, N ) ⇔ |NF (M ) -NF (N )| ≤ r; δ τ ×ρ (M , (d 1 , d 2 ), N ) ⇔ δ τ (π 1 M , d 1 , π 1 N ) ∧ δ ρ (π 2 M , d 2 , π 2 N ) δ τ →ρ (M , d, N ) ⇔ (∀V ∈ CV (τ ). ∀x ∈ τ . ∀W ∈ CV (τ ). δ τ (V , x, W ) ⇒ δ ρ (M V , d( V , x), N W ) ∧ δ ρ (M W , d( V , x), N V )).
An intuition behind the condition required for δ τ →ρ (M , d, N ) is that d( V , x) overapproximates both the "distance" between M V and N W and the one between M W and N V , this whenever W is within the error x from V .

2 Recall that a quantale

Q = (Q, ≤ Q , 0 Q , * Q ) consists of a complete lattice (Q, ≤ Q ) and a monoid (Q, 0 Q , * Q
) such that the lattice and monoid structures properly interact (meaning that monoid multiplication distributes over joins). We refer to [START_REF] Rosenthal | Quantales and their applications[END_REF][START_REF] Hofmann | Monoidal Topology. A Categorical Approach to Order, Metric, and Topology[END_REF] for details.

Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu XXX:7

A Fundamental Lemma

Usually, the main result about any system of logical relations is the so-called Fundamental Lemma, which states that any typable term is in relation with itself. But how would the Fundamental Lemma look like here? Should any term be at somehow minimal distance to itself, in the spirit of what happens, e.g. with metrics [START_REF] Reed | Distance makes the types grow stronger: a calculus for differential privacy[END_REF][START_REF] De Amorim | A semantic account of metric preservation[END_REF]? Actually, there is no hope to prove anything like that for differential logical relations, as the following example shows.

Example 6. Consider again the term M ID = λx.x, which can be given type

τ = REAL → REAL in the empty context. Please recall that τ = R × R ∞ ≥0 → R ∞ ≥0 . Could we prove that δ τ (M ID , 0 τ , M ID )
, where 0 τ is the constant-0 function? The answer is negative: given two real numbers r and s at distance ε, the terms M ID r and M ID s are themselves ε apart, thus at nonnull distance. The best one can say, then, is that δ τ (M ID , f , M ID ), where f (x, ε) = ε.

As the previous example suggests, a term M being at self-distance d is a witness of M being sensitive to changes to the environment according to d. Indeed, the only terms which are at self-distance 0 are the constant functions. This makes the underlying theory more general than the one of logical or metric relations, although the latter can be proved to be captured by differential logical relations, as we will see in the next section.

Coming back to the question with which we opened the section, we can formulate a suitable fundamental lemma for differential logical relations.

Theorem 7 (Fundamental Lemma, Version I). For every

• M : τ there is a d ∈ τ such that (M , d, M ) ∈ δ τ .
Proof sketch. The proof proceeds, as usual, by induction on the derivation of • M : τ . In order to deal with e.g. λ-abstractions we have to strengthen our statement taking into account open terms. This turned out to be non-trivial and requires to extend our notion of a differential logical relation to arbitrary terms. First of all, we need to generalise • and • to environments. For instance, Γ is the set of families in the form α = {α x } (x:ρ)∈Γ , where α x ∈ ρ . Similarly for Γ . This way, a natural space for differences between terms Γ M , N : τ can be taken as τ Γ × Γ , namely the set of maps from Γ × Γ to τ . Given an environment Γ, a family V = {V x } (x:ρx)∈Γ such that V x ∈ CV (ρ x ) is said to be a Γ-family of values. Such a Γ-family of values can naturally be seen as a substitution V mapping each variable (x : ρ) ∈ Γ to V x ∈ CV (ρ x ). As it is customary, for a term Γ M : τ we write M V for the closed term of type τ obtained applying the substitution V to M . We denote by CV (Γ) the set of all Γ-family of values. Given a set Z, an environment Γ, and two Γ-indexed families α = {α x } (x:ρ)∈Γ , β = {β x } (x:ρ)∈Γ over Z (meaning that e.g. α x ∈ Z, for each (x : ρ) ∈ Γ), we introduce the following notational convention. For a Γ-indexed family B = {b x } (x:ρ)∈Γ such that b x ∈ {0, 1}, we can construct a 'choice' Γ-indexed family B α β as follows:

(B α β ) x = α x if b x = 0 β x if b x = 1.
Moreover, given a family B as above, we can construct the inverse family B as the family {1 -b x } (x:ρ)∈Γ . We can now talk about open terms, and from a differential logical relation

{δ τ ⊆ Λ τ × τ × Λ τ } τ construct a family of relations {δ Γ τ ⊆ Λ Γ τ × τ Γ × Γ × Λ Γ τ } τ ,Γ by stipulating that δ Γ τ (M , d, N ) iff δ Γ (V, Y , W) =⇒ ∀B ∈ {0, 1} Γ .δ τ (M B V W , d( V , Y ), N B V W
). We now prove the following strengthening of our main thesis: for any term Γ M : τ , there In the realm of differential logical relations, the Fundamental Lemma plays a similar role, although with a different, quantitative flavor: once C has been proved sensitive to changes according to d, and V , W are proved to be at distance e, then, e.g., the impact of substituting V with W in C can be measured by composing d and e (and V ), i.e. by computing d( V , e). Notice that the sensitivity analysis on C and the relational analysis on V and W are decoupled. What the Fundamental Lemma tells you is that d can always be found.

is a d ∈ τ Γ × Γ such that δ Γ τ (M ,

Our Running Example, Revisited

It is now time to revisit the example we talked about in the Introduction. Consider the following two programs, both closed and of type REAL → REAL:

M SIN = λx.sin 1 (x); M ID = λx.x.
First of all, let us observe that, as already remarked, comparing M SIN and M ID using the sup metric on R → R, as it is done in metric logical relations and applicative distances, The fact that |sin s -sin r| ≤ |s -r| is a consequence of sin being 1-Lipschitz continuous (see, e.g., [START_REF] Dal Lago | Differential logical relations, Part I: The simply-typed case (extended version)[END_REF] for a simple proof). Now, consider a context C which makes use of either M SIN or M ID by feeding them with a value close to 0, call it θ. Such a context could be, e.g., C = (λx.x(xθ)) [•]. C can be seen as a term having type τ = (REAL → REAL) → REAL. A self-distance d for C can thus be defined as an element of h(θ,0)). This allows for compositional reasoning about program distances: the overall impact of replacing M SIN by M ID can be evaluated by computing

τ = REAL → REAL × REAL → REAL → R ∞ ≥0 . namely F = λ λ g, h .h(g(θ),
F ( M SIN , f ).

Of course the context C needs to be taken into account, but once and for all:

the functional F can be built without knowing with which term(s) it will be fed with. any access to either M SIN or M ID .

Logical and Metric Relations as DLRs

The previous section should have convinced the reader about the peculiar characteristics of differential logical relations compared to (standard) metric and logical relations. In Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu XXX:9

this section we show that despite the apparent differences, logical and metric relations can somehow be retrieved as specific kinds of program differences. This is, however, bound to be nontrivial. The naïve attempt, namely seeing program equivalence as being captured by minimal distances in logical relations, fails: the distance between a program and itself can be nonnull.

How should we proceed, then? Isolating those distances which witness program equivalence is indeed possible, but requires a bit of an effort. In particular, the sets of those distances can be, again, defined by induction on τ . For every τ , we give τ 0 ⊆ τ by induction on the structure of τ :

REAL 0 = {0}; τ × ρ 0 = τ 0 × ρ 0 ; τ → ρ 0 = {f ∈ τ → ρ | ∀x ∈ τ .∀y ∈ τ 0 .f (x, y) ∈ ρ 0 }.
Notice that τ → ρ 0 is not defined as τ × τ 0 → ρ 0 (doing so would violate τ → ρ 0 ⊆ τ → ρ ). The following requires some effort, and testifies that, indeed, program equivalence in the sense of logical relations precisely corresponds to being at a distance in τ 0 : Theorem 8. Let {L τ } τ be a logical relation. There exists a differential logical relation

{δ τ } τ satisfying L τ (M , N ) ⇐⇒ ∃d ∈ τ 0 .δ τ (M , d, N ).
What if we want to generalise the argument above to metric relations, as introduced, e.g., by Reed and Pierce [START_REF] Reed | Distance makes the types grow stronger: a calculus for differential privacy[END_REF]? The set τ 0 becomes a set of distances parametrised by a single real number:

REAL r = {r}; τ × ρ r = τ r × ρ r ; τ → ρ r = {f ∈ τ → ρ | ∀x ∈ τ .∀y ∈ τ s .f (x, y) ∈ ρ r+s }.
A result similar to Theorem 8 is unfortunately outside the scope of this paper, but can be found in the Extended Version [START_REF] Dal Lago | Differential logical relations, Part I: The simply-typed case (extended version)[END_REF]. In particular, metric relations are only available in calculi, like FUZZ [START_REF] Reed | Distance makes the types grow stronger: a calculus for differential privacy[END_REF], which rely on linear type systems, thus more refined than the one we endow ST λ R with.

Strengthening the Fundamental Theorem through Finite Distances

Let us now ask ourselves the following question: given any term M ∈ CT (τ ), what can we say about its sensitivity, i.e., about the values d ∈ τ such that δ τ (M , d, M )? Two of the results we have proved about ST λ R indeed give partial answers to the aforementioned question. On the one hand, Theorem 7 states that such a d can always be found. On the other hand, Theorem 8 tells us that such a d can be taken in τ 0 . Both these answers are not particularly informative, however. The mere existence of such a d ∈ τ , for example, is trivial since d can always be taken as d ∞ , the maximal element of the underlying quantale.

The fact that such a d can be taken from τ 0 tells us that, e.g. when τ = ρ → ξ, M returns equivalent terms when fed with equivalent arguments: there is no quantitative guarantee about the behaviour of the term when fed with non-equivalent arguments.

Is this the best one can get about the sensitivity of ST λ R terms? The absence of full recursion suggests that we could hope to prove that infinite distances, although part of the underlying quantale, can in fact be useless. In other words, we are implicitly suggesting that self-distances could be elements of τ <∞ ⊂ τ , defined as follows:

REAL <∞ = R ≥0 ; τ × ρ <∞ = τ <∞ × ρ <∞ ; τ → ρ <∞ = {f ∈ τ → ρ | ∀x ∈ τ .∀t ∈ τ <∞ .f (x, t) ∈ ρ <∞ }.
I C A L P 2 0 1 9

XXX:10 Differential Logical Relations

Please observe that τ <∞ is in general a much larger set of differences than r∈R ∞ ≥0 τ r : the former equals the latter only when τ is REAL. Already when τ is REAL → REAL, the former includes, say, functions like f (r, ε) = (r + ε) 2 , while the latter does not.

Figure 4 A total, but highly discontinuous, function.

Unfortunately, there are terms in ST λ R which cannot be proved to be at self-distance in τ <∞ , and, surprisingly, this is not due to the higher-order features of ST λ R , but to {F n } n∈N being arbitrary, and containing functions which do not map finite distances to finite distances, like

h(r) = 0 if r = 0 1 r
otherwise (see Figure 4). Is this phenomenon solely responsible for the necessity of finite self-distances in ST λ R ? The answer is positive, and the rest of this section is devoted precisely to formalising and proving the aforementioned conjecture.

First of all, we need to appropriately axiomatise the absence of unbounded discontinuities from {F n } n∈N . A not-so-restrictive but sufficient axiom turns out to be weak boundedness: a function f n : R n → R is said to be weakly bounded if and only if it maps bounded subsets of R n into bounded subsets of R. As an example, the function h above is not weakly bounded, because h

([-ε, ε]) is -∞, - 1 ε ∪ {0} ∪ 1 ε , ∞
which is unbounded for any as ε > 0. Any term M is said to be weakly bounded iff any function symbol f n occurring in M is itself weakly bounded. Actually, this is precisely what one needs to get the strengthening of the Fundamental Theorem we are looking for.

Theorem 9 (Fundamental Theorem, Version II). For any weakly bounded term

• M : τ , there is d ∈ τ <∞ such that (M , d, M ) ∈ δ τ .
The reader may have wondered about how restrictive a condition weak boundedness really is. In particular, whether it corresponds to some form of continuity. In fact, the introduced condition only rules out unbounded discontinuities. In other words, weak boundedness can be equivalently defined by imposing local boundedness at any point in the domain R. This is weaker than asking for boundedness, which requires the existence of a global bound.

A Categorical Perspective

Up to now, differential logical relations have been treated very concretely, without looking at them through the lens of category theory. This is in contrast to, e.g., the treatment of metric relations from [START_REF] De Amorim | A semantic account of metric preservation[END_REF], in which soundness of metric relations for FUZZ is obtained as a byproduct of a proof of symmetric monoidal closedness for the category MET of pseudometric spaces and Lipschitz functions.

But what could take the place of pseudometric spaces in a categorical framework capturing differential logical relations? The notion of a metric needs to be relaxed along at least two axes. On the one hand, the codomain of the "metric" δ is not necessarily the set of real numbers, but a more general structure, namely a quantale. On the other, as we already noticed, it is not necessarily true that equality implies indistancy, but rather than indistancy implies inequality. What comes out of these observations is, quite naturally, the notion of a generalized metric domain, itself a generalisation of partial metrics [START_REF] Michael | Partial metric spaces[END_REF]. The rest of this section is devoted to proving that the category of generalised metric domains is indeed cartesian closed, thus forming a model of simply typed λ-calculi.

Formally, given a quantale

Q = (Q, ≤ Q , 0 Q , * Q ) 3 , a generalised metric domain on Q is a pair (A, δ A )
, where A is a set and δ A is a subset of A × Q × A satisfying some axioms akin to those of a metric domain:

δ A (x, 0 Q , y) ⇒ x = y;
(Indistancy Implies Equality)

δ A (x, d, y) ⇒ δ A (y, d, x); (Symmetry) δ A (x, d, y) ∧ δ A (y, e, y) ∧ δ A (y, f , z) ⇒ δ A (x, d * e * f , z). (Triangularity)
Please observe that δ A is a relation rather than a function. Moreover, the first axiom is dual to the one typically found in, say, pseudometrics. The third axiom, instead, resembles the usual triangle inequality for pseudometrics, but with the crucial difference that since objects can have non-null self-distance, such a distance has to be taken into account. Requiring equality to imply indistancy (and thus δ A (x, 0 Q , y) ⇔ x = y), we see that (Triangularity)

gives exactly the usual triangle inequality (properly generalised to quantale and relations [START_REF] Hofmann | Monoidal Topology. A Categorical Approach to Order, Metric, and Topology[END_REF][START_REF] Lawvere | Metric spaces, generalized logic, and closed categories[END_REF]).

In this section we show that generalised metric domains form a cartesian closed category, unlike that of metric spaces (which is known to be non-cartesian closed). As a consequence, we obtain a firm categorical basis of differential logical relations. The category of generalised We can indeed give GMD the structure of a category. In fact, the identity on the object A = (A, Q, δ) in GMD is given by (id A , id A ) where id A : A → A is the set-theoretic identity on A and id A : Q × A → Q is defined by id A (q, a) = q. The composition of two arrows (f , ζ) : (A, Q, δ) → (B, S, ρ) and (g, η) : (B, S, ρ) → (C, T, ν) is the pair (h, θ) where h : A → C is given by the function composition g • f : A → C and h : Q × A → T is given by θ(q, a) = η(ζ(q, a), f (a)). Straightforward calculations show that composition is associative, and that the identity arrow behaves as its neutral element.

Most importantly, we can give GMD a cartesian closed structure, as shown by the following result 4 .

Theorem 11. GMD is a cartesian closed category.

Proof sketch. Before entering details, it is useful to remark that the cartesian product of two quantales is itself a quantale (with lattice and monoid structure defined pointwise). Similarly, for any quantale Q and set X, the function space Q X inherits a quantale structure from Q pointwise. Let us now show that GMD is cartesian closed. We begin showing that GMD has a terminal object and binary products. The former is defined as ({ * }, O, δ 0 ), where O

3 When unambiguous, we will omit subscripts in ≤ Q , 0 Q , and * Q .

4 See [START_REF] Dal Lago | Differential logical relations, Part I: The simply-typed case (extended version)[END_REF] for a detailed proof.

I C

Conclusion

In this paper, we introduced differential logical relations as a novel methodology to evaluate the "distance" between programs of higher-order calculi akin to the λ-calculus. We have been strongly inspired by some unpublished work by Westbrook and Chaudhuri [START_REF] Westbrook | A semantics for approximate program transformations[END_REF], who were the first to realise that evaluating differences between interactive programs requires going beyond mere real numbers. We indeed borrowed our running examples from the aforementioned work.

This paper's contribution, then consists in giving a simple definition of differential logical relations, together with some results about their underlying metatheory: two formulations of the Fundamental Lemma, a result relating differential logical relations and ordinary logical relations, and a proof that generalised metric domains -the metric structure corresponding to differential logical relations -form a cartesian closed category. Such results give evidence that, besides being more expressive than metric relations, differential logical relations are somehow more canonical, naturally forming a model of simply-typed λ-calculi.

As the title of this paper suggests, we see the contributions above just as a very first step towards understanding the nature of differences in a logical environment. In particular, at least two directions deserve to be further explored.

The first one concerns language features: admittedly, the calculus ST λ R we consider here is very poor in terms of its expressive power, lacking full higher-order recursion and thus not being universal. Moreover, ST λ R does not feature any form of effect, including probabilistic choices, in which evaluating differences between programs would be very helpful. Addressing such issues seems to require to impose a domain structure on generalised metric domain, on one hand, and to look at monads on GMD, on the other hand (for the latter, the literature on monadic lifting for quantale-valued relations might serve as a guide [START_REF] Hofmann | Monoidal Topology. A Categorical Approach to Order, Metric, and Topology[END_REF]).

The second one is about abstract differences: defining differences as functions with the same rank as that of the compared programs implies that reasoning about them is complex.

Abstracting differences so as to facilitate differential reasoning could be the way out, given that deep connections exist between logical relations and abstract interpretation [START_REF] Abramsky | Abstract interpretation, logical relations and Kan extensions[END_REF].

Another way to understand program difference better is to investigate whether differential logical relations can be related to abstract structures for differentiation, as in [START_REF] Alvarez-Picallo | Change actions: Models of generalised differentiation[END_REF]. Indeed, Example 6 suggests that an interesting distance between a program and itself can be taken as its derivative, the latter being defined as in [START_REF] Cai | A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation[END_REF].

Figure 2

 2 Figure 2 Typing rules for ST λ R .

Theorem 1 Corollary 2 .

 12 can be proved by way of a standard reducibility argument. Termination implies the following. If • M : REAL then there exists a unique r ∈ R satisfying M ⇓ r, which we indicate as NF (M ).

  nothing more than a term containing a single occurrence of a placeholder [•]. Given a context C, C[M ] indicates the term one obtains by substituting M for the occurrence of [•] in C. Typing rules in Figure 2 can be lifted to contexts by generalising judgments to the form Γ C[∆ • : τ ] : ρ, by which one captures that whenever ∆ M : τ , it holds that Γ C[M ] : ρ. Two terms M and N such that Γ M , N : τ are said to be context equivalent [22] if for every

9 XXX: 8

 98 d, M). At this point the proof is rather standard, and proceeds by induction on the derivation of Γ M : τ .I C A L P 2 0 1 Differential Logical RelationsBut what do we gain from Theorem 7? In the classic theory of logical relations, the Fundamental Lemma has, as an easy corollary, that logical relations are compatible: it suffices to invoke the theorem with any context C seen as a term C[x], such that x : τ , Γ C[x] : ρ. Thus, ultimately, logical relations are proved to be a compositional methodology for program equivalence, in the following sense: if M and N are equivalent, then C[M ] and C[N ] are equivalent, too.

  naturally assigns them distance ∞, the euclidean distance |x -sin(x)| being unbounded when x ranges over R.Let us now prove that (MSIN , f , M ID ) ∈ δ REAL→REAL , where f (x, y) = y + |x -sin x|.Consider any pair of real numbers r, s ∈ R such that |r -s| ≤ ε, where ε ∈ R ∞ ≥0 . We have that: |sin r -s| = |sin r -r + r -s| ≤ |sin r -r| + |r -s| ≤ |sin r -r| + ε = f (r, ε) |sin s -r| = |sin s -sin r + sin r -r| ≤ |sin s -sin r| + |sin r -r| ≤ |s -r| + |sin r -r| ≤ ε + |sin r -r| = f (r, ε).

metric domain, denoted by GMD. Definition 10 .

 10 The category GMD has the following data.An object A is a triple (A, Q, δ) where Q is a quantale and (A, δ) is a generalized metric domain on Q. An arrow (A, Q, δ) → (B, S,ρ) is a pair (f , ζ) consisting of a function f : A → B and another function ζ : Q×A → S satisfying ∀a, a ∈ A.∀q ∈ Q.δ(a, q, a ) ⇒ ρ(f (a), ζ(q, a), f (a )) and ρ(f (a), ζ(q, a ), f (a )).

A L P 2 0 1 9 XXX: 12

 912 Differential Logical Relationsis the one-element quantale {0}, and δ 0 = {( * , 0, * )} (notice that ({ * }, δ 0 ) is a generalized metric domain on O), whereas the binary product A × B of two objects A and B in GMD is given by a triple (A × B, Q × S, δ × ρ). Finally, we define exponentials in GMD. Given C, B in GMD, their exponential C B is the triple (C B , T S×B , ν ρ ), where C B is the function space {f | f : B → C}, T S×B is the exponential quantale, and ν ρ is a ternary relation over C B ×T S×B ×C B defined by: if ρ(b, s, b ) then ν(f (b), d(s, b), f (b )) and ν(f (b), d(s, b ), ζ(b )). Please notice that the relation ν ρ is indeed a differential logical relation. Interestingly, the constructions of product and exponential objects in the proof of Theorem 11 closely match the definition of a differential logical relation. In other words, differential logical relations as given in Definition 5 can be seen as providing a denotational model of ST λ R in which base types are interpreted by the generalised metric domain corresponding to the Euclidean distance.

  base N where x ranges over a set V of variables, r ranges over the set R of real numbers, n is a natural number, and f n ranges over a set F n of total real functions of arity n. We do not make any assumption on {F n } n∈N , apart from the predecessor pred 1 being part of F 1 . The family, in particular, could in principle contain non-continuous functions. The expression M 1 , . . . , M n is simply a shortcut for . . . M 1 , M 2 , M 3 . . . , M n . All constructs are self-explanatory, except for the iflz and iter operators, which are conditional and iterator combinators,

	respectively. An environment Γ is a set of assignments of types to variables in V where
	each variable occurs at most once. A type judgment has the form Γ M : τ where Γ is an
	environment, M is a term, and τ is a type. Rules for deriving correct typing judgments
	are in Figure 2, and are standard. The set of terms M for which • M : τ is derivable is
	indicated as CT (τ ).

Recall that given (pseudo)metric spaces (X, d X ), (Y , d Y ) we can give the set Y X of non-expansive maps between X and Y a (pseudo)metric space structure setting d Y X (f , g) = sup x∈X d Y (f (x), g(x))

x : τ ∈ Γ Γ x : τ Γ r : REAL fn ∈ Fn Γ fn : REAL n → REAL Γ, x : τ M : ρ Γ λx.M : τ → ρ Γ M : τ → ρ Γ N : τ Γ M N : ρ Γ M : τ Γ N : ρ Γ M , N : τ × ρ Γ π1 : τ × ρ → τ

The authors are partially supported by the ERC Consolidator Grant DLV-818616 DIAPASoN, as well as by the ANR projects 14CE250005 ELICA and 16CE250011 REPAS.