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的一个微分扩展，我们为其提供了完全确定性的操作语义。