From Differential Linear Logic to Coherent Differentiation
Abstract
In this survey, we present in a unified way the categorical and syntactical settings of coherent differentiation introduced recently, which shows that the basic ideas of differential linear logic and of the differential lambda-calculus are compatible with determinism. Indeed, due to the Leibniz rule of the differential calculus, differential linear logic and the differential lambda-calculus feature an operation of addition of proofs or terms operationally interpreted as a strong form of nondeterminism. The main idea of coherent differentiation is that these sums can be controlled and kept in the realm of determinism by means of a notion of summability, upon enforcing summability restrictions on the derivatives which can be written in the models and in the syntax.
Cite
@article{arxiv.2401.14834,
title = {From Differential Linear Logic to Coherent Differentiation},
author = {Thomas Ehrhard},
journal= {arXiv preprint arXiv:2401.14834},
year = {2024}
}