Derivatives of Turing Machines and Inductive Inference

Abstract: What is the derivative of an algorithm? Since algorithms are discrete objects and calculus is about

continuous variations, it is certainly not clear that one should expect any meaningful answer to this question

(try varying a bit in a crucial part of your computer’s operating system and see how big the results are!).

Nonetheless, two logicians Ehrhard and Regnier developed in 2003 a theory of derivatives for terms in

Church’s lambda calculus.  Since the lambda calculus gives a formalisation of the concept of “algorithm”

equivalent (in some sense) to Turing’s machines, the Ehrhard-Regnier derivative is something quite

remarkable. I will explain the computational content of their derivative in some special cases, and how it

provides a theoretical foundation for recent work on program synthesis by gradient descent in the machine

learning community.