论文标题
连贯的差分PCF
A coherent differential PCF
论文作者
论文摘要
差分lambda-calculus的分类模型是加性类别，因为Leibniz规则需要求和两个表达式。这意味着，就差异lambda-calculus和差异线性逻辑而言，这些模型具有有限的非确定性，实际上这些语言本质上是非确定性的。在上一篇论文中，我们引入了分化的分类框架，该框架不需要添加性，并且与确定性模型（例如相干空间和概率模型，例如概率相干空间）兼容。基于这种语义，我们开发了差分lambda-calculus的确定性版本的语法。这种新的差异化方法的一个不错的功能是它与术语的总固定点兼容，因此我们的语言实际上是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.
