ch:recursive-types: ch:recursive-types
Problem, result, and invariant. Implement three deliberately separate finite engines: eager iso-recursive typing and reduction, equality of contractive regular type descriptions, and a call-by-name PCF observer. The result is the six-case report in appendix E. The central invariant is that operational contraction never enters the type- equality worklist.
Representation. Represent explicit fold and unfold in an eager term syntax, regular types by finite recursive descriptions, and PCF by a separate term and stack datatype. The regular checker carries a queue of node pairs and a visited-pair cache; the PCF evaluator carries fuel whose exhaustion is an inconclusive result.
First complete version. Type a folded one-cell natural list, contract its explicit unfold, and replay the typed two-step recursive cycle. For type equality, reject an unguarded recursive binder before unfolding and accept equal ordinary constructors by placing their children on the work queue.
Remaining cases. When a regular pair has already been visited, accept that comparison branch; otherwise record it before descending. Check the alpha-variant streams and a product/sum mismatch. In the separate PCF machine, evaluate recursive addition to five and report finite exhaustion for
A failing version. Refuse every revisited regular-type pair. The checker still typechecks but rejects the equal cyclic streams. Disabling the fold/unfold contraction and making
Acceptance test. Run the four gates in appendix E and require six exact PASS lines plus an empty audit. Replay the three recorded mutations one at a time; each must typecheck and fail the frozen stdout oracle before the accepted source is restored.
Mathematical boundary. The finite engines illustrate fold/unfold traces, one visited-pair equality calculation, and two PCF approximants. They prove neither type safety, regular-tree equality soundness or completeness, domain adequacy, divergence, nor step-indexed compatibility.