[logic-ml] Talk by Gordon Plotkin on 1st April 2019 at Kyoto

[Masahito Hasegawa]

皆様、

来週の月曜（４月１日）、京都大学数理解析研究所で、プログラム意味論などの研究で著名なGordon
Plotkinさん（Edinburgh大学）の講演があります。詳細は下記のとおりです。関心をお持ちの方のご来聴を歓迎します。どうぞよろしくお願いいたします。

京都大学数理解析研究所
長谷川真人

==========
Time:  14:00-15:00, 1st April 2019 (Mon.)
Place: Room 110, Research Institute for Mathematical Sciences, Kyoto University
  京都大学数理解析研究所（本館）１階１１０号室
  http://www.kurims.kyoto-u.ac.jp/en/access-01.html

Speaker: Gordon Plotkin (LFCS, University of Edinburgh)

Title:  One-and-a-half simple differentiable programming languages

Abstract:

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.  We  give an operational semantics which, roughly, can be
seen as a formalisation of a version of the trace (or tape) method
used to implement automatic differentiation. The semantics consists of
three parts: ordinary evaluation, symbolic evaluation to eliminate
control constructs, and a source-code transformation to symbolically
differentiate terms with no control constructs,

>From a programming language point of view, however, many types are
lacking, particularly sum types and recursive types, such as lists. 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.
==========