ch:supercompilation: recursive whistle decisions

Problem, result, and invariant. Classify a new process-tree configuration as fold, whistle, or drive without mistaking mere growth for a repeated state. Maintain the decision order: variant equality has priority, then an ancestor-to-current homeomorphic embedding fires the whistle, and only the remaining pair is driven. A generalization witness must reconstruct both compared trees after its holes are instantiated.

Representation tradeoff. Represent the finite signature by Tree = Hole | Num Numeral | Succ Tree | Pair Tree Tree, where Numeral is unary. The fixed finite constructor set makes Kruskal’s hypothesis visible and removes binding from the executable boundary. It cannot represent SC-CBV configurations with environments, let-bound variables, or evaluation contexts. A binding-tree or de Bruijn representation would cover the source calculus, but it would need renaming-aware variant equality and a finite-label encoding before the homeomorphic-embedding argument applies.

First complete version. Implement structural equality and a decision function with only fold and drive. If the ancestor and current tree are equal, return Fold; otherwise return Drive. This minimal version already reports the variant fixture correctly and fixes the priority that the final decision procedure must preserve.

Remaining cases. Implement homeomorphic embedding in rule order. A variable hole couples with a variable hole, every numeral couples with every numeral, diving recurses into a child of the current tree, and coupling requires equal constructor heads plus recursive embedding of corresponding children. In particular, nullary equal heads succeed; a hole does not embed an arbitrary tree merely because it is a hole. Insert the whistle branch after the fold branch. Finally compute a one-hole most-specific generalization for the two growth fixtures and check both substitution instances rather than printing a canned claim. This last check is the executable image of the two reconstruction equations in lemma 128.5. Finally execute the bounded driving projection: contract a call-by-value beta redex, contract a known constructor case, split an open case, render the resulting process tree and residual case, check one map–append fusion equation, and reject an unsafe fold whose constructor heads differ. Execute the ordered classifier on one representative state for every R1–R20 rule and A1–A4c alternative.

Observable result. The accepted run first reports three driving decisions, a rendered process tree and residual case, the fusion oracle, and the rejected unsafe fold. It then reports variant: fold, growth: whistle, unrelated: drive, three base-case checks, and msg-witness: valid. The two rule-ledger lines enumerate every rule in source order. The run ends with All 17 Chapter 128 corpus cases passed.

A failing version. Replace the homeomorphic-embedding test by a second equality test. The mutant still typechecks and still folds the variant fixture, so that positive case does not detect the missing whistle. The growth fixture changes to growth: drive; the exact stdout oracle rejects it. A second mutant deletes the beta contraction from the local driver. It changes driver-beta to outside-projection while leaving the whistle cases intact.

Acceptance test. Apply the procedure in subappendix E.6. Require one passing inline test, the exact accepted transcript, and audit []. Replay both mutations, require failure on the growth and beta-driver lines respectively, restore, and rerun all four commands.

Mathematical boundary. The recursive predicate computes homeomorphic embedding for this fixed finite tree syntax and illustrates the whistle premise of theorem 128.4. The generalization fixture illustrates lemma 128.5. The driver is the exact bounded projection named in the chapter: beta, known case, and open case refinement followed by known-case contraction, and one process-tree residualization. The ordered classifier covers the complete rule-selection card but does not recursively execute the full R1–R20/A1–A4c transformer. The corpus proves neither transformation correctness, termination, nor the may-termination and strong-improvement results.