💻 computer science

Proof Nets for PiL (Full Version)

This paper introduces proof nets for PiL, an extension of first-order multiplicative additive linear logic that enables a shallow encoding of $\pi$ -calculus processes, and establishes their correctness, sequentialization, and ability to canonically represent sequent calculus derivations modulo rule permutations.

Original authors: Matteo Acclavio, Giulia Manara

Published 2026-05-15

📖 5 min read🧠 Deep dive

CC0 1.0

Original authors: Matteo Acclavio, Giulia Manara

Original paper dedicated to the public domain under CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.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 organize a massive, chaotic construction project. You have a team of workers (processes) who need to build something together. Some workers must work one after another (sequential), some can work at the same time (parallel), and some need to share specific tools (names) without getting confused about who owns what.

In computer science, there is a system called the $\pi$ -calculus that describes how these workers interact. The paper you provided introduces a new way to map these interactions using a logic system called PiL. Think of PiL as a very strict, rule-based language that turns the messy instructions of the construction project into neat, mathematical formulas.

However, just writing down the rules isn't enough. You need a way to check if the plan is valid and to see if two different-looking plans are actually doing the exact same thing. This is where the authors introduce Proof Nets.

Here is a simple breakdown of what the paper does, using everyday analogies:

1. The Problem: Too Many Ways to Say the Same Thing

Imagine you are giving directions to a friend.

Route A: "Turn left, then drive 5 miles, then turn right."
Route B: "Drive 5 miles, then turn left, then turn right."

If the "turn left" and "drive 5 miles" don't depend on each other, both routes get you to the same place. In computer logic, these are called independent rule permutations. They look different on paper, but they mean the same thing in reality.

The problem is that standard logic (like a Sequent Calculus) is like a long, rigid list of instructions. It treats Route A and Route B as completely different documents, even though they achieve the same result. This makes it hard to study the "essence" of the process because you get lost in the paperwork.

2. The Solution: Proof Nets (The "Blueprint")

The authors propose Proof Nets as a solution. Think of a Proof Net not as a list of instructions, but as a blueprint or a flowchart.

The Blueprint: Instead of writing "Step 1, Step 2, Step 3," a blueprint shows all the connections at once. It connects the start to the finish using lines and nodes.
Collapsing the Chaos: If two different lists of instructions (derivations) lead to the same blueprint, the Proof Net treats them as identical. It "collapses" all the different ways of writing the same plan into a single, canonical (standard) object.

3. The Special Ingredients (PiL)

The logic system used here, PiL, has some special tools that make it perfect for describing computer processes:

The "◀" Operator: This is like a "Next" button. It forces things to happen in a specific order (Sequential).
The "New" Quantifier (И): This is like a "Fresh Name" generator. In a busy office, you need to make sure two people don't accidentally use the same temporary ID card. This tool ensures that new names are unique and fresh.
The "Ya" Quantifier (Я): This is the partner to "New," handling the other side of the name-sharing coin.

4. The Three Main Achievements

The paper claims to have built a complete toolkit for these Proof Nets:

A. The "Is It Valid?" Test (Correctness Criterion)
Just because you can draw a blueprint doesn't mean the building will stand. You need a test to see if the blueprint is structurally sound.

The authors created a polynomial-time test (a fast, efficient algorithm) to check if a Proof Net is a valid proof. It's like a structural engineer checking the blueprint for cracks. If it passes, it's a valid proof; if not, it's just a drawing of nonsense.

B. The "Back to Instructions" Translator (Sequentialization)
Sometimes you have the blueprint (Proof Net) and need to turn it back into a list of instructions (Sequent Calculus) to execute it.

The paper provides an algorithm to translate the blueprint back into a step-by-step list. This proves that the blueprint isn't just a pretty picture; it actually contains all the necessary information to run the process.

C. The "Flattening" Procedure (Slice Nets)
Sometimes the blueprints get complicated with too many layers of "and" and "or" connections.

The authors introduce a method called Flattening. Imagine taking a complex, multi-story building plan and flattening it into a single, wide floor plan without losing any structural integrity.
They show that you can always simplify a complex Proof Net into a Slice Net (a flat version) and still know exactly what the process does.

5. Why This Matters (The "Canonicity" Claim)

The paper makes a strong claim about Canonicity.

Local Canonicity: If you swap two independent steps (like turning left before driving vs. driving before turning left), the Proof Net stays the same. It ignores the irrelevant order.
Strong Canonicity: Even if you swap steps that are further apart in the process, the "Slice Net" version stays the same.

In simple terms: The authors have created a system where the "fingerprint" of a process is unique. No matter how you write the instructions, if the underlying logic is the same, the Proof Net (or Slice Net) will look exactly the same. This allows researchers to study the true behavior of computer processes without getting distracted by the different ways people write the instructions.

Summary

The paper introduces a new way to visualize and verify computer processes. It turns messy, rule-heavy instructions into clean, graphical blueprints (Proof Nets). It provides a fast way to check if these blueprints are valid, a way to turn them back into instructions, and a method to simplify them. Most importantly, it proves that these blueprints are the "true identity" of the process, ignoring all the irrelevant ways you could have written the instructions to get there.

Technical Summary: Proof Nets for PiL

