皆様、

来週の月曜（４月１日）、京都大学数理解析研究所で、プログラム意味論などの研究で著名な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. ==========