The Cut-Elimination Theorem for Differential Nets with Promotion
The Cut-Elimination Theorem for Differential Nets with Promotion
复制标题
带提升的微分网络割消定理
DOI：
10.1007/978-3-642-02273-9_17
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Michele Pagani
中科院分区：
文献类型：
--
作者：
Michele Pagani
最近Ehrhard和Regnier介绍了差分线性逻辑，简称DiLL-线性逻辑的乘法指数片段的扩展，能够表达非确定性计算。作者研究了通过一个证明网类演算：微分相互作用网的削减消除的促进自由片段的DiLL。我们将这种分析扩展到指数盒，并证明了整个DiLL的割消定理：每个可序列化的微分网都可以简化为无割网。
Recently Ehrhard and Regnier have introduced Differential Linear Logic, DiLL for short -- an extension of the Multiplicative Exponential fragment of Linear Logic that is able to express non-deterministic computations. The authors have examined the cut-elimination of the promotion-free fragment of DiLL by means of a proofnet-like calculus: differential interaction nets. We extend this analysis to exponential boxes and prove the Cut-Elimination Theorem for the whole DiLL: every differential net that is sequentializable can be reduced to a cut-free net.