ch:bunched-implications: ch:bunched-implications

Problem, result, and invariant. Implement the finite BI checker and resource evaluator specified by the seminar project. The finished program distinguishes additive and multiplicative bunch constructors both proof theoretically and semantically. Maintain these invariants:

1. additive and multiplicative ACU comparison never crosses an alternation boundary;

2. weakening and contraction are accepted only where a one-hole context displays an additive child;

3. And-R combines its premise antecedents with semicolon, while Star-R combines them with comma; and

4. forcing reuses one world for $\wedge$, searches decompositions for $\ast$, tests accessible worlds for $\to$, and tests composed resources for $-\ast$.

The observable result is an exact thirteen-line report and one summary line. The inline oracle compares the complete output and requires exit status zero.

Representation. Use ordinary Kappa datatypes for formulas, bunches, one-hole contexts, derivation trees, validation results, finite worlds, and finite models. Bunch contexts have four recursive constructors, one for each side of semicolon and comma; plug makes the scope of a structural rule explicit. Represent inference by either Invalid or $\mathtt{\text{Valid}}(\mathrm{\Gamma },A)$, carrying the inferred antecedent and succedent. Each rule constructor then checks its premises, compares the required bunch shape modulo the appropriate ACU laws, and constructs its conclusion.

Explicit rule trees are preferable here to proof search. Search would obscure whether a rejected specimen failed because of its proposed rule shape or because another branch was chosen. Negative multiplicative structural proposals are therefore checked by a separate function; they are not constructors masquerading as rules of ${\mathsf{LBI}}_0$.

First complete version. Start with atoms, bunch leaves, one-hole contexts, atomic identity, and additive weakening. Implement plug structurally. The first end-to-end specimen is $$P;Q⊢P,$$ represented as DWeak Hole (Leaf P) (Leaf Q) (DId P). The checker infers $P⊢P$, verifies that the premise antecedent is the context filled by $P$, and returns the context filled by $P;Q$.

Implement ACU equality next. Simplify only a matching unit, flatten every maximal node of one constructor, and compare its recursively normalized children as a multiset. The recursion into multiset elements preserves every alternation boundary. The specimen $$(A;B),(C;D)\not\equiv (A,C);(B,D)$$ must already be rejected.

Structural and logical cases. Add contraction by checking that the premise antecedent contains $\mathrm{\Delta };\mathrm{\Delta }$ at the displayed hole. The permanent case constructs $(P;P),Q⊢P\ast Q$ and contracts only the left additive child. Keep multiplicative weakening and contraction out of the derivation datatype; the separate proposal checker returns false for both tags.

Add And-R and Star-R. Their distinction is load bearing and follows the live calculus exactly: $$\frac{\mathrm{\Gamma }⊢A\mathrm{\Delta }⊢B}{\mathrm{\Gamma };\mathrm{\Delta }⊢A\wedge B}\frac{\mathrm{\Gamma }⊢A\mathrm{\Delta }⊢B}{\mathrm{\Gamma },\mathrm{\Delta }⊢A\ast B}.$$ The premise antecedents need not be equal. The additive rule combines them with semicolon; contraction is a separate explicit rule when a shared assumption is to be recovered from two additive copies. The accepted Kappa constructor DAndR therefore returns AddB leftBunch rightBunch; DStarR returns the corresponding MulB.

Add And-L, Star-L, Imp-R, and Wand-R. These reconstruct the mixed formula: weaken the two atomic branches, combine them with Star-R, package both additive subtrees with And-L, then apply Wand-R and Imp-R. Replacing either bunch constructor makes that named case fail.

Finite forcing. Use the numeric fuel only as an internal work bound. Atomic forcing, accessibility, and composition are finite model tables. Additive conjunction evaluates both operands at one world. Multiplicative conjunction enumerates two resources, checks the operands separately, composes the resources, and compares the composition with the target. Additive implication enumerates accessible worlds; the wand enumerates every resource forcing its antecedent and checks the consequent after composition.

The truncated-addition model supplies the four positive semantic distinctions. At world $1$, $P\wedge Q$ is true but $P\ast Q$ is false; at world $2$, the split $1\circ 1=2$ makes the star true. The implication cases use $P$ and $Z$ as in the chapter. Equality-preordered ${\mathbb{Z}}_2$ supplies the structural countermodel: world $0$ forces $P\ast Q$ through $1+1=0$, but does not force $P$.

Fuel exhaustion must return a conservative failure in the finite program, but it is not a logical counterexample. The fixed value 240 is accepted only for the permanent named corpus; this tutorial makes no decision-procedure claim for arbitrary external input.

Three failing versions. Keep each defect at one Boolean mutation point:

1. enabling multiplicative weakening makes its permanent rejection fail;

2. identifying the two bunch constructors erases the alternation tree and makes the interchange specimen congruent; and

3. interpreting $\ast$ by same-world conjunction makes the split and finite countermodel cases fail.

Each mutant still parses and typechecks. The unchanged stdout oracle fails, and main raises the typed acceptance error because the conjunction of case booleans is false.

Acceptance test. The restored source reports, in order: purely additive conjunction; nested additive weakening; nested additive contraction; rejection of multiplicative weakening; rejection of multiplicative contraction; a valid multiplicative split; rejected interchange; the mixed derivation; the two conjunction semantics; the two implication semantics; and the finite weakening countermodel. The final line is

All 13 Chapter 43 corpus cases passed.

After testing all three mutations separately, restore the accepted source and repeat check, test, run, and audit. Appendix E records the current pin, commands, concise oracle, and evidence boundary.

Mathematical boundary. The rule-tree checker illustrates definition 43.5; ACU comparison illustrates definition 43.3; finite evaluation illustrates definition 43.26, proposition 43.30. Thirteen finite cases do not prove congruence completeness, identity expansion, cut elimination, soundness, elementary completeness, or decidability of BI. The chapter proves only its stated disjunction-free completeness theorem locally; full disjunctive completeness remains the external boundary of convention 43.41. It also does not implement Moore closure, the universal BI algebra, algebraic soundness, reflection, or the semantic cut certificate of section 43.5; those are proof objects and mathematical constructions, not finite execution claims.