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.

翻译：微分λ-演算的范畴模型是加法范畴，因为莱布尼茨法则要求对两个表达式进行求和。这意味着，就微分λ-演算和微分线性逻辑而言，这些模型具有有限非确定性特征，实际上这些语言本质上是非确定性的。在先前的一篇论文中，我们引入了一种不需要加法性且与确定性模型（如相干空间）和概率模型（如概率相干空间）兼容的微分范畴框架。基于该语义学，我们发展了一种确定性版本的微分λ-演算的语法。这种新微分方法的一个显著特点是它与项的一般不动点兼容，因此我们的语言实际上是PCF的一种微分扩展，我们为此提供了一种完全确定性的操作语义学。