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.
翻译：微分λ演算的范畴模型是加性范畴，因为Leibniz规则要求两个表达式相加。这意味着，就微分λ演算和微分线性逻辑而言，这些模型具有有限的非确定性，事实上这些语言基本上是非确定性的。在之前的一篇论文中，我们介绍了一种微分范畴的框架，它不需要加性，与确定性模型（如连通空间）兼容，并与概率模型（如概率连通空间）兼容。基于这个语义，我们发展了一个确定性版本的微分λ演算语法。这种新方法微分扩展了PCF，我们提供了一个完全确定性的操作语义。一个很好的特性是，这种新方法兼容术语的一般不动点。
相关内容
微信扫码咨询专知VIP会员