Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the role of connectivity in Linear Logic proofs

Raffaele Di Donna, Lorenzo Tortora de Falco

TL;DR

This work addresses when a graphical proof structure in linear logic corresponds to a sequent calculus proof by linking a connectivity-based geometric property to correctness. It introduces the untyped sequentiality theorem via a $(\neg\mathsf{w}\otimes)$-ps and shows that, inside this framework, the criterion $AC_{\sharp w}$ becomes sufficient for sequentialization, even in fragments with units and exponentials. It further develops a canonical jumping mechanism to refine sequentialization in the (NBT)LL fragment and proves that equivalence under rule permutations is tractable within this setting. The approach extends to multiplicative-exponential logic (MELL) and intuitionistic polarizations, including IMELL and ICOMLL, providing a unified, connectivity-driven perspective on sequentialization, cut-elimination stability, and proof-structure equivalence. Overall, the paper contributes practical criteria and constructive procedures for turning geometric properties of proof-structures into reliable sequentialization tools across several LL fragments.

Abstract

We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic to recover a sequent calculus proof from a proof-structure. We present a geometric condition on untyped proof-structures allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of linear logic for which this property is indeed a correctness criterion. In a suitable fragment of multiplicative linear logic with units, the criterion yields a characterization of the equivalence induced by permutations of rules in sequent calculus. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and it is sufficient for sequentialization in the axiom-free setting.

On the role of connectivity in Linear Logic proofs

TL;DR

This work addresses when a graphical proof structure in linear logic corresponds to a sequent calculus proof by linking a connectivity-based geometric property to correctness. It introduces the untyped sequentiality theorem via a -ps and shows that, inside this framework, the criterion becomes sufficient for sequentialization, even in fragments with units and exponentials. It further develops a canonical jumping mechanism to refine sequentialization in the (NBT)LL fragment and proves that equivalence under rule permutations is tractable within this setting. The approach extends to multiplicative-exponential logic (MELL) and intuitionistic polarizations, including IMELL and ICOMLL, providing a unified, connectivity-driven perspective on sequentialization, cut-elimination stability, and proof-structure equivalence. Overall, the paper contributes practical criteria and constructive procedures for turning geometric properties of proof-structures into reliable sequentialization tools across several LL fragments.

Abstract

We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic to recover a sequent calculus proof from a proof-structure. We present a geometric condition on untyped proof-structures allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of linear logic for which this property is indeed a correctness criterion. In a suitable fragment of multiplicative linear logic with units, the criterion yields a characterization of the equivalence induced by permutations of rules in sequent calculus. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and it is sufficient for sequentialization in the axiom-free setting.

Paper Structure

This paper contains 14 sections, 46 theorems, 11 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Formulae, sequent calculus and proof-structures
  3. Definitions
  4. Desequentialization
  5. Correctness criteria and cut elimination
  6. Untyped sequentiality theorem
  7. The fragment (NBT)LL
  8. Extensions to MELL
  9. The intuitionistic polarization
  10. Technical appendix
  11. Complements of Section 2
  12. Complements of Section 3
  13. Complements of Section 4
  14. Complements of Section 6

Key Result

Proposition 18

Let $R$ be a ps.

Figures (10)

  • Figure 1: Sequent calculus rules.
  • Figure 2: Desequentialization $(\cdot)^\circ$ of sequent calculus proofs in $\mathit{MLL}$ into pss of $\mathit{MLL}$. Double arrows to a $\bullet$ node are a shorthand for an arbitrary number of arcs, each targeting a distinct $\bullet$ node.
  • Figure 3: Two pss satisfying $\mathsf{AC}\mathsf{C}_{\sharp \mathsf{w}}$ which are not sequentializable.
  • Figure 4: A ps for which the splitting is not uniquely determined.
  • Figure 5: From left to right: a $(\neg\mathsf{w}\otimes)$-ps with erasing nodes highlighted, a $\mathsf{w}$-compatible switching, a non-$\mathsf{w}$-compatible switching, a $\mathsf{w}$-switching path, a non-$\mathsf{w}$-switching path.
  • ...and 5 more figures

Theorems & Definitions (120)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Remark 6
  • Definition 7
  • Definition 8
  • Remark 10
  • Definition 11
  • ...and 110 more