We study the deep relations existing between di erential logical relations and incremental computing, by showing how self-di erences in the former precisely correspond to derivatives in the latter. We also show how di erential logical relations can be seen as a powerful metatheoretical tool in the analysis of incremental computations, enabling an easy proof of soundness of di erentiation.
One of the major challenges programming language theory is facing these days
is the development of adequate abstractions to deal with the (highly)
increasing complexity and heterogeneity of modern software systems. Indeed, since the
very birth of the discipline, researchers have been focused on the design of
compositional techniques for software analysis, whereby one can study the overall
behavior of a system by inspecting its constituent parts in isolation. A prime
example of the successfulness of such an analysis is given by the theory of
program equivalence. Notwithstanding its successful history, program equivalence
is revealing some weaknesses when applied to nowadays software, where exact
reasoning about components is, either because of the very nature of the
software involved or because of the cost of such an analysis, oftentimes not feasible.
Examples witnessing such weaknesses are given by the elds of probabilistic
computing, where small perturbations in probabilities break equivalence, numerical
computing, where program implementing numerical functions can be optimized
at the price of introducing an acceptable error in the output, and, more generally,
approximate computing [
The common pattern behind all the aforementioned examples is the shift from
an exact analysis of software, whereby equivalent pieces of software are
interchangeable within any system, to an approximate analysis of software, whereby
non-equivalent pieces of software are replaced within a system at the price of
producing an acceptable error, and thus an approximately correct result. Moving
from an exact to an approximate analysis of programs poses several challenges
? Copyright c 2020 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
to programming language semantics, the main one arguably concerning
compositionality. In fact, once we replace a program P with a non-equivalent one Q
in a system C[ ], then C[ ] may amplify the error introduced by the
replacement of P with Q, this way invalidating compositionality of the analysis. This
point becomes evident when studying (higher-order) program metric or program
distance [
Motivated by these general observations, researchers are showing an increasing interest in quantitative analysis of programs, with a special focus on di erential properties of programs. Although the expression di erential has no precise meaning in this context, we may identify it with the collection of properties relating local and global changes in software. Thus, for instance, we can think of the (error produced by the) replacement of P with Q as a local change, and investigate its relationship with the global change we observe between C[P ] and C[Q].
The study of such di erential properties has led, oftentimes abusing terminology, to the development of several notions of a program derivative. Among those, some of the main ones one encounters when looking at the relevant literature are the following.
Those coming from the eld of automatic di erentiation [
Those coming from the di erential -calculus [
Those coming from incremental computing [
Those coming from di erential logical relations [
It is thus natural to ask whether there are connections between such notions.
Although for some of the aforementioned cases the answer seems to be negative
(for instance, the derivatives one nds in incremental computing are
generalizations of nite di erences [
In this paper we study such similarities and establish a formal connection between di erential logical relations and incremental computing, by showing how self-di erences in the former precisely correspond to derivatives in the latter. In fact, as we will see, the derivative of a program P can be seen as a way to quantify how much changes in the input of P in uence changes in its output, this way acting as a self-di erence for P .
Besides its conceptual implications, the advantages of such a correspondence
are twofold. On the one hand, di erential logical relations qualify as a lightweight
operational technique for incremental computing: we witness that by giving a
proof of soundness of di erentiation for the incremental -calculus of Cai et al.
[
In this section we shortly review the main ideas behind di erential logical
relations (DLRs) and the incremental -calculus. In order to do so, we introduce the
vehicle calculus of (the rst part) of this work, namely a call-by-value simply
typed -calculus with a primitive type for real numbers, which we denote by
STR. The calculus is standard and it is essentially the same calculus used in [
We use letters t; s; : : : to range over terms, and v; w; : : : to range over values.
Additionally, we follow standard syntactic conventions as in, e.g., [
The dynamics of STR is given by a standard call-by-value operational semantics, de ned in Figure 2, where for a function ' : Rn ! R and a number r 2 R we write 'r : Rn 1 ! R for the mapping (r1; : : : ; rn 1) 7! '(r; r1; : : : ; rn 1). Notice, in particular, that ' r1 rn eventually reduces to '(r1; : : : ; rn).
Since STR is simply-typed, standard reducibility [
! ; x :
` x : t; s ::= x j r j ' j ht; si j x:t j out1 t j out2 t j ts v; w ::= x j r j ' j hv; wi j x:t ` r : R ` ' : R ! | {z n ! R ! R
} ` t : 1 2 ` out1 t : 1 ` t : ! ` ts : ` t : 1 2 ` out2 t : 2 ` s : closed value v|that we indicate as nf(t)|in a nite number of !-steps (notation t + v). We write t +n v, for n 2 N, to state that t evaluates to v in n number to !-steps and ! for the re exive and transitive closure of !.
( x:t)v ! t[v=x] ' r ! 'r outi hv1; v2i ! vi t ! t0 ts ! t0s s ! s0 vs ! vs0 t ! t0 ht; si ! ht0; si
s ! s0 hv; si ! hv; s0i
t ! t0 outi t ! outi t0 Despite its simplicity, STR allows us to justify the shift from program equivalence|that is the family of notions concerning equality between programs|to program distance, in general, and to di erential logical relations, in particular.
First, let us de ne a suitable notion of program equivalence for STR programs.
Due to its simple nature, STR allows us to choose among a large family of
notions of program equivalence, ranging from denotationally-based equivalences to
operationally-based ones. Here we choose extensional or applicative equivalence4.
4 This is nothing but a simpli cation of Abramsky's applicative bisimilarity [
De nition 1. De ne the type-indexed family of relations (= V V ) as follows (where i 2 f1; 2g): ; =V hv1; v2i =V1 2 hw1; w2i () 8i: vi =Vi wi t = t0 () nf(t) =V nf(t0) r =RV r0 () r = r0 v =V
! v0 () 8w 2 V : vw = v0w
It is well-known that extensional equivalence is a congruence relation, this way enabling compositional reasoning about program behaviors: s = s0 entails t[s=x] = t[s0=x] for any term x : ` t : . Unfortunately, one soon realizes that due to the presence of (constants for) real-numbers, program equivalence is a too coarse notion for reasoning about STR programs. For it is desirable to regard two programs of type R whose outputs are " apart to be themselves " apart, rather than just state that the two are not equivalent.5
The natural way to overcome this problem is to re ne = into a map :
! R following Lawvere's correspondence between ordered sets and
(generalized) metric spaces [
r (t; t0) , V (nf(t); nf(t0))
V1 2 (hv1; v2i; hw1; w2i) , max i2f1;2g V! (v; v0) , sup w2V
Vi (vi; wi)
(vw; v0w)
which can be easily proved to be generalized metrics6 [
Unfortunately, we immediately see that fails to be non-expansive, and thus
compositional. Even worse, any reasonable non-expansive metric-like map is
bound to trivialize, meaning that it collapses to a congruence relation. Roughly,
given two terms s; s0 which are " 6= 0 apart, for any positive real number c it is
always possible to nd an open term x : ` t : such that t[s] and t[s0] are c
apart. For it is su cient to take a term t using its input x enough times: once
the terms t[s] and t[s0] are evaluated, any time t uses x the distance between s
5 A similar argument can be formulated for any language/calculus exhibiting, either in
its syntax or in its semantics, some quantitative behavior. Typical examples of such
behaviors are given by types for quantitative objects, such as numeric types, but
also by probabilistic primitives, the latter making relevant semantic notions, such as
termination, quantitative [8, 10{12, 15, 27, 5].
6 Additionally, by replacing r0 r and supr1;:::;rn (r1; : : : ; rn) '(r1; : : : ; rn) with
jr0 rj and supr1;:::;rn j (r1; : : : ; rn) '(r1; : : : ; rn)j, respectively, becomes a
pseudometric [
Di erential Logical Relations
The failure of non-expansiveness of quantitative re nements of notions of
program equivalence has led researchers to propose several notions of program
distance [
Let us expand on this last point by means of an example. Consider the (linear) programs t , x:x and s , x:sin x for the identity and sine function, respectively. It is easy to see that measuring the distance between t and s as we did when de ning , we are forced to conclude such a distance to be 1. In fact, for r ! 1 we have jr sin(r)j ! 1. This is rather unsatisfactory, as such distance does not take into account which input the environment will actually pass to t and s. For instance, if the environment feeds t and s with an input v close to zero, then the distance between tv and sv should be close to 0 too, and thus we would like to conclude that in all such cases the distance between t and s is itself close to zero.
Summing up, ordinary notions of program distance are not sensitive to the
context in which programs are used. This ultimately relies on the fact that
measuring the distance between two programs (regarded as functions) as just one
single number there is no way to give information on how such programs interact
with the environments in which they are used. Di erential logical relations have
been introduced in [
Di erential logical relations take the form of (type-indexed) ternary relations
D relating pairs of programs together with di erences between them. When
dealing with programs of type ! , di erences take the form of functions
mapping input programs of type and di erences for such programs to di
erences for programs of type . This is why here we consider a
computationallyoriented notion of di erence whereby di erences between programs are de ned
as programs themselves (cf. [
We formalize these ideas by assigning to each type a type habitants are terms acting as di erences between terms of type . whose in
R , R; ( ) , ; ( ! ) , ! ! :
Notice, in particular, that a di erence between two programs of type ! is a program taking an input of type and a -di erence, and returning a -di erence.
Obviously, given two programs t; t0 of type , not all programs of type can act as (meaningful) di erences between t and t0. Di erential logical relations (DLRs for short) are ternary relations speci cally designed to isolate meaningful di erences between programs. More precisely, a DLR is a type-indexed family of ternary relations D , (D ; DV ) , where D and DV V V V , such that D (dt; t; t0) holds if and only if dt is a di erence7 between t and t0 (and similarly for values).
De nition 3 (Asymmetric DLRs). A di erential logical relation is a typeindexed family of ternary relations (D ; DV V V V ) such that:
DRV (dr; r; r0) () r0
r = dr DV1 2 (dv; v; v0) () 8i 2 f1; 2g: DVi (outi dv; outi v; outi v0) DV! (dv; v; v0) () 8dw; w; w0: DV (dw; w; w0) =) D (dv w dw; vw; v0w0) D (dt; t; t0) ()
DV (dv; v; v0) where dt + dv; t + v; t0 + v0:
Remark 1. Contrary to the original formulation of DLRs [
As already remarked, DLRs have been introduced with the goal of developing
a compositional theory of program distance. This goal is achieved by the so-called
Fundamental Lemma [
Lemma 1 (Fundamental Lemma, Version 1). For any program t 2
there exists a self-di erence dt for it. That is, D (dt; t; t).
7 Following conventions in, e.g., [
Lemma 1 enables compositional reasoning on program di erences. Informally, by regarding a context x : ` t : as a term x:t we are guaranteed a selfdi erence dt for t to exist, so that given two programs s; s0 of type with di erence ds between them, one can compute the di erence between t[s=x] and t[s0=x] starting from s, ds, and dt alone. 2.3
The Incremental -calculus and Program Derivatives Albeit enabling compositional reasoning on program di erences, Lemma 1 has the major drawback of guaranteeing the existence of self-distances without giving any explicit information on how to construct them. As we will see in the next section, the self-distances of Lemma 1 are precisely the program derivatives used in the incremental -calculus.
The incremental -calculus is a formalism introduced by Cai et al. [
In order to provide a formal foundation for higher-order incremental
computation, Cai et al. [
In the next section, we will show how we can easily prove such results using
DLRs, and, dually, how by identifying di erences with changes we can improve
8 Obviously, to be practically useful, the map f 0 should be such that computing
f 0(a; da) is cheaper than computing f (a da).
9 The terminology is misleading. For instance, we should not think of the derivative
D' of a term ' : R ! R as the syntactic counterpart of the derivative of ' : R ! R.
Rather, D' represents the nite di erence [
De nition 4. Given functions ' : Rn ! R and d' : (R maps ' d' : Rn ! R and ' : (R R)n ! R by: R)n ! R, de ne the ('
d')(x1; : : : ; xn) , '(x1; : : : ; xn) + d'((x1; 0); : : : ; (xn; 0)); '((x1; dx1); : : : ; (xn; dxn)) , '(x1 + dx1; : : : ; xn + dxn) '(x1; : : : ; xn): The map ' is known as the nite di erence of '. Notice that ' ' = '.
De nition 5. De ne the partial operator : (outi t) ( x:t) ! !
as follows: (outi dt) , outi (t
dt); ( x: dx:dt) , x:(t
dt); (ts) (dt s ds) , (t dt) (s ds): x r ' dx , x; dr , r + dr; d' , ' d'; dt; s ht; si hdt; dsi , ht
dsi;
The de nition of t dt may appear weird at rst, but it will become clear once the notion of a derivative is introduced. Intuitively, given a term t and a change dt, we can see t dt as the term obtained by changing t according to dt. Clearly, this is possible only if dt has the `right' structure (for instance, it would be meaningless to do something like changing a function according to a number). We immediately notice that if v is a value and v dv is de ned, then dv and v dv are values too. Moreover, the following typing rule is admissible, whenever t dt is de ned: ` t :
d ; ` t
` dt : dt : where for = x1 : 1; : : : ; xn : n, we have d , dx1 :
Next, we de ne the notion of a derivative of a term. 1; : : : ; dxn :
De nition 6. The derivative Dt of a term t is thus de ned:
Dx , dx; D' , ';
Dr , 0;
Dht; si , hDt; Dsi; D(outi t) = outi Dt;
D( x:t) , x: dx:Dt;
D(ts) , Dt s Ds:
Observe that we can indeed think of Dt as the generalization of nite differences to arbitrary programs. Moreover, we easily see that if ` t : , then ; d ` Dt : and that t Dt is de ned and equal to t itself.
In this section we relate DLRs with the incremental -calculus we introduced in
the previous section. We do so acting on two orthogonal axes. On the one hand,
we show that derivatives are precisely the self-distances of Lemma 1. That is, for
any program t, Dt is a self-distance for t. This result allows us to strength the
fundamental lemma of DLRs (Lemma 1), as now self-di erences can be e ectively
computed. On the other hand, we prove by means of DLRs a major result on
the incremental -calculus, namely soundness of di erentiation [
Let us begin proving that derivatives are actually self-di erences. In order
to achieve such a result, we have to rst extend the notion of a DLR to open
terms [
De nition 7. We extend the notion of a DLR to substitutions over an environment as follows: D (d ; ; 0) () 8(x : ) 2 : DV (d (dx); (x); 0(x)), where ; 0 2 S( ) and d 2 S(d ).
As it is customary, we write t[ ] for the application of the substitution to the term t, and [x 7! v] for the substitution mapping x to v and behaving as otherwise. Before proving our re nement of Lemma 1, let us observe that DLRs are closed under reduction, in the following sense.
D (dt; t; t0) ^ t ! D (dt; s; s0) ^ s ! s ^ t0 ! t ^ s0 ! s0 =) t0 =)
D (dt; s; s0); D (dt; t; t0):
We are now ready to prove our new version of the Fundamental Lemma. Lemma 3 (Fundamental Lemma, Version 2). For any program t 2 have D (Dt; t; t). we Proof (sketch). The thesis follows from the stronger statement: for any term ` t : and value ` v : we have: 8d ; ; 0: D (d ; ; 0) =)
DV (Dv[ ; d ]; v[ ]; v[ 0]) ^ D (Dt[ ; d ]; t[ ]; t[ 0]): The proof of the latter is a routine induction on t and v. tu
Notice how Lemma 3 improves the compositionality principle of DLRs. Given a term x : ` t : and two values ` v; v0 : such that DV (dv; v; v0) the impact of replacing v with v0 in t can be computed as Dt[v=x; dv=dx]. Next, we show how the incremental -calculus can bene t from DLRs by showing how the latter support an easy proof of soundness of di erentiation.
Theorem 1 (Soundness of Di erentiation [
Our proof of Theorem 1 is based on the following result which states that changes indeed behave as such. Recall that = extends to open terms by stipulating that for ` t; t0 : we have t = t0 i t[ ] = t0[ ], for any substitution 2 S( ) (and similarly for values).
Proposition 1. The following holds for all (possibly open) terms t; t0; dt and values v; v0; dv such that t dt and v dv is de ned.
D (dt; t; t0) =) t0 = t dt;
DV(dv; v; v0) =) v0 = v dv: Proof (sketch). The proof is by induction on , the relevant case being the one of values. We show how to handle the case for arrow types. Assume ` t; t0 : ! . We have to show that for any 2 S( ), t0[ ] = (t dt)[ ]. First, observe that we have the following general result (by induction on t), where (D )(dx) , D (x): (t dt)[ ] = t[ ] dt[ ; D ]. By Lemma 3, we have D (D ; ; ), hence DV! (dt[ ; D ]; t[ ]; t0[ ]). In particular, we must have t[ ] = x:s, t0[ ] = x:s0, and dt[ ; D ] = x: dx:ds, for some s; s0, and ds. Since ( x:s) ( x: dx:ds) = x:(s ds) (notice that this term is indeed de ned, as it is obtained from t dt, which is de ned by hypothesis, replacing variables y; dy with closed values v, Dv), in order to prove the thesis we have to show s0[v=x] = (s ds)[v=x] for any closed value v of type . Since (s ds)[v=x] = s[v=x] ds[v=x; Dv=dx] we obtain the thesis from DV! (dt[ ; D ]; t[ ]; t0[ ]) and DV(Dv; v; v), the latter being a consequence of Lemma 3.
We can nally prove soundness of di erentiation.
Proof (Theorem 1). Assume DV(dv; v; v0). By Lemma 3 we have D ! (Dt; t; t), and thus D (Dt s ds; ts; ts0), by Lemma 2. We conclude that tv0 = (tv) (Dt v dv) from Proposition 1.
Remark 2. To the best of the authors' knowledge, all proofs of Theorem 1 in
the literature are based on either denotational semantics or on logical relations
resembling DLRs, but speci cally extended with a clause requiring t dt = t0
for all related terms dt; t; t0, at any type [
Di erential logical relations have been introduced by the authors and Yoshimizu
[
The incremental -calculus has been introduced by Cai et al. [
In this work we have established a formal connection between di erential
logical relations and the incremental -calculus of Cai et al. [
In addition to its conceptual relevance, the connection established in the
present work also allows us to obtain technical improvements both on the
theory of incremental -calculus and on the one of di erential logical relations.
Concerning the former, we have showed how di erential logical relations
constitute a lightweight operational technique for incremental computing, and we have
witnessed that by giving a new, relatively easy proof of soundness of di
erentiation. Concerning the latter, we have strengthened the fundamental lemma of
DLRs [