💻 computer science

Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic

This paper introduces the VMELL fragment of multiplicative exponential linear logic, which unifies classical and intuitionistic polarizations and establishes a computationally efficient correctness criterion by extending the Danos-Regnier property to characterize bang calculus terms via proof-nets.

Original authors: Raffaele Di Donna, Giulio Guerrieri, Lorenzo Tortora de Falco

Published 2026-07-23

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Raffaele Di Donna, Giulio Guerrieri, Lorenzo Tortora de Falco

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to solve a massive, tangled knot of string. In the world of computer science and logic, this "string" is a proof—a step-by-step argument that a computer program or a mathematical statement is correct. For decades, mathematicians have used a special kind of map called a "proof-net" to untangle these knots. Think of a proof-net not as a straight line of text, but as a complex, multi-dimensional web where different parts of the argument connect in surprising ways. The big challenge has always been figuring out which of these tangled webs are actually valid proofs and which are just messy scribbles that look like proofs but aren't.

To make sense of this, logicians have developed "correctness criteria," which are like rulebooks for checking the map. The most famous rulebook says that a valid map must be "acyclic" (no loops that go round and round forever) and "connected" (you can walk from any point to any other point without lifting your foot). This works perfectly for simple logic, but when we add more powerful tools to the mix—tools that let us copy or delete parts of the argument—the old rules start to break. Suddenly, we have maps that look valid but are actually broken, or maps that are valid but look like they have disconnected islands. The question becomes: How do we fix the rulebook so it works for these more complex, powerful systems without getting lost in the mess?

This paper, titled "Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic," tackles exactly that problem. The authors, Raffaele Di Donna, Giulio Guerrieri, and Lorenzo Tortora de Falco, are exploring a specific type of logical system called Multiplicative Exponential Linear Logic (MELL). They introduce a new, slightly tweaked rule for checking if a proof-net is valid. Instead of demanding that the whole map be perfectly connected, they propose a more flexible rule: the number of disconnected islands on the map should be exactly one more than the number of "trash cans" (nodes that delete information) on the map.