Problem Statement
The paper addresses the challenge of providing a canonical, graph-based representation for proofs in PiL, a logical system extending first-order multiplicative additive linear logic (MALL1). PiL was introduced to offer a shallow encoding of processes in the $\pi$ -calculus, specifically to prove the completeness of choreographic programming with respect to race-free, deadlock-free processes.

The core difficulty lies in the unique operators of PiL:

The $\blacktriangleleft$ operator: A non-commutative, non-associative, self-dual connective modeling sequential composition.
Nominal Quantifiers ( $\new$ and $\ya$ ): Quantifiers modeling name binding and freshness, requiring strict bookkeeping of variable usage to ensure names are shared by at most one pair of dual quantifiers.

Existing proof net formalisms for MALL (such as Girard's nets or conflict nets) struggle with the combination of additives, quantifiers, and non-commutative/non-associative connectives. Furthermore, standard sequent calculus derivations suffer from non-canonicity due to independent rule permutations, which obscures the underlying semantics of process execution trees. The paper seeks to define proof nets that collapse these permutations into a single syntactic object while handling the specific constraints of nominal quantifiers and the $\blacktriangleleft$ operator.

Methodology
The authors adopt conflict nets as the foundational framework, extending them to the first-order setting of PiL. The methodology involves three main components:

Structure Definition (Pre-structures and Proof Nets):
- Links and Dualizers: The authors define links (axiomatic connections between sub-sequents) and associate them with dualizers (substitutions). Dualizers map variables in a link to existential or nominal witnesses, enforcing duality and handling the unification required by quantifiers.
- Coco-trees: The underlying structure is a "concord-conflict tree" (coco-tree) where leaves are links and internal nodes are labeled with concord ( $\smile$ ) or conflict ( $\#$ ) relations.
- Coalescence: A rewriting procedure (coalescence) is defined to reduce a proof structure to a trivial form (a single leaf). This process mimics the bottom-up construction of a sequent derivation. A proof net is defined as a proof structure that admits a coalescence path to a trivial pre-structure.
Correctness and Sequentialization:
- A polynomial-time correctness criterion is established: a structure is a valid proof net if and only if it is coalescent.
- A sequentialization procedure is provided, which translates a valid proof net back into a sequent calculus derivation in PiL. This proves the completeness of the net formalism with respect to the logic.
- A proof translation algorithm translates PiL derivations into conflict nets, establishing soundness.
Slice Nets and Flattening:
- To achieve a more canonical form, the authors introduce slice nets, a subclass of conflict nets where the underlying coco-tree is "flat" (containing at most one $\#$ -node at the root).
- A flattening procedure is defined as a rewriting rule that moves concord nodes above conflict nodes. The authors prove that flattening is strongly normalizing, confluent, and preserves coalescence. This allows any conflict net to be transformed into a unique canonical slice net.

Key Contributions

Definition of Conflict Nets for PiL: The paper defines the first proof net formalism for a logic combining additives, first-order quantifiers, and the non-commutative/non-associative $\blacktriangleleft$ connective.
Polynomial-Time Correctness: It provides a polynomial-time correctness criterion (specifically $O(n^5)$ ) based on the coalescence of coco-trees with witness maps.
Sequentialization and Translation: It establishes a bidirectional translation between PiL sequent derivations and proof nets, proving that the nets are both sound and complete.
Canonical Representation (Slice Nets): It introduces slice nets and the flattening procedure, proving that every conflict net reduces to a unique slice net.
Canonicity Results: The paper proves two distinct levels of canonicity:
- Local Canonicity: Conflict nets provide a canonical representation of derivations modulo local rule permutations (independent rule swaps).
- Strong Canonicity: Slice nets provide a canonical representation modulo both local and non-local rule permutations.

Results

Theorem 1: A sequent $\Gamma$ is provable in PiL if and only if there exists a conflict net for $\Gamma$ .
Theorem 2: Flattening preserves coalescence, ensuring that the transformation from conflict nets to slice nets maintains validity.
Theorem 3: A sequent $\Gamma$ is provable in PiL if and only if there exists a slice net for $\Gamma$ .
Theorem 4:
- Two derivations $D$ and $D'$ are locally equivalent ( $D \approx D'$ ) if and only if their associated conflict nets are isomorphic.
- Two derivations $D$ and $D'$ are strongly equivalent ( $D \simeq D'$ ) if and only if their associated slice nets are isomorphic.

Significance and Claims
The paper claims that proof nets for PiL provide a canonical representation of sequent calculus derivations, effectively collapsing classes of derivations that differ only by independent rule permutations. This is significant for the semantics of process calculi because:

It aligns with the semantics of execution trees in the $\pi$ -calculus, where the order of independent actions should not affect the process's meaning.
It distinguishes between local canonicity (relevant where the order of branching matters) and strong canonicity (relevant for equivalences like bisimulation where branching order is irrelevant).
It offers a foundation for developing new tools to study the semantics of concurrent systems and choreographies by treating proof nets as representatives of execution trees, ignoring irrelevant interleavings while preserving observable phenomena like race conditions.

The authors explicitly state that they do not study cut-elimination in this work, as their focus is on cut-free proofs representing computation trees. They note that cut-elimination for PiL involves non-trivial handling of nominal quantifiers and stores, which is left for future work. Similarly, while they suggest their framework could be extended to general first-order MALL, they do not claim to have solved the general case in this paper.