[yaseer]

Fantastic stuff!

Does your work still keep the non-determinism of Ehrhard and Regnier?

This was the part that 'bothered' me, but it provided evidence of a link with process calculi.

I've also thought Ehrhard and Regnier's work was groundbreaking. It potentially opens up not just insights into differentiable programming, but a theory of concurrent computation and an algebraic theory of computation. My expectation is that it will reveal some deep links with other areas of mathematics, like group theory.

[dmurfet]

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!

[yaseer]

P.S - Silly question, I can see it does. I responded before reading.