Coherent differentiation

TL;DR

This paper introduces a new categorical framework for differentiation that avoids the need for additive categories, enabling deterministic and probabilistic models in differential lambda-calculus.

Contribution

It proposes a non-additive categorical semantics for differentiation, compatible with deterministic and probabilistic models, and sketches a deterministic differential lambda-calculus.

Findings

Compatible with coherence spaces and probabilistic coherence spaces

Supports deterministic models in differential lambda-calculus

Provides a foundation for non-additive categorical differentiation

Abstract

The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite nondeterminism and indeed these languages are essentially non-deterministic. We introduce a categorical framework for differentiation which does not require additivity and is compatible with deterministic models such as coherence spaces and probabilistic models such as probabilistic coherence spaces. Based on this semantics we sketch the syntax of a deterministic version of the differential lambdacalculus.