Recursive types, domains, and general recursion

Chapter 12 keeps two calculi separate. The eager ${\lambda }_{\mu }^{\mathsf{iso}}$ fragment inherits $\mathbf{1}$, products, sums, and arrows, and locally adds $\mathbb{N}$, numerals, and explicit fold/unfold. Its only new root is E-UnfoldFold. The call-by-name ${\mathsf{PCF}}_{\mathsf{n}}$ fragment has only naturals, arrows, successor, predecessor-binding zero test, lambda, application, and typed fix. PCF has no argument context; the eager calculus evaluates both application positions. No adequacy or strategy theorem is silently transferred between them.

Type substitution, term substitution, and folded canonical forms are lemma 24.3, lemma 24.4. Preservation, deterministic progress, and finite safety are theorem 24.5. These results permit divergence: ${\mathrm{\Omega }}_D:\mathbb{N}$ has a typed two-step cycle. More strongly, for every closed function value $v$, the generic term ${\mathsf{Fix}}_{A}v$ diverges under the eager call-by-value strategy because evaluation repeatedly demands its recursive argument. The eta-delayed operator $\mathsf{Z}$ is the separate repair at function type; its exact pointwise and contextual boundaries are recorded below.

This is a separate closed, contractive finite-graph problem. Decision of bisimilarity $A{\equiv }_{\mu }B$ for that exact grammar is theorem 24.8. It is equality, not subtyping, and does not add a conversion rule to the iso-recursive calculus. Unguarded expressions such as $\mu X.X$ are outside both the algorithm and theorem.

PCF substitution is part of lemma 24.12. The same lemma proves preservation, deterministic progress, and natural canonical forms. The selected roots are P-Beta, P-SuccN, P-IfZ, P-IfS, and P-Unroll. The chapter gives a complete terminating trace for addition and the exact one-step self-loop $$\mathsf{fix}x:\mathbb{N}.x⟼\mathsf{fix}x:\mathbb{N}.x.$$ Fuel exhaustion in the executable companion is only a finite observation, never a proof of divergence.

All order theory is specialized to omega-chains. Product order is componentwise, sums are separated, liftings add a fresh bottom, and continuous function spaces use pointwise order and lubs. The local development proves the constructor and function-space facts in lemma 24.14, lemma 24.15. Pairing, evaluation, and currying are lemma 24.16. Kleene leastness and continuity of the fixed-point operator are theorem 24.17, lemma 24.20; parameterized fixed points and admissible induction are lemma 24.21, lemma 24.22. No theorem about arbitrary directed joins is claimed.

The sole solved recursive domain is the partial natural-list cpo $\mathcal{L}$. Its elements, order, truncations, compact elements, and continuous inverse maps $$\mathcal{L}\cong (\{\ast \}+\mathbb{N}\times \mathcal{L}{)}_{\mathrm{\perp }}$$ are fixed by definition 24.23, proposition 24.28. The singleton $\{\ast \}$ is a carrier poset, not the object type $\mathbf{1}$. Proposition 24.29 relates only hole-free finite domain lists to canonical eager $\mathsf{ListNat}$ values. Infinite and holed domain elements are deliberately not eager returned values.

The object type $\mathbb{N}$ denotes the flat carrier ${\mathbb{N}}_{\mathrm{\perp }}$, and arrows denote continuous function spaces. The natural successor and case maps are strict. Every displayed semantic clause is well defined and continuous by lemma 24.31, lemma 24.33. Semantic substitution and reduction invariance are lemma 24.34. The logical approximation is admissible, including at arrows, and its fundamental theorem is theorem 24.38. Computational adequacy theorem 24.39 is exactly for closed terms of PCF natural type; it is not full abstraction and gives no adequacy result for the eager recursive calculus.

The exact call-by-value fragment and its complete context grammar are fixed in convention 24.40. Value equivalence ${\approx }_n^A$ consumes an index at $\mu$ and quantifies over all smaller tests at arrows. Term equivalence ${\mathcal{E}}_n^A$ compares both terminating traces shorter than the index. The well-founded measure is lexicographic in index, type size, and value/term phase. Trace decomposition and the proof-complete package of downward closure, value-to-term closure, two-sided finite anti-reduction, related substitution, and evaluation-context compatibility are lemma 24.43, lemma 24.47.

The eta-delayed operator ${\mathsf{Z}}_{A,B}$ satisfies only the pointwise common- reduct statement of proposition 24.49; a diverging function context separates the un-applied equation. The recursive list copier does satisfy structural convergence on every canonical finite input, and indexed anti-reduction yields the natural-result contextual biconditional of lemma 24.50, theorem 24.51. That biconditional preserves numeral results but does not promise convergence in a context that diverges independently.

Safety, partial correctness, termination, finite-tail productivity, and totality have the separate definitions and witnesses of definition 24.53, proposition 24.54. Productivity is a property of $\mathcal{L}$ via Obs-Zero and Obs-Cons, not the return of an eager infinite value. If unrestricted Pr-Fix is admitted at proposition types, $\mathsf{fix}p:P.p$ inhabits every $P$, including the empty type, while looping. Hence the extension is operationally type safe but not a total propositions-as-types core.

The pinned Kappa companion in appendix E represents the eager iso-recursive checker/evaluator, contractive regular equality, and the call-by-name PCF machine as object-language nominal data. Its six cases and three semantics mutations test only the displayed finite examples. They are not proofs of the metatheorems above or of Kappa itself.