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 nondeterminism and indeed these languages are essentially non-deterministic. We introduce 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 sketch the syntax of a deterministic version of the differential lambdacalculus.
翻译：由于Leibniz 规则要求将两种表达方式相加,因此,区分羊肉计算法的绝对模型是添加型。这意味着,就区别羊肉计算法和不同的线性逻辑而言,这些模型具有有限的非确定性,事实上这些语言基本上是非决定性的。我们引入了明确的区分框架,它不要求相加性,而且与诸如一致性空间和概率一致性空间等概率模型等确定型模型相容。基于这一语义学,我们绘制了差异羊肉计算法的确定性版本的语法。
相关内容
微信扫码咨询专知VIP会员