Change actions: from incremental computation to discrete derivatives

Thesis

It seems to be a piece of folkloric knowledge among the incremental computation community that incremental programs behave, in some way, like derivatives. Indeed, they track the effect of a function on finite differences in the input, much like derivatives in calculus track the effect of a function on infinitesimal differences. This idea has recently come to the forefront when Kelly, Pearlmutter and Siskind proposed reinterpreting Cai's incremental lambda-calculus as a basis to understand automatic differentiation.

On the other hand, the differential lambda-calculus, an extension of the lambda-calculus equipped with a differential operator that can differentiate arbitrary higher-order terms, has been shown to constitute a model for differentiation in the traditional sense -- that is, there is a model of the differential lambda-calculus where function spaces correspond to spaces of smooth functions, and the term-level derivative operator corresponds to the usual notion of derivative of a multivariate function.

The goal of this thesis is threefold: first, to provide a general semantic setting for reasoning about incremental computation. Second, to establish and clarify the connection between derivatives in the incremental sense and derivatives in the analytic sense, that is to say, to provide a common definition of derivative of which the previous two are particular instances. Third, to give a theoretically sound calculus for this general setting.

To this end we define and explore the notions of change actions and differential maps between change actions and show how these notions relate to incremental computation through the concrete example of the semi-naive evaluation of Datalog queries. We also introduce the notion of a change action model as a setting for higher-order differentiation, and exhibit some interesting examples. Finally, we show how Cartesian difference categories, a family of particularly well-behaved change action models, generalise Cartesian differential categories and give rise to a calculus in the spirit of Ehrhard and Regnier's differential lambda-calculus.

Authors: Alvarez-Picallo, M

• DOI: 10.5287/ora-w4dbbm4mp
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: calculus of finite differences; incremental computation; differential lambda-calculus; programming language semantics
• Subjects: Lambda calculus; Datalog (Computer program language); Denotational semantics