报告人：Daniel Murfet (University of Melbourne)
时间：2018-11-30 09:30-10:20
地点：Room 1304, Sciences Building No. 1
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.
