一句话：提出确定性微分 lambda 演算，基于非加性范畴语义，将 PCF 扩展为完全确定性的微分语言。
微分 lambda 演算与微分线性逻辑的范畴模型因 Leibniz 规则需要求和而本质上是加法范畴，这使其模型带有有限非确定性，语言也因此是非确定性的。本文基于作者先前提出的无需加法性的微分范畴框架——该框架同时兼容相干空间等确定性模型与概率相干空间等概率模型——为微分 lambda 演算构造一种确定性语法。该方法的优点是与项的一般不动点兼容，因此所得语言实际上是 PCF 的微分扩展，作者为其提供了完全确定性的操作语义。
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.