A Linear Time Algorithm for
Automatic Generation ofMultiplicative Planar Proof
Nets
Satoshi MatsuokaAISTMotivation• Discovery of a new linear time correctness condition for MLLproof nets
• Efficient implementation (in Proof Net Calculator)• Found a theory bug in the first implementation: may result in deadlock• The second implementation seems correct: adding a deadlock prevention
mechanism• Formal verification (not yet, but seems to be OK by using an easystate machine encoding)• Testing using test data
• Effective test data generation: automatic generation of MLL proofnetsThe system MLL
MLL formulas:
Inference rules:

are multisets of MLL formulas

MLL Proof Nets
• Abstract formal proofs of formulas of Multiplicative LinearLogic• A subset of the set of MLL proof structures• Sequentializable MLL proof structures

Linkspremises

pp

A

B

A&A

ID-Links

Par-Links

B

MultiplicativeLinks

B
Tensor-Links

A

B

conclusions

MLL proof structure• A set of links• Satisfying two conditions

Cond. (1): any formula (occurrence) is aconclusion of exactly one link

Cond.(2): any formula (occurrence) does not
become a premise of more than one link

MLL proof structures (but not MLLproof nets)

MLL Proof Structure(also MLL proofnet)

1 =Definition of Proof Nets:
Sequentializability

A DR-switching S for a proofstructure • A function from the set of par-links in  to {L, R}

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 netifffor any DR-switching S for ,the DR-graph S is acyclic and connectedA DR-graph of 1

Another DR-graph of 1

An MLL proof structure (But not an
MLL proof net)

2 =

A DR graph for 2

Another DR-graph for 2

A new linear time correctness condition• Given an MLL proof structure • Select a DR-switching S for • If the DR-graph S() is not acyclic and connected then  is not aproof net• Otherwise, construct the deNM-tree T for  and S,
1.
2.
3.

check whether or not T can reduce to one node using three rewrite rules
If it succeeds, then  is a proof net
Otherwise, not a proof net• To establish linear time termination, must use union-find datastructure

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Three rewrite rules
union-elimination&local jump

Example 1: An MLL proof net

Example 1: its deNM-tree (by extremely leftswitching)Example 2: An MLL proof structure, but not PN

Example 2: its deNM-tree (by extremely leftswitching)Example 2: the reduced deNM-tree

Union-Find Data Structure• Dynamic operations on a finite set S = {a1, a2, …, an}:• Make-Set(x): creates the singleton set {x}• Union(x, y): makes the union set Sx ∪Sy, whereSx (resp. Sy) is the current subset including x (resp. y)• Find-Set(x): return the representative element of Sx• Can check whether or not two elements x and y belong to thesame subset of S currently• Runs in almost linear time (in practical sense)• Runs in linear time over special cases, especially over planargraphs

A new linear time correctness condition• Found bugs twice (at this moment)• The first bug was a trivial mistake• Then the algorithm was implemented• The second bug was a subtle one:found it through a comparison test with an existing
quadratic correctness condition• Hope that the current one is the last one• Would like to confirm its correctness through tests

The goal• Generation of a number of MLL proof structures but notproof nets
• The implementation must answer “no” for these• This part is relatively easy

• Generation of a number of MLL proof nets
• The implementation must answer “yes” for these• This part is not so easy, especially for generating big proof nets

Generation of general MLL proof structures
1. Generation of one-conclusion pre proof structure P
2. Assignment of multiplicative links to P

One-conclusion pre proof structure• binary tree with even-number leavesplus• fixpoint free involution over the leaves• Can be easily extended to connected multi-conclusion preproof structures

Binary tree with even-number leaves

A simple observation about binary tree witheven-number leaves• When a binary tree has 2n leaves, the tree has 2n-1 internal
nodesfixpoint free involution over an even cardinal set

One conclusion pre proof structureOne conclusion proof structure• One conclusion pre proof structureplus• An assignment of { , } to the internal nodes• An assignment of {+, -} to the leaves• An assignment of an appropriate fixpoint involution&

A necessary condition for a one conclusion
MLL proof net• numID = num&

• num

ID= num+1

Random generation of MLL proof structures• Generate a random binary tree with even-number leaves• Generate an assignment of multiplicative links to internal
nodes satisfying the necessary condition• Generate an appropriate fixpoint free involution with polarity• Can generate MLL proof structures, but very few MLL proofnets

Inductive definition of MLL proof nets

Use of ind. def. of MLL PNs for test data gen.
• Closely related to Galton-Watson branching processes

Proof Net Generation from connected multiconclusion pre proof structures (connected prePSʼs)) = halt) = let n be

Gen(…

&Gen(and Gen(…

…

)

…

nGen(

= let n beandGen()…
n…

) and Gen(…

)Remarks• A forest can be linear-ordered in a bottom up manner by
topological sort in linear time• Naïve implementation of the Gen procedure is quadratic:connected check at each recursive step
• We have found a linear time Gen procedure:
but in the special case, i.e., in the planar casePlanar pre proof structureQuiz• Can you find a solution?
• Hint: use of union-find data structureOur solution• Get attention to faces• Observations:
1. Each internal node has at most three faces
2. Each conclusive internal node has (necessarily not different) two(up and down) faces

Case 1: removal of conclusion node results in
two connected components

f2

The up face is the same as the down facef1

In this case, Find-Set(f1) == Find-Set(f2)Case 2: Otherwisef2

The up face is not the same as the down facef1

In this case, Find-Set(f1) != Find-Set(f2)Case 2: Otherwise (Cont.)

Execute Union(f1, f2)

Question• How can we assign faces to a pre proof structure?

Our answer• Use of union-find data structureStep 1: Assign numbers to the regions in an
input binary tree

73138

14

1115

16

9412

10
652

3

10Step 2: Assign polarities to the leaves
Positive leaf must connect to negative leaf in order to be planar (necessarycondition)+

3-++

78+--+
13+
14-+
15-

+
11-

94

12

10
652

3

10+
16-

Step 3: applying union operation to regions
Left region of left conclusion is unified to right region of right conclusion
Right region of left conclusion is unified to left region of right conclusion+3-++

78+--+
13+14-+15-+11-

94

12

106

52+
16

310

Execute Union(3, 12) and Union(11, 16)-Open Question• Generalization to the non-planar case
• A special case to a general open question (decremental graphconnectivity problem)• Already in quadratic time
• Embedding into general surfaces and applying similar methods inlinear time?