Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A coherent differential PCF

Thomas Ehrhard

TL;DR

The paper develops Λ_cd, a deterministic differential lambda-calculus built on a coherent-differentiation framework that replaces full additivity with a summability structure. It provides a syntax and a categorical semantics that support differentiation with general fixpoints, and demonstrates soundness of reductions within a Kleisli-LL setting, plus a completeness result via a Krivine-style machine. The Rel and PCS models instantiate the framework, with Rel offering a relational interpretation and PCS yielding a deterministic semantics for probabilistic computation, while Scott-summable and elementary-summability notions underpin recursion and differentiation in a partially additive setting. The work thus delivers a fully deterministic differential extension of PCF, complete with an abstract machine and intersection-type techniques bridging syntax, operational semantics, and denotational models. This advances differentiable programming by reconciling differentiation with deterministic computation and fixed-point definitions, with potential implications for coherent differentiable programming languages and semantic models of LL-based systems.

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.

A coherent differential PCF

TL;DR

The paper develops Λ_cd, a deterministic differential lambda-calculus built on a coherent-differentiation framework that replaces full additivity with a summability structure. It provides a syntax and a categorical semantics that support differentiation with general fixpoints, and demonstrates soundness of reductions within a Kleisli-LL setting, plus a completeness result via a Krivine-style machine. The Rel and PCS models instantiate the framework, with Rel offering a relational interpretation and PCS yielding a deterministic semantics for probabilistic computation, while Scott-summable and elementary-summability notions underpin recursion and differentiation in a partially additive setting. The work thus delivers a fully deterministic differential extension of PCF, complete with an abstract machine and intersection-type techniques bridging syntax, operational semantics, and denotational models. This advances differentiable programming by reconciling differentiation with deterministic computation and fixed-point definitions, with potential implications for coherent differentiable programming languages and semantic models of LL-based systems.

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.
Paper Structure (53 sections, 91 theorems, 212 equations, 14 figures)

This paper contains 53 sections, 91 theorems, 212 equations, 14 figures.

Table of Contents

  1. Introduction
  2. Contents
  3. Semantic motivations
  4. The choice of PCF
  5. Syntax
  6. Categorical semantics and soundness
  7. Intersection types, Krivine machine and completeness of the reduction
  8. Probabilistic semantics and determinism
  9. Preliminaries
  10. Notations
  11. Rewriting
  12. Semantic motivations
  13. A summary of summable differential categories
  14. The associated monad, its monoidal strength and its commutativity
  15. Differentiation as a double distributive law on a resource category
  16. ...and 38 more sections

Key Result

Lemma 3.1

Let $f\in\mathcal{L}(X,Y)$ and $g\in{\mathcal{L}}_\oc(Y,Z)$, we have $g\mathrel\circ\mathsf{Lin}_{\mathord\oc}(f)=g\,\oc{f}$.

Figures (14)

  • Figure 1: Linear reduction, $L$ must be a linear context of height $1$.
  • Figure 2: Typing rules
  • Figure 3: Inductive definition of the differential of a term
  • Figure 4: Inductive definition of the differential of a context
  • Figure 5: Main reduction rules
  • ...and 9 more figures

Theorems & Definitions (185)

  • Lemma 3.1
  • proof
  • Lemma 3.2
  • Definition 3.3
  • Remark 3.4
  • Lemma 3.5
  • Lemma 3.6
  • Lemma 3.7
  • Theorem 3.8
  • proof
  • ...and 175 more