ch:recursive-functions: ch:recursive-functions
Problem, result, and invariant. Accept a mutually recursive component only when every internal call carries a predecessor certificate. Maintain the invariant that a lexicographic scan accepts at its first strict coordinate, continues only across equal coordinates, and rejects immediately at an earlier increase.
Representation tradeoff. A full implementation could store source terms and replay typed subterm proofs. The companion stores a finite call graph whose edges carry a list of Strict, Same, or Increase changes. Proof objects would support kernel replay; the change list keeps the decisive lexicographic control flow explicit and gives deterministic negative tests.
First complete version. Implement the coordinate scan before graph traversal. The empty list fails; Strict succeeds; Same recurses; and Increase fails without inspecting later entries. Treat a direct-child structural call as the one-coordinate list [Strict]. Then compute the components. Two vertices share one exactly when each reaches the other by at least one edge, so a reachability closure suffices; bound it by the vertex count, since the reachable set grows monotonically inside the vertex list and therefore stabilizes after one round per vertex. Require the certificate predicate on exactly the edges whose endpoints share a component.
Remaining cases. Represent even–odd by its two predecessor edges, and add a third edge to an auxiliary base that increases its argument. That call leaves the component, so it carries no obligation — which is precisely what the component computation must decide. Add a reset example whose later increase follows an earlier strict decrease, a same-argument edge, and a later-coordinate-only edge. The program checks the certificate logic rather than parsing Timpl clauses.
Observable result. The accepted program prints two accepted groups and two edge-specific rejections, each edge read out of the graph. Its terminal line is
Two failing versions. Change the Increase branch so that it continues scanning; the mutant accepts a later decrease masked by an earlier increase. Then, separately, drop the component filter so that every call site must descend; the mutant rejects even-odd on its call to base. Without the second mutation the component computation could be deleted without any test noticing.
Acceptance test. Run the four commands in subappendix E.5. Require a passing check, one passing inline test, the exact five-line run transcript, and an empty audit. Replay each mutation, require rejection by the stdout oracle, restore the source, and repeat all four commands.
Mathematical boundary. The scan implements the finite certificates of definition 123.4 and illustrates the premise of lemma 123.12. It does not synthesize accessibility proofs, type translated bodies, or prove termination for arbitrary recursive programs.