Here is the twist: The authors prove that while this flexible rule is necessary (you can't have a valid proof without it), it isn't sufficient on its own for the entire system. There are still some tricky, invalid maps that pass this test. However, they discover a special "geometric restriction"—a way of coloring the connections on the map with "input" and "output" labels—that acts like a filter. When they apply this filter, they find a specific, notable fragment of logic they call VMELL. In this VMELL world, their flexible rule becomes a perfect, one-to-one test: if a map passes the rule, it is definitely a valid proof, and if it fails, it's definitely not.

This discovery is a big deal because VMELL is a "unifying" territory. It sits right at the crossroads where two different ways of thinking about logic—called "intuitionistic" (which is like a strict, step-by-step construction) and "classical" (which allows for more dramatic, "either-or" jumps)—meet and shake hands. Before this, these two worlds were often studied separately with their own different rulebooks. The authors show that in VMELL, their new connectivity rule works for both sides simultaneously.

Furthermore, the paper connects this abstract logic to the actual code we write every day. They demonstrate that this VMELL fragment is the perfect home for the "bang calculus," a powerful programming tool that can simulate both "call-by-name" (where you wait to see if you need a value before calculating it) and "call-by-value" (where you calculate it immediately). They provide a way to translate computer programs written in these styles directly into these proof-net maps. They prove that when a computer program runs and simplifies itself (a process called reduction), it is exactly mirrored by the process of cutting and simplifying the knots in the proof-net map.

In short, the paper doesn't just fix a rulebook; it builds a bridge. It shows that by looking at the geometry of how these logical maps are connected, we can create a single, efficient, and reliable system that handles both classical and intuitionistic logic, and even serves as a universal translator for different styles of computer programming. The authors have proven that for this specific, well-behaved fragment of logic, checking if a proof is real is as simple as counting the islands and the trash cans, making a complex logical puzzle much easier to solve.

Technical Summary: Connectivity at the Crossroad of Intuitionistic and Classical Polarizations in Linear Logic

Problem Statement

The paper addresses the fundamental problem of correctness criteria for proof-structures in Multiplicative Exponential Linear Logic (MELL). While proof-nets (graph-based representations of proofs) offer a richer syntax than sequent calculus, not all proof-structures represent valid proofs. The standard correctness criterion for the purely multiplicative fragment (MLL) is the Danos-Regnier criterion (ACC), which requires that every switching graph of a proof-structure be acyclic and connected.

In MELL, the presence of the weakening rule and the bottom constant ( $\bot$ ) breaks the connectivity requirement. Consequently, the property AC (acyclicity only) is often used, but it characterizes proofs only in an extended sense (allowing the mix rule). A necessary condition for a MELL proof-structure to represent an actual proof is the property $ACC^\sharp_w$ : every switching graph must be acyclic, and the number of connected components ($cc$) must satisfy the equation $cc = w + 1$, where $w$ is the number of nodes corresponding to weakening or bottom.

However, $ACC^\sharp_w$ is known to be necessary but not sufficient for sequentializability (recovering a sequent calculus proof) in general MELL, as demonstrated by specific counterexamples. The paper seeks to identify a geometric restriction on proof-structures where $ACC^\sharp_w$ becomes a sufficient correctness criterion, thereby recovering a computationally efficient verification method without resorting to non-canonical "jumps."

Methodology

The authors employ a geometric and structural approach to proof-nets, focusing on polarization and connectivity:

Untyped Geometric Analysis: The authors first analyze untyped proof-structures. They introduce a "pure polarization" discipline, assigning input ( $i$ ) and output ( $o$ ) labels to arcs based on local constraints (Figure 5). This creates polarized proof-structures.
The $i/o$ Graph: For a polarized ground-structure, they define an $i/o$ graph ( $G^{i/o}$ ) by erasing input premises of specific nodes ( $\parr_o$ ) and reversing the orientation of input arcs. They define a new property $ACC^{i/o}$ , requiring this specific graph to be acyclic and satisfy a connectivity condition related to classical and output nodes.
The $\parr_o$ -terminal Condition: A crucial geometric restriction is introduced: a proof-structure is $\parr_o$ -terminal if the conclusion of every $\parr_o$ node is a premise of another $\parr_o$ node or an output node ( $\bullet$ ).
Equivalence Proof: The core technical method involves proving that for $\parr_o$ -terminal polarized proof-structures, the complex property $ACC^\sharp_w$ (checking all switching graphs) is equivalent to the simpler, linear-time checkable property $ACC^{i/o}$ .
Typed Fragments and Calculi: The authors define a new fragment of MELL, VMELL, which unifies classical and intuitionistic polarizations. They then translate the bang calculus (a unifying calculus for call-by-name and call-by-value $\lambda$ -calculi) into proof-nets of VMELL, specifically into a sub-fragment called !MELL.

Key Contributions

1. The Fragment VMELL and Correctness Criterion

The paper introduces VMELL, a fragment of MELL containing both classically and intuitionistically polarized formulae.

Result: For any $\parr_o$ -terminal proof-structure in VMELL (specifically those without axiom cuts and multiplicative cuts), the property $ACC^\sharp_w$ is a correctness criterion.
Significance: This turns a necessary condition into a sufficient one for a notable fragment. Furthermore, checking $ACC^\sharp_w$ for these structures becomes linear time relative to the size of the proof-structure, as it is equivalent to checking $ACC^{i/o}$ (Remark 22).

2. Unification of Polarizations

The work demonstrates that connectivity naturally appears at the "crossroad" of classical and intuitionistic polarizations.

Classical Case: In the classical polarized fragment ( $MELL_{pol}$ ), $ACC^\sharp_w$ is equivalent to Laurent's correctness criterion.
Intuitionistic Case: In the intuitionistic fragment ($IMELL $),$ ACC^\sharp_w$ characterizes the single-output property essential to intuitionistic logic.
Synthesis: VMELL allows these two polarizations to coexist, and the geometric condition $ACC^\sharp_w$ serves as the unified correctness criterion for this combined setting.

3. Bang Calculus and Proof-Nets

The paper provides a precise characterization of the bang calculus (which subsumes call-by-name and call-by-value $\lambda$ -calculi) within the framework of proof-nets.

Translation: They define a translation of typed bang calculus terms into bang proof-nets (proof-nets of !MELL).
Factorization: They prove that this translation factorizes Girard's two standard translations of the $\lambda$ -calculus (call-by-name and call-by-value) into linear logic. Specifically, the translation of a $\lambda$ -term via the bang calculus embedding coincides with the direct Girard translations (Theorem 45).
Simulation: They prove that reduction steps in the bang calculus are simulated by a finite number of cut-elimination steps in the corresponding proof-nets (Theorem 43).
Characterization: They provide an explicit geometric characterization of the proof-nets that represent bang calculus terms (Theorem 44), identifying them as the $m$ -normal forms of specific translations.

Results

Theorem 21: Establishes that for $\parr_o$ -terminal polarized proof-structures, $ACC^\sharp_w \iff ACC^{i/o} \iff$ Sequentializability.
Corollary 35: Confirms that $ACC^\sharp_w$ is a correctness criterion for cut-free (or $m$ -normal) proof-structures in VMELL.
Theorem 43 & 45: Demonstrate the dynamic and static correspondence between the bang calculus and proof-nets, showing that the bang calculus acts as a unifying layer for CbN and CbV $\lambda$ -calculi within the proof-net framework.
Complexity: The verification of correctness for the identified fragments is reduced from exponential (checking all switchings) to linear time (checking the $i/o$ graph).

Significance and Claims

The paper claims that its primary contribution is identifying VMELL as a fragment where the geometric property of connectivity ( $ACC^\sharp_w$ ) is not just necessary but sufficient for sequentializability. This resolves a long-standing issue where $ACC^\sharp_w$ was known to be insufficient in general MELL.

The authors emphasize that this result:

Reconciles Polarizations: It shows that classical and intuitionistic polarizations can coexist in a single fragment where a unified geometric correctness criterion applies.
Computational Efficiency: It provides a linear-time algorithm for checking correctness in this fragment, avoiding the need for complex "jump" mechanisms often used to restore connectivity.
Logical Foundation for the Bang Calculus: It establishes the bang calculus as a natural inhabitant of the proof-net world, providing a unified logical setting for studying both call-by-name and call-by-value evaluation strategies. The paper explicitly states that the translation of the bang calculus into proof-nets "factorizes" the two Girard translations, offering a "fine-tuned (logical) setting" to study these calculi uniformly.

The paper concludes modestly, noting that while the current work focuses on the multiplicative and exponential fragments, future work will investigate extending these results to the additive fragments and further exploring the quotient on bang terms induced by the proof-net translation.