Categorical semantics of a simple differential programming language

TL;DR

This paper unifies two theoretical frameworks for differential programming languages, using category theory to model and potentially improve the semantics of automatic differentiation in machine learning.

Contribution

It combines the approach of Abadi and Plotkin with reverse differential categories, providing a categorical model for a simple differential programming language.

Findings

Models Abadi and Plotkin's language using reverse derivative categories

Suggests potential improvements to operational semantics

Bridges two recent theoretical approaches in differential programming

Abstract

With the increased interest in machine learning, and deep learning in particular, the use of automatic differentiation has become more wide-spread in computation. There have been two recent developments to provide the theoretical support for this types of structure. One approach, due to Abadi and Plotkin, provides a simple differential programming language. Another approach is the notion of a reverse differential category. In the present paper we bring these two approaches together. In particular, we show how an extension of reverse derivative categories models Abadi and Plotkin's language, and describe how this categorical model allows one to consider potential improvements to the operational semantics of the language.