dmurfet

I think these papers are fascinating! I would also recommend the Neural Turing Machine paper from DeepMind, which I know better than the papers you mention.

But keep in mind that this is a very young field, and there is no definitive point of view.

I think it’s too early to say what differential lambda calculus or linear logic is “good for” in a practical sense. However, I don’t tend to think of it as being about breaking problems into smaller pieces.

I think it is more about error propagation: you can’t estimate which inputs to an algorithm contribute more to the final error, without some notion of derivative of an algorithm with respect to its inputs (even if those inputs are discrete, so that making infinitesimal variations does not obviously make sense).

I think Pearlmutter and Siskind‘s work is primarily about using ideas from lambda calculus to clean up AD (automatic differentiation) of numeric functions. Whereas differential lambda calculus is not about numeric functions per se: the aim is to define derivatives for arbitrary algorithms.

So, for example, I do not think that in the Pearlmutter-Siskind system that a function of type Int -> Int would have a meaningful derivative, whereas in the differential lambda calculus it does (this is surprising).

I do not recall the details of the Pearlmutter-Siskind system, but some approaches to programming with AD is based on adding formal infinitesimals. There are no infinitesimals explicitly in differential lambda calculus or linear logic, but in the semantics of the latter that we use, derivatives do arise from the coalgebra (k[x]/x^2)^* which is the manifestation of a first-order infinitesimal in algebraic geometry. So in some sense both subjects proceed by adding formal infinitesimals to an existing programming language, but in differential lambda calculus this is implicit.

I don’t think so, but I haven’t really thought about it.

Right. In practice one would want to use more complicated types (such as the type of Turing machines, explained in Clift’s thesis) but in the talk I did not have time to explain more interesting examples.

Thanks! You’re welcome.

I think you are right, the meaning of the sums that appear in syntactic derivatives is quite subtle, and I don’t claim to have an authoritative answer as to their deep meaning.

Semantically, however, I think things are clearer. The denotation of the syntactic derivative of a proof is a limit, and the terms in the limit have an interpretation as probabilistic processes in a (close to) standard sense. So while the sum-over-linear-substitutions doesn’t have a clear probabilistic interpretation (at least that I can see) it is the limit of computational processes where you run the probability of making a substitution to zero.

I don’t know anything about process calculi, unfortunately!

Author here. The theoretical background can be found in:

https://arxiv.org/abs/1407.2650

https://arxiv.org/abs/1701.01285

http://therisingsea.org/notes/MScThesisJamesClift.pdf

As neel_k notes, a good way to understand this picture is in terms of differential linear logic (a refinement of simply-typed differential lambda calculus). I did not provide references in the talk as unfortunately I did not understand the subject at the time, but the introduction to the second paper above hopefully serves to remedy that omission. Suffice to day that Ehrhard and Regnier discovered something quite profound in differential lambda calculus, the implications of which are still being explored; this discovery should have significant bearing on what people refer to as differentiable programming, I think.

The third link above is the master’s thesis of my talented student James Clift. We have subsequently extended that work and are finishing a paper which explains the computational content of derivatives of Turing machines, according to differential linear logic. This might be of interest to people here. I will post a link when we put it online.