Confluence of Pure Differential Nets with Promotion
Confluence of Pure Differential Nets with Promotion
复制标题
纯差分网络与提升的融合
DOI：
10.1007/978-3-642-04027-6_36
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Paolo Tranquilli
中科院分区：
文献类型：
--
作者：
Paolo Tranquilli
研究了纯环境下Ehrhard和Regnier微分网指数推广的汇流问题。在缺乏（共）收缩的结合性的情况下，融合与促进和代码排斥失败。因此，我们引入它作为一个必要的等价，连同其他可选的。然后，我们证明了纯微分网是Church-Rosser模这样的等价。这个结果推广到线性逻辑正则证明网，其中等价的相同概念已经在文献中研究过，但仅针对类型化设置中的规范化问题。我们的证明使用的结果有限的发展，这在这种情况下是由强规范化时，阻止一个合适的概念“新”的削减。
We study the confluence of Ehrhard and Regnier's differential nets with exponential promotion, in a pure setting. Confluence fails with promotion and codereliction in absence of associativity of (co)contractions. We thus introduce it as a necessary equivalence, together with other optional ones. We then prove that pure differential nets are Church-Rosser modulo such equivalences. This result generalizes to linear logic regular proof nets, where the same notion of equivalence was already studied in the literature, but only with respect to the problem of normalization in a typed setting. Our proof uses a result of finiteness of developments, which in this setting is given by strong normalization when blocking a suitable notion of "new" cuts.