Confluence of Pure Differential Nets with Promotion

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.

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Paolo Tranquilli
• Keywords: Automated Reasoning, CSL 2009, Exponential Promotion, Pure Setting, Regular Proof Nets