We thank the three reviewers very much for their comments.
We reply below to some of them.
Reviewer 1
> I did not have a very clear idea of
> what the extra generality of QLRs offers over, for example, generalised metric
> domains presented by Dal Lago, Gavazzo and Yoshimizu.
Generalized metric domains satisfy some axioms which are not compatible with the metric structures investigated in the paper. Our approach consisted in identifying the simplest structure to which the constructions from [27] and [36] could be extended, and then to study in full generality the metric axioms compatible with such constructions (in particular, our discussion of "relaxed metrics" encompasses the case of generalized metric domains).
> It is also not clear to me how (or if) the proposed category LL
> of locally Lipschitz maps (which I generally found of more interest) relates to Q.
The two categories have a different cartesian closed structure, due to the restriction, in LL, to morphisms in which the second map is additive in its second variable. The simplest idea to relate Q and LL is to consider a subcategory of Q (call it Qadd) where morphisms enjoy this restriction. Qadd is still cartesian closed, but with exponential structure similar to that of LL and not to that of Q. It should then be possible to define a suitable functor from Qadd to LL preserving the cartesian closed structure. However, while it is not trivial to find (e.g. real-valued) functions with an additive derivative in Q, the locally Lipschitz functions are well-known, so we preferred to work directly with LL.
> Finally, the authors have pointed to some very tantalizing potential
> connections to incremental and differential calculi, which are sadly left unexplored.
Due to space limitation our discussion of this connection could not go beyond observing some formal similarities. Yet, due to the centrality of "derivatives" in our constructions it seemed important to mention that such connections exist. In particular, it seemed worth observing that the restriction to additive derivatives (in Section VI) yields an exponential structure closely resembling that of the differential lambda-calculus.
> In Cartesian difference categories, linearity is weakened to a "regularity" condition
> stating f'(x, a + b) = f'(x, a) + f'(x + \varepsilon a, b). Do derivatives in QLRs
> satisfy a similar property, or are there any suitably simple conditions under which
> linearity or regularity can be recovered?
The regularity condition of cartesian difference categories can be retrieved for the QLR which arise from a change structure (as discussed below).
> Lemma 4.1 is startlingly similar to Theorem 2.9 in Cai, Giarrusso et al, 2014,
> except they start from a difference operator rather than a metric. Is there a deeper
> connection that can be made precise? Are change structures a particular case of QLRs?
We thank the reviewer for this observation. Indeed, a change structure (A,Delta A, +, - ) where DeltaA is a quantale yields a QLR (A,DeltaA, d) with d(x,y)=x-y. In particular, when - satisfies a few more axioms, this yields a partial metric space (an example is the change structure over the reals with the Lawvere quantale with truncated subtraction). Under this correspondence Theorem 2.9 from Cai, Giarrusso et al. 2014 is a special case of our Lemma 4.1.
Reviewer 2
> The authors claim that including the $φ$ component is a crucial ingredient for
> obtaining a Cartesian-closed category. I didn't understand why this was the
> case.
The essential (and related) ingredients behind the two families of cartesian closed categories discussed in the paper are the fact of considering distances measured over distinct quantales, and the (consequent) fact of accompanying functions with maps relating distances in input with distances in output.
With a fixed quantale, and no \Phi component, one can still obtain, in some special cases, a cartesian closed category of metric spaces (see [22]). However, this will depend on restricting to metric spaces enjoying some special condition (e.g. to injective metric spaces), and not on general semantic constructions as those we introduced.
> it is unclear how much this $φ$ (or, more generally, the semantics) helps us
> with this analysis -- e.g. it could be the case that the computed bound grows
> very large for many programs.
The computation of the derivative of a program involves an approximation (i.e. the computation of a sup) which can be more or less accurate depending on the chosen QLR structure and the chosen overall model. For example, let f: R-->R be the real-valued function f(x)=x^2 and B be the ball of center 0 and radius epsilon. The derivative of f in Q computed in B yields the ball of center f(0)=0 and radius epsilon^2. Instead, the derivative of f in pV computed in B yields the closed interval [0, \epsilon^2]. Hence the two derivative approximate the behavior of f in different ways, the second one looking somehow finer.
Moreover, we should have highlighted that the accuracy of such bounds is not affected by the applications of the cartesian closed operations of lambda-abstraction and evaluations, since these do not involve the computation of new approximations (i.e. of new sups).
> It would be nice to present more interesting,
> self-contained program properties that can benefit from the semantics
For reasons of space, we could not go too deep with examples, but we agree that this might help motivate our proposal. The fundamental quantitative properties we have in mind is the (compositional) computation of error bounds for contextual program transformations, in which a program is replaced with one which is only approximately similar. In the semantics of differential logical relations [27] and diameter spaces [36], that our approach generalizes, these applications have been demonstrated in more details (e.g. for well-known techniques like loop perforation and numerical integration).
Reviewer 3
> One point where I am not completely sure, is how far this models are from the
> differential logical relations of [27]
Differential logical relations (DLR) and QLR are indeed very similar semantics, which differ in considering the distance as a relation or as a function. In fact, several results from Section IV can be reformulated in terms of DLR. However, the models pV and V from Section V, and the generalization of locally Lipschitz functions, do not seem to have a clear analog within DLR.
> Why do you consider only relations on a set X? Why not having as objects also
> relations of the form X x Y --> Q?
For a quantitative study of STLC we could have well considered an alternative category, say R, where objects are "non-uniform" QLR as suggested and arrows are triples (f,g,\varphi) defined in a somehow similar way. However, we chose to restrict ourselves to "uniform" QLR (and to the category Q) since our main goal was to investigate metric structures compatible with cartesian closedness. In particular, specializing QLR to metric spaces requires to consider uniform QLR and their morphisms (which do not form a full subcategory of R), and also the constructions from Section V and VI do not have clear analogs in the non-uniform case.
> About related work, at the level of objects, quantitative logical relations have also
> been considered previously, say in [A]
We thank the reviewer for signaling this relevant reference.