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