A Formal Model of A New
Linear Time Correctness
Condition for Multiplicative
Linear Logic
Satoshi Matsuoka
AISTMotivation• Can specify many computational problems by Linear Logic
formulas• Be able to specify many NP-complete problems using MLLformulas• Can Use Proof Search as Problem Solving• Proof Net Construction: a method of LL Proof Search Construct a proof structure associated with the input specification
formula,and then check whether it is a proof net using a correctness

condition

Efficient (Linear Time) Correct Condition is a Key

Brief History of CCs of MLL proof nets
• 1987: Girard
Introduction of Proof NetsLong Trip Condition for unit-free Multiplicative Linear Logic (MLL)• 1989: Danos & Regnier
Acyclic & Connected Condition over DR-graphs• 1999: Guerrini
The First Linear Time Correctness Condition based on Danos’s
Contractability Condition• 2000: Murawski & Ong
Another Linear Time Correctness Conditions based on Lamarche’s
Condition of IMLL proof nets
• 2007: de Naurois & Mogbil
New Correctness Condition Establishing NL-completeness: we only needjust one DR-graphOur result• A new linear time correctness condition based on de Naurois &Mogbil‘s work• Introduction of deNM-trees• Rewriting system over deNM-trees with three rewrite rules• Use of union-find data structures in order to establish linear timetermination• Introduction of deadlock prevention mechanism in order toestablish completeness of the algorithm• Easy to implement (in Proof Net Calculator)• A formal model (a finite transition system) based on theimplementation

The system MLL
MLL formulas:
Inference rules:

are multisets of MLL formulas

Linkspremises

pp

A

B&A

ID-Links

Par-Links

BABA

B

conclusions

MultiplicativeLinks
Tensor-Links

MLL proof structures• A set of links• Satisfying two conditions:
1. any formula (occurrence) is a conclusion of exactly one link
2. any formula (occurrence) is at most one premise of a link

MLL Proof Nets
• Abstract formal proofs of Multiplicative Linear Logic• Sequentializable MLL proof structures

Definition of Proof Nets:
Sequentializability

A DR-switching S for a proofstructure Θ• A function from the set of par-links in Θ to {Left,Right}

The DR graph ΘS induced by DRswitching S

A Graph-theretic characterization of proof nets
• Theorem (Girard, Danos-Regnier)
A MLL proof structure Θ is a MLL proof net
ifffor any DR-switching S for Θ,the DR-graph ΘS is acyclic and connectedOur new linear time correctness condition
1. Given an MLL proof structure Θ
2. Select a DR-switching S for Θ
3. If the DR-graph S(Θ) is not acyclic and connected, then Θis not a proof net
4. Otherwise, construct the deNM-tree T for Θ and S,

1. check whether or not T can reduce to exactly one node deNM-tree
using three rewrite rules
2. If it succeeds, then Θ is a proof net3. Otherwise, not a proof net

deNM-trees• Trees consisting of the following two types of nodes:&S is a set of labels lL or rL where L is a-link

Example 1: An MLL proof net

Example 1: its deNM-treeRewriting System• Rewriting System over deNM-trees• Only three rewrite rules• Choose an active (labeled) node arbitrarily

Three rewrite rules
union-elimination&local jump

Example 1: its deNM-tree

Example 1: the reduced one node deNM-tree

Example 2: An MLL proof structure, but not PNExample 2: its deNM-tree

activeExample 2: the reduced deNM-tree
activeactiveRemark• Any naïve implementation has worst cases terminating inquadratic time
• Need of more sophisticated data structures: union-find datastructures

Union-Find Data Structures• Maintenance of a partition on a finite set S = {a1, a2, …, an}:• Each partition (subset) Sa of S has the representative element a• union(a, b): makes the union set Sa ∪Sb, whereSa (resp. Sb) is the current subset including a (resp. b)• find(a): return the representative element b of Sb that includes a• Can check whether two elements a and b belong to thesame partition• Runs in almost linear time (in the sense of amortized cost)• Runs in linear time over special cases, especially over trees

Our finite transition system• States denotes the current active nodemaintains the information about labeled node idenotes the representative element of the partition including imaintains the information about -node jetc.

Our transition system (Cont.)• Four transition rules:-elimination rewrite rule is divided into two transition rules• Use of union-find data structuresunion operation in union transition rulefind operation in two -elimination transition rules for the elimination
condition
find operation in local jump transition rule in order to find the next active node
• Each transition rule only uses constant number of Union-Find operations⇒
Linear time termination

Deadlock prevention mechanism• Without it, we would judge that correct proof nets were not:can not establish completeness of the algorithm• Realized by queue data structures and union-find datastructures

Indices for not yet eliminated -nodes are maintained inqueues• Its correctness (deadlock freedom) can be stated by aliveness property:“Indices for not yet eliminatedin some queues”-nodes must be always

Additional Results• (Yet another) linear time sequentialization algorithm
Easy to implement
The basic idea is to repeat linear time CC twice• Linear time algorithm for automated generation of planar
proof nets
can be reduced to decremental graph connectivity
problemOur implementation• Can be downloaded fromhttps://staff.aist.go.jp/s-matsuoka/PNCalculator/index.html
as a software package called Proof Net Calculator

Future Work
• Incorporation of backtracking mechanism
Seeking elegant (verifiable) implementation• Semi-persistent data structures?
• Extensions to other fragments and/or variants of LL

Thank you