ch:focusing-proof-search: ch:focusing-proof-search

Problem, result, and invariant. The task is to turn definition 39.21 into a finite search program without treating Kappa’s own typechecker as a logical oracle. The program has two phases. It first constructs every focused sequent reachable by one bottom-up rule step from the root. It then computes the least set of those candidates closed under rule conclusions. The invariant is correspondingly two-part:

1. every premise stored in the rule graph is itself a reachable candidate;

2. every candidate admitted to the known set has a stored rule instance all of whose premises were already known at an earlier saturation stage.

The concrete result is a decision and, for accepted examples, rule codes that expose the selected phase transitions.

Representation. Use a tagged data type Formula with one constructor for every positive and negative connective. Keep persistent negative hypotheses and positive suspensions distinct in Hyp; represent the ordered inversion queue by a list; and represent right focus, inversion, and left focus by the three constructors of Sequent. A RuleInstance stores a rule code and its list of premises. Structural equality on these finite data types makes sequent membership decidable.

A direct representation by partial proof trees looks simpler, but duplicates the same subgoal each time a cycle reaches it and supplies no stable object to memoize. The finite rule graph separates discovery from provability: the graph may contain cycles, while its least fixed point still has a precise meaning.

First complete version. Implement structural equality and a membership-tested insertion operation before implementing any interesting rule. Then define rules so that it returns all bottom-up rule instances for one sequent. The worklist procedure reachable removes one pending sequent, skips it if it is already in seen, otherwise inserts it and appends every premise returned by rules. This establishes the first invariant by construction.

For the second phase, let round scan the finite universe and insert a candidate when someRuleKnown finds a rule whose premises all belong to known. Begin with the empty known set: nullary rules enter in the first round. Repeat until two consecutive sets are extensionally equal. Fuel is retained only to expose a bug in graph finiteness or fixed-point iteration; fuel exhaustion is never reported as underivability.

At this point a small end-to-end version can already accept an atomic identity and reject an unsupported atom. Test that version before adding compound connectives.

Remaining cases. Add rules in the same phase order as the calculus: deterministic queued-left inversions, stable right rules, right-focus choices, releases and suspensions, and finally left-focus rules. Preserve both alternatives for disjunction and both projections for negative conjunction. The forced example records the codes $$34,26,21,21,33,31,16,$$ so moving a focus transition in front of the inversion prefix is observable. The two disjunction branches must expose codes $13,14$, and the two negative-conjunction projections codes $44,45$.

A failing version. Delete the membership test before adding a newly discovered candidate. The hypothesis $\downarrow p^{-}\Rightarrow p^{-}$ then recreates the same sequent, the worklist never closes, and the cyclic test reports fuel exhaustion rather than ordinary rejection. This input distinguishes memoized graph closure from unbounded tree unfolding. As a second mutation, replace the second disjunction rule by the first; the right-injection input then fails while the left-injection input continues to pass.

Acceptance test. The seven named cases must have these outcomes:

• Forced inversion accepts with the seven rule codes above.

• Left and right disjunction accept with codes $13$ and $14$.

• The first and second negative-conjunction cases accept with codes $44$ and $45$.

• The cyclic implication rejects without fuel exhaustion.

• The unsupported atom rejects without fuel exhaustion.

The accepted run therefore reports seven passing cases. Appendix E records the pinned program, commands, complete output, and audit result.

Mathematical boundary. This program illustrates the finite saturation construction used in theorem 39.23. Its executions do not prove that the mathematical candidate space is finite, that saturation is exact, or that focalization relates the focused and ordinary calculi. Those are theorems of the chapter, not consequences of a successful corpus run.