ch:proof-nets: ch:proof-nets

Problem, result, and invariant. The task is to implement the direct switching checker of definition 40.18, followed on positive inputs by the chapter’s reverse sequentialization procedure. For each switching, depth-first search maintains this invariant: the visited vertices are exactly the explored part of the root component; every visited nonroot has its recorded parent edge; and an edge to a visited nonparent vertex is a cycle witness. When search ends, an unvisited vertex is a disconnection witness. The observable result records acceptance or the first rejection reason and switching number; positive cases also record the reconstructed rule count.

Representation. Give every formula occurrence a stable natural-number identifier. Store axiom and tensor-premise edges in one fixed-edge list, but store each par link as a root with its left and right premise identifiers. A structure also records its vertices, tensor links, and conclusion roots. This representation makes one switching an ordinary undirected graph obtained by choosing exactly one edge from each par link.

Using formula text as the vertex identity is a tempting alternative, but it collapses distinct occurrences of the same atom and can create or destroy paths spuriously. Stable occurrence identifiers make graph equality and the parent-edge test independent of printed formula names.

First complete version. Start with neighbors and the mutually recursive visit/visitNeighbors. Ignore the edge back to the recorded parent; reject any other already visited neighbour as a cycle. After the search, compare the visited set with the complete vertex set to detect disconnection. This is already a complete checker for a structure with no par links.

Next implement enumerate. Process par links in a fixed order and recurse first on the left edge and then on the right. Stop at the first failed switching, retaining its one-based count and reason; accept only after every bit vector has passed. This supplies the promised direct $O(2^{k}n)$ algorithm for $k$ par links and $n$ graph size.

Remaining cases. For reverse sequentialization, first remove a conclusion par. If none exists, try conclusion tensors in stable order: delete one tensor root and its incident edges, compute the two connected components, restrict the structure to each component, and recurse only when both are nonempty proof structures. A single axiom is the base case. Count one reconstructed rule at every successful axiom, par, or tensor step. Explicit fuel exposes a defective recursive decomposition; it is not a logical rejection reason.

A failing version. A checker that inspects only the first switching accepts the structure PN-LAST-CYCLE-16: its first fifteen switchings are trees, while the all-right vector 1111 fails at switching $16$. This mutation shows why the universal quantifier in the correctness criterion must become an exhaustive enumeration. A second common error is to treat the parent edge as a revisit; even the two-vertex axiom graph is then reported cyclic.

Acceptance test. The permanent corpus must report exactly the following semantic outcomes:

• PN-CORRECT-2 accepts two switchings and reconstructs four rules.

• PN-CYCLIC-1 rejects switching one for a cycle.

• PN-DISCONNECTED-4 rejects switching one for disconnection.

• PN-FOUR-PAR-16 accepts sixteen switchings and reconstructs thirteen rules.

• PN-LAST-CYCLE-16 rejects switching sixteen for a cycle.

Thus the accepted run reports five passing cases. Appendix E supplies the source pin, commands, complete transcript, audit result, and mutation record.

Mathematical boundary. The implementation realizes the reference algorithm of proposition 40.19. Five finite executions do not prove correctness for every proof structure, sequentialization, cut elimination, confluence, or the asymptotic bound. They test the representation and selected cases; the chapter supplies the mathematics.