Languages for learning pose interesting foundational challenges. We look at one case: the foundations of differentiable programming languages with a first-class differentiation operator. Graphical and linguistic facilities for differentiation have proved their worth over recent years for deep learning (deep learning makes use of gradient descent optimisation methods to choose weights in neural nets). Automatic differentiation, also known as algorithmic differentiation, goes much further back, at least to the early 1960s, and provides efficient techniques for differentiation, e.g., via source code transformation. It seems fair to say, however, that differentiable programming languages have begun to appear only recently. It seems further fair to say that, while there has certainly been some foundational study of differentiable programming languages, there is ample opportunity to do more.

We investigate the semantics of a simple first-order functional programming language with reals, product types, and a first-class reverse-mode differentiation operator (reverse-mode differentiation generalises gradients). The semantics employs a standard concept of real analysis: smooth multivariate functions with open domain. It turns out that such partial functions fit well with programming constructs such as conditionals and recursion; indeed they form a complete partial order, and so standard fixed-point methods can be applied. From a programming language point of view, however, many types are lacking, particularly sum types and recursive types, such as list types. We conclude with a brief presentation of notions of shapely datatypes and smooth functions. These can be used to give the semantics of such types and the usual functions between them while retaining first-class differentiation.

This work constitutes only an initial exploration, and we look forward to a rich field connecting two worlds: programming languages and their foundations, and real analysis and allied areas of mathematics.

Gordon David Plotkin, FRS, FRSE (born 9 September 1946) is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics were very influential.

Plotkin was elected a Fellow of the Royal Society in 1992, is a Fellow of the Royal Society of Edinburgh and a Member of the Academia Europæa. He is also a winner of the Royal Society Wolfson Research Merit Award. Plotkin received the 2012 Royal Society Milner Award for “his fundamental research into programming semantics with lasting impact on both the principles and design of programming languages.”[19]

His nomination for the Royal Society reads:

Plotkin has contributed to Artificial Intelligence, Logic, Linguistics and especially to Computer Science. In AI he worked on hypothesis-formation and universal unification; in Logic, on frameworks for arbitrary logics; in Linguistics, on formalising situation theory. His main general contribution has been to establish a semantic framework for Computer Science, especially programming languages. Particular significant results are in the lambda-calculus (elementary models, definability, call-by-value), non-determinism (powerdomain theory), semantic formalisms (structured operational semantics, metalanguages), and categories of semantic domains (coherent, pro-finite, concrete). Further contributions concern the semantic paradigm of full abstraction, concurrency theory (event structures), programming logic and type theory.

(from https://en.wikipedia.org/wiki/Gordon_Plotkin)