Sequent reconstruction in LLM -- A sweepline proof (Q1892938): Difference between revisions

Proof-nets for linear logic are defined as certain (inductively defined) graph structures satisfying a further (topological) correctness criterion. The criterion makes the construction of inductive arguments over proof-nets difficult. The fact that to any proof-net there corresponds a proof in the standard sequent presentation of the logic, is known as the sequentialization theorem, for which we know several proofs, all non-trivial. The paper gives a new proof of the theorem, applying a technique well-known in computational geometry (sweepline algorithms), which exploits the graphical nature of the nets. The sequent proof is reconstructed by processing the proof-net one slice at a time, starting with the top (at the axioms) and proceeding downwards. The crucial notion for this approach to work is that of standard layout of a proof-net (informally, each premise of a node lies above the node; the conclusion of a node lies below the node; for any par-node, all the other nodes which contribute to the construction of the formulas in the par lie above the par). Main (but not difficult) result of the paper is that any proof- net has a standard layout. At this point the sweepline algorithm is almost obvious. The paper starts with the pure multiplicative case. Then it covers the multiplicative constants and the exponentials. The unit for par and the weakening are treated by extending the proof-nets with a new kind of link (the probe), which ensures connectedness. With probes, the Danos-Regnier criterion holds also for constant and exponential proof- nets.