A coherent differential PCF

TL;DR

This paper introduces a deterministic differential lambda-calculus framework compatible with non-additive models, extending PCF with a semantics that supports fixpoints and deterministic computation.

Contribution

It develops a new categorical framework for differentiation that avoids additivity, enabling deterministic models and extending PCF with a fully deterministic semantics.

Findings

Compatible with coherence spaces and probabilistic models

Supports general fixpoints in a deterministic setting

Provides a fully deterministic operational semantics

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 non-determinism and indeed these languages are essentially non-deterministic. In a previous paper we introduced 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 develop a syntax of a deterministic version of the differential lambda-calculus. One nice feature of this new approach to differentiation is that it is compatible with general fixpoints of terms, so our language is actually a differential extension of PCF for which we provide a fully deterministic operational semantics.