Chapter 24Core route

Recursive Types, Domains, and General Recursion

A finite simple type can describe one list cell, two list cells, or any other fixed number of cells. It cannot describe the type of all finite lists by repeating itself finitely many times. The equation $L ≅ 1 + (N \times L)$ says what is missing: the type being defined occurs in its own description. Such a self-referential type expression is a recursive type. One programming interpretation makes the crossing between a recursive type and one unfolding of its body observable. The equi-recursive alternative in section 24.2 instead identifies their regular unfoldings.

Crossing a recursive equation explicitly

The calculus $λ_{μ}^{iso}$ is the eager simply typed calculus with $1$ , $2$ , $N$ , products, sums, arrows, and the two term forms ${fold}_{μ X . A} e$ and $unfold e$ . Type variables are bound only by $μ$ . It is an iso-recursive calculus: crossing the recursive equation requires an explicit fold or unfold term.

Definition 24.1 — The eager iso-recursive calculus ¶

The complete type and term grammars are $\begin{aligned} A, B ::= & 1 ∣ 2 ∣ N ∣ X ∣ A \to B ∣ A \times B ∣ A + B ∣ μ X . A, \\ e ::= & x ∣ unit ∣ tt ∣ ff ∣ n ∣ λ x : A . e ∣ e_{1} e_{2} ∣ if (e; e_{1}; e_{2}) \\ ∣ ⟨ e_{1}, e_{2} ⟩ ∣ fst e ∣ snd e ∣ inl e ∣ inr e \\ ∣ case e of {inl x \mapsto e_{0}; inr y \mapsto e_{1}} \\ ∣ {fold}_{μ X . A} e ∣ unfold e . \end{aligned}$ Types are identified up to alpha-renaming, but $μ X . A$ is not judgmentally equal to $A [μ X . A / X]$ . The type formers have their syntax-directed formation rules. Recursive types are formed by

Δ, X ⊢ A type

Δ ⊢ μ X . A type

Mu-F

Rule Mu-F requires the body to be a type under the bound type variable. Term typing is the least judgment containing the following rules: $\begin{matrix} \frac{x : A \in Γ}{Γ ⊢ x : A}, Γ ⊢ unit : 1, Γ ⊢ tt : 2, Γ ⊢ ff : 2, Γ ⊢ n : N, \\ \frac{Γ, x : A ⊢ e : B}{Γ ⊢ λ x : A . e : A \to B}, \frac{Γ ⊢ e_{1} : A \to B Γ ⊢ e_{2} : A}{Γ ⊢ e_{1} e_{2} : B}, \\ \frac{Γ ⊢ e : 2 Γ ⊢ e_{1} : A Γ ⊢ e_{2} : A}{Γ ⊢ if (e; e_{1}; e_{2}) : A}, \\ \frac{Γ ⊢ e_{1} : A Γ ⊢ e_{2} : B}{Γ ⊢ ⟨ e_{1}, e_{2} ⟩ : A \times B}, \frac{Γ ⊢ e : A \times B}{Γ ⊢ fst e : A}, \frac{Γ ⊢ e : A \times B}{Γ ⊢ snd e : B}, \\ \frac{Γ ⊢ e : A}{Γ ⊢ inl e : A + B}, \frac{Γ ⊢ e : B}{Γ ⊢ inr e : A + B}, \\ \frac{Γ ⊢ e : A + B Γ, x : A ⊢ e_{0} : C Γ, y : B ⊢ e_{1} : C}{Γ ⊢ case e of {inl x \mapsto e_{0}; inr y \mapsto e_{1}} : C} . \end{matrix}$ The recursive introduction and elimination rules are

Γ ⊢ e : A [μ X . A / X]

Γ ⊢ {fold}_{μ X . A} e : μ X . A

T-Fold

Γ ⊢ e : μ X . A

Γ ⊢ unfold e : A [μ X . A / X]

T-Unfold

The type context $Δ$ is used only for formation; every term judgment has well-formed types under the ambient $Δ$ , suppressed when empty.

Values and call-by-value evaluation contexts are exactly $\begin{aligned} v ::= & unit ∣ tt ∣ ff ∣ n ∣ λ x : A . e ∣ ⟨ v_{1}, v_{2} ⟩ ∣ inl v ∣ inr v ∣ {fold}_{μ X . A} v, \\ E ::= & [] ∣ E e ∣ v E ∣ if (E; e_{1}; e_{2}) ∣ ⟨ E, e ⟩ ∣ ⟨ v, E ⟩ \\ ∣ fst E ∣ snd E ∣ inl E ∣ inr E \\ ∣ case E of {inl x \mapsto e_{0}; inr y \mapsto e_{1}} \\ ∣ {fold}_{μ X . A} E ∣ unfold E . \end{aligned}$ The compatible closure uses precisely these root contractions:

(λ x : A . e) v ⟼ e [v / x]

E-Beta

if (tt; e_{1}; e_{2}) ⟼ e_{1}

E-IfTrue

if (ff; e_{1}; e_{2}) ⟼ e_{2}

E-IfFalse

fst ⟨ v_{1}, v_{2} ⟩ ⟼ v_{1}

E-Fst

snd ⟨ v_{1}, v_{2} ⟩ ⟼ v_{2}

E-Snd

case (inl v) of {inl x \mapsto e_{0}; inr y \mapsto e_{1}} ⟼ e_{0} [v / x]

E-CaseL

case (inr v) of {inl x \mapsto e_{0}; inr y \mapsto e_{1}} ⟼ e_{1} [v / y]

E-CaseR

unfold ({fold}_{μ X . A} v) ⟼ v

E-UnfoldFold

In particular, the payload of a fold is evaluated before the folded term is a value. No other root or evaluation-context form belongs to this calculus.

Referenced from 3 locations

Put $ListNat : = μ X . (1 + N \times X) .$ Its two constructors are ordinary terms: $\begin{array}{rcl} nil & : = & {fold}_{ListNat} (inl unit), \\ cons & : = & λ n : N . λ x s : ListNat . {fold}_{ListNat} (inr ⟨ n, x s ⟩) . \end{array}$ Rule T-Fold checks the first payload at $1 + N \times ListNat$ , and it checks the second at the same type through its right summand. A list case is an abbreviation: $caseList e of {nil \mapsto e_{0}; cons (n, x s) \mapsto e_{1}}$ is defined by the sum case $case (unfold e; u . e_{0}; z . e_{1} [(fst z) / n] [(snd z) / x s]),$ where $u$ and $z$ are fresh. The cons branch projects $n$ and $x s$ from the ordinary product. If the branch uses only $x s$ , substitution leaves only the $snd$ projection. Put $p = inr ⟨ 3, nil ⟩$ . Then $\begin{aligned} caseList (cons 3 nil) of {nil \mapsto nil; cons (n, x s) \mapsto x s} \\ \overset{t w o β s t e p s f o r cons}{⟼^{2}} case (unfold ({fold}_{ListNat} p); u . nil; z . snd z) \\ \overset{E - U n f o l d F o l d}{⟼} case (p; u . nil; z . snd z) \\ \overset{r i g h t s u m - β}{⟼} snd ⟨ 3, nil ⟩ \overset{snd - β}{⟼} nil . \end{aligned}$ For a numeral $n$ and term $e$ , write $cell (n, e) : = {fold}_{ListNat} (inr ⟨ n, e ⟩) .$ The term $cell (n, v)$ is a canonical list value when $v$ is one. By contrast, the curried term $cons n v$ takes two beta steps to that value.

Exercise 24.1 ¶

★☆☆ Draw the complete typing derivation for $cons 3 nil$ , then write every reduction in the displayed list case. Name the unique use of E-UnfoldFold.

Referenced from 3 locations

Finite unfolding does not solve the original problem. If $L_{0} = 1$ and $L_{k + 1} = 1 + N \times L_{k}$ , then $L_{k}$ represents at most $k$ cons cells. The constructor for a $(k + 1)$ -st cell expects $L_{k}$ , not $L_{k + 1}$ , so no fixed member of this sequence is closed under lists of arbitrary finite length. The fold packages all finite unfoldings behind one type.

Safety survives the equation

The recursive-type binder requires type substitution; lambda and branch binders require term substitution.

Lemma 24.2 — Composition of distinct type substitutions ¶

If $X \neq Y$ and $Y \notin FV (B)$ , then $(E [D / Y]) [B / X] = E [B / X] [D [B / X] / Y] .$ The equation holds for every type expression $E$ after alpha-renaming its bound variables away from $B$ and $D$ .

Referenced from 4 locations

Proof of Lemma 24.2 — Composition of distinct type substitutions

Proof. Induct on $E$ . At a variable, the cases $E = X$ , $E = Y$ , and $E \notin {X, Y}$ are the two substitution definitions; the side condition $Y \notin FV (B)$ closes the case $E = X$ . Arrows, products, and sums apply the induction hypotheses componentwise. For $E = μ Z . C$ , choose $Z \notin FV (B) \cup FV (D) \cup {X, Y}$ , apply the induction hypothesis to $C$ , and restore the same $μ Z$ binder. ◻

Lemma 24.3 — Type and term substitution ¶

The following hold, after alpha-renaming bound variables away from the substituend.

If $Δ_{0}, X, Δ_{1} ⊢ A type$ and $Δ_{0} ⊢ B type$ , then $Δ_{0}, Δ_{1} ⊢ A [B / X] type$ .
If $Δ_{0}, X, Δ_{1}; Γ ⊢ e : A$ and $Δ_{0} ⊢ B type$ , then $Δ_{0}, Δ_{1}; Γ [B / X] ⊢ e [B / X] : A [B / X]$ .
If $Γ, x : A ⊢ e : B$ and $Γ ⊢ v : A$ , then $Γ ⊢ e [v / x] : B$ .

Referenced from 5 locations

Proof of Lemma 24.3 — Type and term substitution

Proof. Items 1 and 2 are simultaneous inductions on formation and typing. The new formation case is $μ Y . C$ . Choose $Y \neq X$ fresh for $B$ ; the induction hypothesis forms $C [B / X]$ under the substituted context extended by $Y$ , then Mu-F forms $μ Y . C [B / X]$ . For T-Fold, the induction hypothesis gives $Γ [B / X] ⊢ e [B / X] : (C [μ Y . C / Y]) [B / X] .$ By lemma 24.2, with $D = μ Y . C$ and the chosen $Y \neq X$ , the required equation is $(C [μ Y . C / Y]) [B / X] = C [B / X] [μ Y . C [B / X] / Y],$ which is exactly the premise of the substituted T-Fold. The T-Unfold case uses this equation in the opposite direction. All inherited binders use the same alpha-renaming convention.

Item 3 is induction on the typing derivation. Fold and unfold do not bind term variables. Apply the induction hypothesis to their premises and restore the same last rule. The lambda case is the inherited capture-avoiding case. ◻

Lemma 24.4 — Folded canonical forms ¶

If $\cdot ⊢ v : μ X . A$ , then $v = {fold}_{μ X . A} w and \cdot ⊢ w : A [μ X . A / X]$ for some value $w$ .

Referenced from 4 locations

Proof of Lemma 24.4 — Folded canonical forms

Proof. Inspect the value forms. Unit, numerals, lambdas, pairs, and injections have different outer type constructors by inversion of their introduction rules. The only remaining value form is a fold. Inverting its typing derivation gives the payload judgment. There is no subsumption rule in $λ_{μ}^{iso}$ , so no final rule hides the constructor. ◻

Theorem 24.5 — Preservation, progress, and safety ¶

For $λ_{μ}^{iso}$ :

if $\cdot ⊢ e : A$ and $e ⟼ e^{'}$ , then $\cdot ⊢ e^{'} : A$ ;
if $\cdot ⊢ e : A$ , then $e$ is a value or some $e^{'}$ satisfies $e ⟼ e^{'}$ ;
consequently, every finite evaluation of a closed well-typed term ends in a value or can take another step.

Referenced from 6 locations

Proof of Theorem 24.5 — Preservation, progress, and safety

Proof. Preservation is induction on the reduction derivation. The inherited beta, projection, and case roots use lemma 24.3, item 3. Compatible steps restore the corresponding typing rule. The only new root has a typing derivation ending $\frac{\frac{\cdot ⊢ v : A [μ X . A / X]}{\cdot ⊢ {fold}_{μ X . A} v : μ X . A} T - Fold}{\cdot ⊢ unfold ({fold}_{μ X . A} v) : A [μ X . A / X]} T - Unfold .$ The reduct is $v$ , and the inner premise types it at $A [μ X . A / X]$ .

Progress is induction on typing. In the fold case, the payload either steps, with that step lifted by the fold context, or is a value, making the whole fold a value. In the unfold case, the scrutinee either takes a lifted step or is a value. In the latter alternative, lemma 24.4 writes it as a folded value, and E-UnfoldFold applies. The inherited eliminators use their ordinary canonical-form clauses from lemma 2.22; the product, sum, Boolean, and natural-number extensions use the identical rule-inversion schema for their introduction forms. Item 3 follows by induction on the length of a finite evaluation, alternating items 1 and 2. ◻

Exercise 24.2 ¶

★☆☆ Redo the E-UnfoldFold preservation case when the recursive body is $N \times X + 1$ . Display the substitution instance in the premise and explain why no type equality rule is used.

Referenced from 3 locations

Safety is not normalization

Let $D : = μ X . (X \to N), δ : = λ x : D . (unfold x) x .$ Because $D$ unfolds to $D \to N$ , $δ : D \to N$ , and ${fold}_{D} δ : D$ . Thus $Ω_{D} : = δ ({fold}_{D} δ) : N .$ Its evaluation repeats a two-step cycle: $\begin{aligned} δ ({fold}_{D} δ) & ⟼ (unfold ({fold}_{D} δ)) ({fold}_{D} δ) \\ ⟼ δ ({fold}_{D} δ) . \end{aligned}$ The term is safe by theorem 24.5 and does not normalize. The negative occurrence of $X$ in $X \to N$ , not recursive syntax by itself, enables the loop. The decisive point is local: $\cdot ⊢ δ ({fold}_{D} δ) : N$ follows from T-Fold, T-Unfold, and T-App. No dynamic cast, blame rule, or gradual calculus is used.

More generally, put $\begin{aligned} D_{A} & = μ X . (X \to A), \\ δ_{f} & = λ x : D_{A} . f ((unfold x) x), \\ {Fix}_{A} & = λ f : A \to A . δ_{f} ({fold}_{D_{A}} δ_{f}) . \end{aligned}$ Then ${Fix}_{A} : (A \to A) \to A$ . For every closed function value $v : A \to A$ , its call-by-value unfolding reaches $\begin{aligned} {Fix}_{A} v & \overset{β}{⟶} δ_{v} ({fold}_{D_{A}} δ_{v}) \\ \overset{β}{⟶} v ((unfold ({fold}_{D_{A}} δ_{v})) ({fold}_{D_{A}} δ_{v})) \\ \overset{E - U n f o l d F o l d}{⟶} v (δ_{v} ({fold}_{D_{A}} δ_{v})) . \end{aligned}$ The three roots leave the recursive subterm $δ_{v} ({fold}_{D_{A}} δ_{v})$ in argument position. The hypothesis that $v$ is a closed function value is operationally necessary in this eager calculus: an open variable in operator position would be stuck, and a reducible closed operator must first evaluate. More importantly, this is only a compatible-beta fixed point. In call by value, ${Fix}_{A} v$ diverges for every closed function value $v$ . Indeed, put $r = (unfold ({fold}_{D_{A}} δ_{v})) ({fold}_{D_{A}} δ_{v}) .$ Then $r ⟼^{2} v r$ ; evaluation of $v r$ must evaluate $r$ before the beta step can run, and repeats the same demand forever. Thus ${Fix}_{A}$ is not a call-by-value programming recursion operator. The eta-delayed repair $Z$ , which returns a lambda before demanding its recursive argument, is given explicitly in definition 24.48 and used in the list-copy example. If types are read as propositions and the empty type is included, then ${Fix}_{0} (λ x : 0 . x) : 0$ is a closed inhabitant. It diverges rather than producing an empty-type value, but inhabitation alone already invalidates the usual normalization-based consistency argument. Operational type safety and proof-theoretic consistency are different claims. Here the bold glyph $0$ is the empty type; the upright $0$ in the operational examples is the natural-number numeral.

Exercise 24.3 ¶

★★☆ Give the full typing derivation of $Ω_{D}$ , and prove by induction on $k$ that it has a reduction sequence of length $2 k$ returning to its original syntax. Then derive the type and unfolding equation of ${Fix}_{A}$ at a closed function value.

Referenced from 3 locations

Equality of regular recursive descriptions

Equi-recursive equality compares the infinite regular trees generated by two closed contractive type graphs. It changes no fold/unfold typing or reduction rule in $λ_{μ}^{iso}$ .

Definition 24.6 — Contractive regular types and tree equality ¶

A contractive recursive type is one in which every occurrence of the variable bound by $μ X . A$ lies strictly below a product, sum, or arrow constructor. In particular, $μ X . X$ is rejected. Represent a closed type by a finite directed graph: constructor nodes carry their ordered children, and a recursive occurrence points back to its binder’s body node. Unfolding that graph yields a possibly infinite regular tree. For a raw graph node $a$ , write $expose (a) = (κ; a_{1}, \dots, a_{n})$ when following zero or more recursive back-edges first reaches the constructor $κ$ , whose ordered children are $a_{1}, \dots, a_{n}$ . By contractiveness, every back-edge path reaches a constructor, so $expose$ is total. The unfolded tree rooted at $a$ has root $κ$ , and its $i$ -th subtree is rooted at $a_{i}$ . Thus $expose$ maps raw graph nodes to constructor observations; the two sets are distinct.

Define a bisimulation to be a relation on positions of two unfolded trees such that related positions have the same constructor and every pair of corresponding children is again related. Write $A \equiv_{μ} B$ when some bisimulation relates the two roots. Equivalently, bisimilarity is the greatest fixed point of this closure clause; proofs may therefore use coinduction by exhibiting such a relation. Arrow children are compared in their written order; this is equality, not subtyping.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

For example, $μ X . (1 + N \times X) \equiv_{μ} 1 + N \times μ X . (1 + N \times X),$ whereas replacing $N$ by $2$ fails at the first product reached after the right injection.

Definition 24.7 — Worklist equality algorithm ¶

Given roots $a, b$ in finite contractive type graphs, maintain a worklist $W$ of node pairs and a visited set $V$ . Initially $W = [(a, b)]$ and $V = \emptyset$ . Repeatedly remove a pair:

if it belongs to $V$ , continue;
otherwise add it to $V$ , compute $expose (a) = (κ; a_{1}, \dots, a_{n})$ and $expose (b) = (κ^{'}; b_{1}, \dots, b_{m})$ , and reject if $κ \neq κ^{'}$ or $n \neq m$ ;
for matching heads, append every pair of corresponding children.

Accept when the worklist is empty. Contractiveness guarantees that following back-edges reaches a constructor before revisiting the same binder.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Theorem 24.8 — Decision of contractive regular equality ¶

For closed contractive regular types $A, B$ , the worklist algorithm terminates and accepts exactly when $A \equiv_{μ} B$ .

Referenced from 3 locations

Proof of Theorem 24.8 — Decision of contractive regular equality

Proof. Let $N_{A}, N_{B}$ be the finite node sets. A pair is expanded only on its first visit. Hence at most $| N_{A} | | N_{B} |$ iterations expand a pair. Every constructor has arity at most two, so those expansions enqueue at most $2 | N_{A} | | N_{B} |$ pairs in addition to the initial pair; duplicate-removal iterations are therefore finite as well. Contractiveness bounds each head exposure by the finite path to its next constructor, so the whole run terminates.

For soundness, let $V_{f}$ be the final visited set of raw graph-node pairs in an accepting run. If $(a, b) \in V_{f}$ , then $expose (a) = (κ; a_{1}, \dots, a_{n})$ and $expose (b) = (κ; b_{1}, \dots, b_{n})$ , and every child pair $(a_{i}, b_{i})$ was queued and hence lies in $V_{f}$ at termination. Consequently the relation between the unfolded tree positions rooted at pairs in $V_{f}$ is a bisimulation containing the root pair. The unfolded trees are bisimilar.

For completeness, let $R$ be a tree bisimulation containing the roots. Maintain the following invariant: for every queued node pair $(c, d)$ , there are positions $p, q$ in the two unfolded trees such that $(p, q) \in R$ and the subtrees at $p, q$ are rooted by the graph nodes $c, d$ . The initial root pair has these witnesses. When $(c, d)$ is expanded, bisimulation gives equal constructor heads at $p, q$ and relates every pair of corresponding child positions. Those child positions witness the invariant for every enqueued pair. Removing a duplicate changes no remaining witness. The head test therefore never rejects, and termination forces acceptance. ◻

Remark 24.9 ¶

Any fixed fuel bound on textual unfolding can reject equal regular types whose finite graph comparison needs more head exposures than that bound permits. The worklist instead terminates because it expands at most $| N_{A} | | N_{B} |$ distinct node pairs.

Exercise 24.4 ¶

★☆☆ Run the worklist algorithm on $μ X . (N \times X + 1) and N \times μ X . (N \times X + 1) + 1 .$ List the visited pairs. Then replace the right-hand $N$ by $2$ and identify the first rejecting pair.

Referenced from 3 locations

The restriction is load bearing. For $μ X . X$ , head exposure chases the same back-edge without revealing a constructor, so neither the algorithm nor the regular-tree construction of definition 24.6 yields a constructor-headed regular tree. No decidability claim for unrestricted recursive type expressions follows.

A call-by-name language with general recursion

Programming Computable Functions ${PCF}_{n}$ evaluates only the operator of an application; it has no argument evaluation context. We write its step as $⟼$ , reserving $⟼$ for the eager fold calculus.

Definition 24.10 — Call-by-name PCF ¶

The grammar is $\begin{array}{rcl} A, B & ::= & N ∣ A \to B, \\ e & ::= & x ∣ n ∣ succ e ∣ ifz e then e_{0} else x . e_{s} \\ ∣ λ x : A . e ∣ e e ∣ fix x : A . e . \end{array}$ The successor branch binds the predecessor to $x$ . Typing consists of the ordinary variable, numeral, abstraction, and application rules together with

Γ ⊢ e : N

Γ ⊢ succ e : N

P-Succ

Γ ⊢ e : N

Γ ⊢ e_{0} : A

Γ, x : N ⊢ e_{s} : A

Γ ⊢ ifz e then e_{0} else x . e_{s} : A

P-Ifz

Γ, x : A ⊢ e : A

Γ ⊢ fix x : A . e : A

P-Fix

Values are numerals and abstractions. Evaluation contexts are $E ::= [] ∣ E e ∣ succ E ∣ ifz E then e_{0} else x . e_{s} .$ There is no argument context $v E$ . The root rules are

(λ x : A . e) d ⟼ e [d / x]

P-Beta

succ n ⟼ n + 1

P-SuccN

ifz 0 then e_{0} else x . e_{s} ⟼ e_{0}

P-IfZ

ifz (n + 1) then e_{0} else x . e_{s} ⟼ e_{s} [n / x]

P-IfS

fix x : A . e ⟼ e [fix x : A . e / x]

P-Unroll

Compatible closure under $E$ is the one-step relation. Write $e ⇓ n$ when $e ⟼^{*} n$ . Write $e ⟼^{ω}$ when there is an infinite sequence $e = e_{0} ⟼ e_{1} ⟼ e_{2} ⟼ \dots$ .

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

The eager calculus uses $⟼$ ; call-by-name ${PCF}_{n}$ uses $⟼$ .

Lemma 24.11 — Unique call-by-name decomposition ¶

Every closed nonvalue PCF term has at most one decomposition $E [r]$ , where $E$ is an evaluation context of definition 24.10 and $r$ is one of its five root redexes. Consequently it has at most one one-step reduct.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.11 — Unique call-by-name decomposition

Proof. Induct on the term. An application selects its operator until that operator is a lambda, after which the whole application is the unique beta root; there is no argument context. Successor and zero test select their unique scrutinee until it is a numeral, at which point exactly one arithmetic or zero-test root matches. A fixpoint is always the unique unrolling root. Variables cannot occur in a closed term, and values have no decomposition. The context and root alternatives are disjoint in every case. ◻

The predecessor binder keeps recursive arithmetic readable. Define $\begin{aligned} plus : = & fix f : N \to N \to N . \\ λ m : N . λ n : N . \\ ifz m then n else k . succ (f k n) . \end{aligned}$ Write $P$ for this closed fixed-point term and abbreviate $B (m, n) : = ifz m then n else k . succ (P k n) .$ Call by name substitutes an argument before evaluating it: $\begin{aligned} P 2 1 & ⟼ (λ m . λ n . B (m, n)) 2 1 & P - U n r o l l \\ ⟼ (λ n . B (2, n)) 1 & P - B e t a \\ ⟼ B (2, 1) & P - B e t a \\ ⟼ succ (P 1 1) & P - I f S \\ ⟼ succ ((λ m . λ n . B (m, n)) 1 1) & P - U n r o l l \\ ⟼ succ ((λ n . B (1, n)) 1) & P - B e t a \\ ⟼ succ (B (1, 1)) & P - B e t a \\ ⟼ succ (succ (P 0 1)) & P - I f S \\ ⟼ succ (succ ((λ m . λ n . B (m, n)) 0 1)) & P - U n r o l l \\ ⟼ succ (succ ((λ n . B (0, n)) 1)) & P - B e t a \\ ⟼ succ (succ (B (0, 1))) & P - B e t a \\ ⟼ succ (succ 1) & P - I f Z \\ ⟼ succ 2 & P - S u c c N \\ ⟼ 3. & P - S u c c N \end{aligned}$ Each successor branch decreases the first argument and adds one surrounding $succ$ ; the zero branch returns the second argument. Thus the trace reaches $3$ . By contrast, $Ω_{N} = fix x : N . x ⟼ fix x : N . x$ diverges in one repeated step.

Lemma 24.12 — PCF structural and safety properties ¶

The following hold for ${PCF}_{n}$ .

If $Γ, x : A ⊢ e : B$ and $Γ ⊢ d : A$ , then $Γ ⊢ e [d / x] : B$ .
If $Γ ⊢ e : A$ and $e ⟼ e^{'}$ , then $Γ ⊢ e^{'} : A$ .
If $\cdot ⊢ e : A$ , then $e$ is a value or there is a unique $e^{'}$ with $e ⟼ e^{'}$ . A closed value of type $N$ is a numeral.

Referenced from 4 locations

Proof of Lemma 24.12 — PCF structural and safety properties

Proof. Substitution is induction on typing. In P-Ifz, alpha-rename the predecessor binder away from $x$ and the free variables of $d$ , then use the three induction hypotheses. In P-Fix, alpha-rename its binder and apply the induction hypothesis under the extended context. The other cases are the simply typed cases.

Preservation is induction on reduction. Rules P-Beta, P-IfS, and P-Unroll use substitution; the other roots retain the type by inversion. Contexts restore the last typing rule. For progress, inspect the typing derivation. An application first evaluates its function; a closed function value is a lambda, so P-Beta applies without evaluating the argument. Successor and zero test first evaluate their numeral scrutinee. Fix always uses P-Unroll. Unique decomposition is lemma 24.11. Inspecting the value grammar and inverting the last typing rule gives the final natural canonical form. ◻

Exercise 24.5 ¶

★★☆ Repeat the displayed calculation for $plus 1 2$ , naming every root rule and checking that four beta steps occur. Then evaluate $(λ x : N .0) Ω_{N}$ under the displayed call-by-name contexts. If an argument context $v E$ is added and P-Beta is restricted to value arguments for call by value, prove that the same application takes infinitely many steps instead of reaching $0$ .

Referenced from 3 locations

Approximation as an ordered object

A finite evaluator can observe the first $k$ unfoldings of a recursive program. A denotation orders these observations by $⊑_{D}$ and takes their least upper bound. The order $⊑_{D}$ compares definedness inside one domain; it is not a cross-language precision relation.

Definition 24.13 — Pointed omega-cpos and continuity ¶

A poset has a reflexive, transitive, antisymmetric order. An omega-chain is a sequence $d_{0} ⊑_{D} d_{1} ⊑_{D} \dots$ . An omega-cpo has a least upper bound $⨆_{n} d_{n}$ for every omega-chain. A pointed omega-cpo is an omega-cpo with a least element $⊥$ ; a domain here is a pointed omega-cpo.

A monotone function $f : D ⟶ E$ satisfies $d ⊑_{D} d^{'}$ implies $f (d) ⊑_{D} f (d^{'})$ . It is a continuous function when it is monotone and $f (⨆_{n} d_{n}) = ⨆_{n} f (d_{n})$ for every omega-chain. Write $[D ⟶ E]_{c}$ for the continuous functions, ordered pointwise.

An element $c \in D$ is compact when, for every omega-chain $(d_{i})$ , $c ⊑_{D} ⨆_{i} d_{i} ⟹ c ⊑_{D} d_{j} for some j .$ Thus a compact observation below a chain lub already occurs at a finite stage.

Only omega-chains are required. For a monotone countable grid $(a_{i, j})$ , its diagonal is cofinal—every grid entry lies below a diagonal entry—because $a_{i, j} ⊑_{D} a_{k, k}$ whenever $k \geq i, j$ .

Referenced from 2 locations

Recursive Types, Domains, and General Recursion

The flat natural domain adjoins bottom to the discrete set of natural numbers: $N_{⊥} = {⊥} \cup N, ⊥ ⊑_{D} n,$ with no order between distinct naturals. Every chain is either constantly bottom or has indices $i$ and $n$ such that every member from index $i$ onward is $n$ ; its lub is $⊥$ or $n$ , respectively.

The recursive list equation also uses products, separated sums (different tags are incomparable), and a fresh bottom. We fix their orders before using the equation. Let ${*}$ be the singleton poset, and give $N$ the discrete order, in which only equal elements are comparable. The ambient domains determine the omitted order subscripts: $\begin{array}{rcl} (d, e) ⊑_{D} (d^{'}, e^{'}) & ⟺ & d ⊑_{D} d^{'} and e ⊑_{D} e^{'}, \\ inl d ⊑_{D} inl d^{'} & ⟺ & d ⊑_{D} d^{'}, \\ inr e ⊑_{D} inr e^{'} & ⟺ & e ⊑_{D} e^{'}, \end{array}$ with no comparison between the two sum tags. The lifting $D_{⊥} = {⊥} \cup {↑ d ∣ d \in D}$ has $⊥ ⊑_{D} z, ↑ d ⊑_{D} ↑ d^{'} ⟺ d ⊑_{D} d^{'} .$

Lemma 24.14 — Orders used by the recursive equation ¶

If $D$ and $E$ are omega-cpos, then so are $D \times E$ , $D + E$ , and $D_{⊥}$ . Their chain lubs are respectively componentwise, within the unique sum tag, and $⨆_{i} z_{i} = {\begin{cases} ⊥, & z_{i} = ⊥ for every i, \\ ↑ (⨆_{i \geq j} d_{i}), & z_{i} = ↑ d_{i} from some stage j . \end{cases}$ The bottom of a lifting is compact. Compact elements are preserved by pairing, either sum injection, and nonbottom lifting; the element of ${*}$ and every element of discrete $N$ is compact.

Referenced from 5 locations

Proof of Lemma 24.14 — Orders used by the recursive equation

Proof. A chain of pairs projects to two chains, and the pair of their lubs has exactly the required upper-bound property. A chain in a separated sum can never change tags: elements with different tags are incomparable. Its lub is therefore the injection of the lub of its payload chain. A lifting chain is either constantly bottom or, after its first nonbottom member, consists of lifted elements; the stated lub equation is then forced by the upper-bound property. These calculations prove the omega-cpo assertions.

For compactness of a pair $(c, d)$ , suppose $(c, d) ⊑_{D} ⨆_{i} (x_{i}, y_{i})$ . By compactness of $c$ and $d$ , choose $r, s$ with $c ⊑_{D} x_{r}$ and $d ⊑_{D} y_{s}$ ; the stage $max (r, s)$ contains both observations. The sum and nonbottom-lifting claims reduce to compactness of the payload after the chain has entered the matching tag. Bottom lies below stage zero of every lifting chain. A chain in a discrete poset is constant, so its lub is already one of its members. ◻

Lemma 24.15 — Continuous function spaces ¶

If $D$ and $E$ are omega-cpos, then $[D ⟶ E]_{c}$ is an omega-cpo. The least upper bound of a chain $(f_{n})$ is the pointwise map $f (d) = ⨆_{n} f_{n} (d)$ . If $E$ is pointed, its constant-bottom map is the least element.

Referenced from 6 locations

Proof of Lemma 24.15 — Continuous function spaces

Proof. Pointwise monotonicity of $f$ follows from monotonicity of every $f_{n}$ . For a chain $(d_{m})$ , continuity of the $f_{n}$ and monotonicity of the doubly indexed family give $\begin{aligned} f (⨆_{m} d_{m}) & = ⨆_{n} f_{n} (⨆_{m} d_{m}) = ⨆_{n} ⨆_{m} f_{n} (d_{m}) \\ = ⨆_{m} ⨆_{n} f_{n} (d_{m}) = ⨆_{m} f (d_{m}) . \end{aligned}$ The middle exchange is valid because both iterated joins are the least upper bound of the same monotone doubly indexed grid: any upper bound of all $f_{n} (d_{m})$ bounds either iterated join. Pointwise leastness proves that $f$ is the function-space join. The constant-bottom assertion is immediate. ◻

Lemma 24.16 — Continuous pairing, evaluation, and currying ¶

Let $P, D, E$ be omega-cpos.

Identity maps and composites of continuous maps are continuous. Finite products of omega-cpos have componentwise lubs; the empty product is the one-point omega-cpo.
Projections are continuous, and continuous $f : P ⟶ D$ and $g : P ⟶ E$ have continuous pairing $p \mapsto (f (p), g (p))$ .
Evaluation $ev : [D ⟶ E]_{c} \times D ⟶ E, (f, d) \mapsto f (d),$ is continuous.
If $h : P \times D ⟶ E$ is continuous, then every section $d \mapsto h (p, d)$ is continuous and $curry (h) : P ⟶ [D ⟶ E]_{c}, p \mapsto (d \mapsto h (p, d)),$ is continuous.

Referenced from 5 locations

Proof of Lemma 24.16 — Continuous pairing, evaluation, and currying

Proof. Identities preserve every chain lub. If $f$ and $g$ are continuous, then $g (f (⨆_{i} d_{i})) = g (⨆_{i} f (d_{i})) = ⨆_{i} g (f (d_{i}))$ , proving closure under composition. Induction on the number of factors, using the binary-product construction of lemma 24.14, gives finite products; the empty case has one element and its only possible order. The same product lub calculation proves item 2 componentwise. For a chain $(f_{i}, d_{i})$ , continuity of each $f_{i}$ , followed by cofinality of the diagonal in the grid, gives $\begin{aligned} ev (⨆_{i} (f_{i}, d_{i})) & = (⨆_{i} f_{i}) (⨆_{j} d_{j}) = ⨆_{i} ⨆_{j} f_{i} (d_{j}) \\ = ⨆_{k} f_{k} (d_{k}) = ⨆_{k} ev (f_{k}, d_{k}) . \end{aligned}$ Monotonicity is the same two-coordinate comparison, so evaluation is continuous.

For item 4, fixing one coordinate sends a chain in the other coordinate to a chain in the product, and therefore gives a continuous section. For a chain $(p_{i})$ , pointwise function-space lubs and continuity of $h$ give, for every $d$ , $(⨆_{i} curry (h) (p_{i})) (d) = ⨆_{i} h (p_{i}, d) = h (⨆_{i} p_{i}, d) .$ This is the required equality of continuous functions. Monotonicity follows from monotonicity of $h$ . ◻

Theorem 24.17 — Kleene least fixed point ¶

Let $D$ be a pointed omega-cpo and let $F : D ⟶ D$ be continuous. Then $lfp (F) : = ⨆_{n \geq 0} F^{n} (⊥)$ is a fixed point of $F$ , and it lies below every pre-fixed point $d$ satisfying $F (d) ⊑_{D} d$ .

Referenced from 7 locations

Proof of Theorem 24.17 — Kleene least fixed point

Proof. Monotonicity gives the chain $⊥ ⊑_{D} F ⊥ ⊑_{D} F^{2} ⊥ ⊑_{D} \dots$ . Continuity and deletion of its first, least member give $F (lfp F) \overset{c o n t i n u i t y}{=} ⨆_{n} F^{n + 1} ⊥ \overset{d e l e t e t h e l e a s t f i r s t m e m b e r}{=} ⨆_{n} F^{n} ⊥ \overset{d e f i n i t i o n o f lfp}{=} lfp F .$ If $F (d) ⊑_{D} d$ , induction gives $F^{n} ⊥ ⊑_{D} d$ for every $n$ : the base uses bottom, and the step uses monotonicity followed by the pre-fixed-point premise. Least-upper-bound minimality then gives $lfp F ⊑_{D} d$ . ◻

Remark 24.18 ¶

Knaster–Tarski obtains a least fixed point for a monotone endomap of a complete lattice. Theorem 24.17 assumes only a pointed omega-cpo rather than all joins, pays for that weaker carrier with Scott continuity, and gains the explicit approximation formula $⨆_{n} F^{n} ⊥$ . Only the latter omega-chain construction is used in this chapter.

Example 24.19 ¶

Let strict multiplication send $⊥$ to $⊥$ , and define the continuous functional on $[N_{⊥} ⟶ N_{⊥}]_{c}$ by $Φ (f) (⊥) = ⊥, Φ (f) (0) = 1, Φ (f) (m + 1) = (m + 1) \cdot f (m) .$ Writing $⊥_{f}$ for the everywhere-bottom map, its first approximants are $\begin{array}{ccccc} 0 & 1 & 2 & 3 \\ Φ^{0} ⊥_{f} & ⊥ & ⊥ & ⊥ & ⊥ \\ Φ^{1} ⊥_{f} & 1 & ⊥ & ⊥ & ⊥ \\ Φ^{2} ⊥_{f} & 1 & 1 & ⊥ & ⊥ \\ Φ^{3} ⊥_{f} & 1 & 1 & 2 & ⊥ \\ Φ^{4} ⊥_{f} & 1 & 1 & 2 & 6 \end{array}$ In general $Φ^{n} ⊥_{f} (m) = m!$ exactly when $m < n$ , and is $⊥$ otherwise. The pointwise supremum is the total factorial function. This calculation is why the continuous function space is ordered pointwise: each iteration adds one more defined input without changing earlier answers.

Lemma 24.20 — Continuity of the least-fixed-point operator ¶

For a pointed omega-cpo $D$ , the map ${lfp}_{D} : [D ⟶ D]_{c} ⟶ D, F \mapsto lfp (F),$ is continuous.

Referenced from 3 locations

Proof of Lemma 24.20 — Continuity of the least-fixed-point operator

Proof. Let $F_{0} ⊑_{D} F_{1} ⊑_{D} \dots$ and put $G = ⨆_{i} F_{i}$ , using the pointwise function-space join of lemma 24.15. For every $n$ , $G^{n} ⊥ = ⨆_{i} F_{i}^{n} ⊥ .$ First, if $F ⊑_{D} F^{'}$ , then $F^{n} ⊥ ⊑_{D} (F^{'})^{n} ⊥$ for every $n$ : induction on $n$ uses the pointwise inequality at $F^{n} ⊥$ and monotonicity of $F^{'}$ . Hence $(F_{i}^{n} ⊥)_{i}$ is an omega-chain and the displayed lub exists. The displayed equation is proved by induction on $n$ . The zero case is the constant bottom chain. For the step, continuity of $G$ and its pointwise definition give the double join $⨆_{i} ⨆_{j} F_{j} (F_{i}^{n} ⊥)$ . The diagonal terms $F_{k} (F_{k}^{n} ⊥)$ are cofinal: for any $i, j$ , take $k \geq i, j$ and use monotonicity of both the chain of maps and $F_{k}$ . The double join is therefore $⨆_{k} F_{k}^{n + 1} ⊥$ , as required.

Now exchange the two omega-chain joins. Both iterated joins are the least upper bound of the same monotone doubly indexed grid, by the common-upper-bound argument used for function spaces: $lfp (G) = ⨆_{n} ⨆_{i} F_{i}^{n} ⊥ = ⨆_{i} ⨆_{n} F_{i}^{n} ⊥ = ⨆_{i} lfp (F_{i}) .$ Thus ${lfp}_{D}$ preserves omega-chain lubs; monotonicity follows from the same iterate comparison. ◻

Lemma 24.21 — Parameterized least fixed points ¶

Let $P$ be an omega-cpo, let $D$ be a pointed omega-cpo, and let $Φ : P \times D ⟶ D$ be continuous. For $p \in P$ , put $F_{p} (d) = Φ (p, d), μ Φ (p) = lfp (F_{p}) .$ Then every $F_{p}$ is continuous and $μ Φ : P ⟶ D$ is continuous.

Referenced from 5 locations

Proof of Lemma 24.21 — Parameterized least fixed points

Proof. The section $F_{p}$ is continuous by lemma 24.16. Monotonicity of $μ Φ$ follows by induction on the Kleene iterates: if $p ⊑_{D} q$ , then $F_{p}^{n} ⊥ ⊑_{D} F_{q}^{n} ⊥$ for every $n$ , and taking lubs preserves the inequality.

Let $p_{0} ⊑_{D} p_{1} ⊑_{D} \dots$ , put $p = ⨆_{i} p_{i}$ , and write $a_{i, n} = F_{p_{i}}^{n} ⊥$ . Induction on $n$ proves $F_{p}^{n} ⊥ = ⨆_{i} a_{i, n} .$ The zero case is the constant-bottom chain. For the successor case, the pairs $(p_{i}, a_{i, n})$ form a chain: monotonicity in $i$ was proved in the preceding paragraph. Continuity of $Φ$ and the induction hypothesis now give $F_{p}^{n + 1} ⊥ = Φ (⨆_{i} p_{i}, ⨆_{i} a_{i, n}) = ⨆_{i} Φ (p_{i}, a_{i, n}) = ⨆_{i} a_{i, n + 1} .$ The family $a_{i, n}$ is increasing in both indices. Hence its two iterated lubs are the least upper bound of the same set of elements. Using the displayed equality, $μ Φ (p) = ⨆_{n} ⨆_{i} a_{i, n} = ⨆_{i} ⨆_{n} a_{i, n} = ⨆_{i} μ Φ (p_{i}) .$ Thus $μ Φ$ preserves omega-chain lubs and is continuous. ◻

Lemma 24.22 — Admissible fixed-point induction ¶

Let $D$ be a pointed omega-cpo, let $F : D ⟶ D$ be continuous, and let $P \subseteq D$ contain $⊥$ , be closed under lubs of omega-chains, and satisfy $d \in P \Rightarrow F d \in P$ . A subset containing bottom and closed under omega-chain lubs is called admissible. Then $lfp F \in P$ .

Referenced from 3 locations

Proof of Lemma 24.22 — Admissible fixed-point induction

Proof. Induction gives $F^{n} ⊥ \in P$ for every $n$ . Closure under the chain’s least upper bound gives the conclusion. ◻

Continuity cannot be weakened to monotonicity in Kleene’s calculation. On the chain $0 ⊑_{D} 1 ⊑_{D} \dots ⊑_{D} ω$ , define $H (n) = 0 (n < ω), H (ω) = 1.$ This map is monotone, but $H (⨆_{n} n) = 1 \neq 0 = ⨆_{n} H (n) .$ Thus the step that moves $F$ through the lub genuinely uses continuity.

Exercise 24.6 ¶

★★☆ Assume $F (d) = d$ . Without citing the leastness conclusion of theorem 24.17, prove by induction that $F^{n} ⊥ ⊑_{D} d$ for every $n$ , and then use the defining least-upper-bound property to derive $lfp (F) ⊑_{D} d$ . Then find a monotone but discontinuous map on an omega-cpo for which the displayed continuity calculation fails. For the second part, use the chain $0 ⊑_{D} 1 ⊑_{D} \dots ⊑_{D} ω$ and test whether an input has reached its limit.

Referenced from 3 locations

One recursive domain equation

Finite eager lists are not closed under chain lubs. Their increasingly defined prefixes form the chain $⊥ ⊑_{D} cons (0, ⊥) ⊑_{D} cons (0, cons (0, ⊥)) ⊑_{D} \dots,$ but no eager finite list is its least upper bound: every finite candidate reveals only a bounded prefix or ends in $nil$ . Completing the order forces the infinite all-zero sequence. More generally, compatible prefixes determine one natural number at each revealed position, hence an infinite limit sequence. The carrier must therefore contain finite holed words, finite nil-terminated words, and infinite sequences.

Definition 24.23 — The partial-list order ¶

Let $L$ consist of finite natural-number words ending in a hole $⊥$ , finite words ending in $nil$ , and infinite natural-number sequences. Write the first two forms recursively as $⊥$ , $nil$ , and $cons (n, d)$ . A finite holed word is below every finite or infinite extension with the same revealed prefix. A finite word ending in $nil$ and an infinite word are comparable only with themselves and their holed prefixes. Equivalently, the order is generated by $⊥ ⊑_{D} d, cons (n, d) ⊑_{D} cons (n, d^{'}) when d ⊑_{D} d^{'},$ and contains no further pairs.

For $k \in N$ , the depth- $k$ observation is $\begin{array}{rclcrcl} d ↾ 0 & = & ⊥, & ⊥ ↾ (k + 1) & = & ⊥, \\ nil ↾ (k + 1) & = & nil, & cons (n, d) ↾ (k + 1) & = & cons (n, d ↾ k) . \end{array}$ The last clause also defines the finite observation of an infinite sequence.

Referenced from 3 locations

Lemma 24.24 — Finite observations determine the partial-list order ¶

For every $k$ , truncation $d \mapsto d ↾ k$ is monotone, and $d ⊑_{D} u ⟺ d ↾ k ⊑_{D} u for every k .$

Referenced from 4 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.24 — Finite observations determine the partial-list order

Proof. Monotonicity is induction on $k$ followed by inspection of the two generating order clauses. A second induction on $k$ , with a case split on $d$ , gives $d ↾ k ⊑_{D} d$ : the successor case applies the induction hypothesis beneath the common $cons$ head. Transitivity then proves the forward implication.

Conversely, if $d$ is finite, choose $k$ beyond its last cons cell. Whether $d$ ends in $nil$ or in $⊥$ , one has $d ↾ k = d$ , so the hypothesis directly gives $d ⊑_{D} u$ . If $d$ is infinite and $u$ were finite, choose $k$ beyond the final constructor of $u$ ; the longer word $d ↾ k$ could not lie below $u$ by either generating order clause. Hence $u$ is infinite. For every depth $k$ , the inequality $d ↾ k ⊑_{D} u$ forces the first $k$ heads of $u$ to equal those of $d$ . The two infinite sequences therefore have every component equal, so $u = d$ . ◻

Lemma 24.25 — The lazy-list omega-cpo ¶

The poset $L$ is a pointed omega-cpo.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.25 — The lazy-list omega-cpo

Proof. The hole is least. Let $d_{0} ⊑_{D} d_{1} ⊑_{D} \dots$ be an arbitrary chain. For each fixed $k$ , there is an index $i_{k}$ after which the finite observations $d_{i} ↾ k$ are constant. Prove this by induction on $k$ . At depth zero there is nothing to prove. At depth $k + 1$ , the chain either remains bottom, reaches $nil$ and stays there, or reaches a first cons. In the cons case all later heads are the same numeral and the tails form a chain, whose depth- $k$ observations stabilize by induction.

The stable observations are compatible: truncating the stable depth- $(k + 1)$ observation gives the stable depth- $k$ one. If some observation ends in $nil$ , the compatible family describes that finite total list. If the number of revealed cons cells is bounded but nil never appears, it describes a finite holed word. Otherwise it describes the unique infinite sequence with those heads. Call the result $d$ . Every $d_{i} ⊑_{D} d$ , since each finite observation of $d_{i}$ occurs in the compatible family. If $u$ bounds the chain, monotonicity in lemma 24.24 puts every stable finite observation of $d$ below $u$ ; the converse direction of that lemma gives $d ⊑_{D} u$ . Thus $d = ⨆_{i} d_{i}$ . ◻

Lemma 24.26 — Compact lazy lists ¶

The compact elements of $L$ are exactly its finite words, whether they end in $⊥$ or in $nil$ .

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.26 — Compact lazy lists

Proof. Every finite word $c$ is compact. If $c ⊑_{D} ⨆_{i} d_{i}$ , choose $k$ beyond its last cons cell. The construction of the lub makes truncation commute with it at depth $k$ : for some stabilization stage $j$ , $(⨆_{i} d_{i}) ↾ k = d_{j} ↾ k$ . Since $c = c ↾ k$ , monotonicity and lemma 24.24 give the complete chain $c = c ↾ k ⊑_{D} (⨆_{i} d_{i}) ↾ k = d_{j} ↾ k ⊑_{D} d_{j} .$ Thus $c$ is compact. An infinite $d$ is not compact: the increasing chain $d ↾ 0 ⊑_{D} d ↾ 1 ⊑_{D} \dots$ has lub $d$ , but $d$ lies below no finite member. This proves the compactness classification. ◻

Lemma 24.27 — The lazy-list unfolding isomorphism ¶

There are continuous inverse maps $L \underset{in}{\overset{out}{⇄}} ({*} + N \times L)_{⊥} .$

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.27 — The lazy-list unfolding isomorphism

Proof. Define $\begin{array}{rclcrcl} out (⊥) & = & ⊥, & in (⊥) & = & ⊥, \\ out (nil) & = & ↑ (inl *), & in (↑ (inl *)) & = & nil, \\ out (cons (n, d)) & = & ↑ (inr (n, d)), & in (↑ (inr (n, d))) & = & cons (n, d) . \end{array}$ The target is an omega-cpo by lemma 24.14. The defining clauses show by cases that both maps are monotone and are inverse. An order isomorphism preserves chain lubs: $out (⨆_{i} d_{i})$ is an upper bound of the $out (d_{i})$ . If $z$ is another such upper bound, then $out (d_{i}) ⊑_{D} z$ , so monotonicity of $in$ gives $d_{i} = in (out (d_{i})) ⊑_{D} in (z) .$ Hence $⨆_{i} d_{i} ⊑_{D} in (z)$ ; applying $out$ gives $out (⨆_{i} d_{i}) ⊑_{D} z$ . The argument for $in$ is symmetric. Hence both maps are continuous and the equation is an isomorphism of pointed omega-cpos, not merely a set bijection. ◻

Proposition 24.28 — The lazy list solution ¶

The poset $L$ is a pointed omega-cpo. Its compact elements are exactly its finite words, whether they end in $⊥$ or in $nil$ . There are continuous inverse maps $L \underset{in}{\overset{out}{⇄}} ({*} + N \times L)_{⊥} .$

Referenced from 6 locations

Proof of Proposition 24.28 — The lazy list solution

Proof. Combine lemma 24.25, lemma 24.26, lemma 24.27. ◻

The compactness classification makes finite observation exact: whenever a finite list prefix lies below the limit of an increasing computation, that entire prefix is already present at one finite stage. This is the order-theoretic form of finite observability for recursive list programs.

For a closed $ListNat$ value, the operational embedding is $\begin{aligned} ι (nil) & = nil, \\ ι (cell (n, v)) & = cons (n, ι (v)) . \end{aligned}$ On unfolded payload values, put $ι_{+} (inl unit) = inl *, ι_{+} (inr ⟨ n, v ⟩) = inr (n, ι (v)) .$ Recall that $↑$ is the nonbottom injection into a lifting; here its codomain is the lifted sum.

Proposition 24.29 — Finite operational lists commute with out ¶

If $\cdot ⊢ v : ListNat$ is a value and $unfold v ⟼ p$ , then $ι (v)$ is a hole-free finite compact element of $L$ and $out (ι (v)) =↑ ι_{+} (p) .$ Conversely, every hole-free finite element of $L$ is $ι (v)$ for a unique canonical list value $v$ .

Referenced from 4 locations

Proof of Proposition 24.29 — Finite operational lists commute with out

Proof. Folded canonical forms write $v = {fold}_{ListNat} p$ . Sum and product canonical forms give either $p = inl unit$ or $p = inr ⟨ n, v^{'} ⟩$ with $v^{'} : ListNat$ . Rule E-UnfoldFold yields $p$ , and the defining clause of $out$ gives the equation in either case. Induction on the finite payload tree shows that $ι (v)$ has no hole. It is compact by proposition 24.28. The same induction reconstructs the unique nested fold/injection syntax from a hole-free finite domain list. Infinite and holed elements are deliberately outside this correspondence. ◻

The chain $⊥ ⊑_{D} cons (0, ⊥) ⊑_{D} cons (0, cons (0, ⊥)) ⊑_{D} \dots$ has the infinite all-zero list as its lub. Consequently $L$ is not the set of eager finite $ListNat$ values from the opening calculus. The two objects solve related equations for different purposes.

Exercise 24.7 ¶

★★★ Prove directly that $out$ preserves the displayed all-zero chain’s lub. Then classify chains that reveal $nil$ at a finite stage, and use the classification to give an alternative, clause-by-clause proof of continuity of $in$ , rather than reusing the order-isomorphism argument in proposition 24.28.

Referenced from 3 locations

The Scott interpretation of PCF

Interpret $N$ by $N_{⊥}$ and arrows by continuous function spaces: $[[N]] = N_{⊥}, [[A \to B]] = [[[A]] ⟶ [[B]]]_{c} .$ Induction on $A$ , using lemma 24.15 at arrows, proves that every $[[A]]$ is a pointed omega-cpo. For $Γ = x_{1} : A_{1}, \dots, x_{r} : A_{r}$ , put $[[Γ]] = \prod_{i = 1}^{r} [[A_{i}]]$ with the componentwise order. An environment $η$ is an element of this finite product.

Definition 24.30 — Strict natural operations ¶

A map of pointed omega-cpos is strict when it preserves bottom. Fix a pointed omega-cpo $D$ . Define $\begin{array}{rclcrcl} {succ}_{⊥} (⊥) & = & ⊥, & {succ}_{⊥} (n) & = & n + 1, \\ {case}_{D} (⊥, d, h) & = & ⊥_{D}, & {case}_{D} (0, d, h) & = & d, \\ {case}_{D} (n + 1, d, h) & = & h (n) . \end{array}$ Here ${case}_{D} : N_{⊥} \times D \times [N_{⊥} ⟶ D]_{c} ⟶ D$ . At a successor $n + 1$ , the third argument receives its predecessor $n$ .

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Lemma 24.31 — Continuity of the strict natural operations ¶

The maps ${succ}_{⊥}$ and ${case}_{D}$ of definition 24.30 are continuous.

Referenced from 4 locations

Proof of Lemma 24.31 — Continuity of the strict natural operations

Proof. A chain in $N_{⊥}$ either remains bottom or reaches one numeral and is constant thereafter. In the first case the defining strictness equation sends every chain member to bottom. In the second, there are $i, n$ such that every image member from index $i$ onward is $succ (n)$ , which is its lub.

For a chain $(s_{i}, d_{i}, h_{i})$ , if every $s_{i} = ⊥$ , both sides of the continuity equation for ${case}_{D}$ are bottom. Otherwise the scrutinee is a fixed numeral from some stage onward. At zero, the result tail is $(d_{i})$ and has lub $⨆_{i} d_{i}$ . At $n + 1$ , the result tail is $(h_{i} (n))$ ; the pointwise-lub clause of lemma 24.15 states $⨆_{i} h_{i} (n) = (⨆_{i} h_{i}) (n)$ . These are exactly the zero and successor clauses at the componentwise lub. The same cases prove monotonicity. ◻

Definition 24.32 — PCF denotation ¶

Define the interpretation simultaneously by the following clauses. Lemma 24.33 proves that the lambda and fixed-point clauses land in the indicated continuous function spaces. $\begin{array}{rcl} [[x {]]}_{η} & = & η (x), \\ [[n {]]}_{η} & = & n, \\ [[λ x : A . e {]]}_{η} & = & (d \mapsto [[e {]]}_{η [x \mapsto d]}), \\ [[e_{1} e_{2} {]]}_{η} & = & [[e_{1} {]]}_{η} ([[e_{2} {]]}_{η}), \\ [[succ e {]]}_{η} & = & {succ}_{⊥} ([[e {]]}_{η}), \\ [[ifz e then e_{0} else x . e_{s} {]]}_{η} & = & {case}_{[[A]]} ([[e {]]}_{η}, [[e_{0} {]]}_{η}, d \mapsto [[e_{s} {]]}_{η [x \mapsto d]}), \\ [[fix x : A . e {]]}_{η} & = & lfp (d \mapsto [[e {]]}_{η [x \mapsto d]}) . \end{array}$ In the zero-test clause, $A$ is the common type of the two branches.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Lemma 24.33 — Semantic typing and continuity ¶

Give the environments for a finite context $Γ$ the pointwise omega-cpo structure. If $Γ ⊢ e : A$ , then $η \mapsto [[e {]]}_{η}$ is a continuous map from the environment cpo into $[[A]]$ . In particular every clause of definition 24.32 is well defined.

Referenced from 4 locations

Proof of Lemma 24.33 — Semantic typing and continuity

Proof. Identify $[[Γ, x : A]]$ with $[[Γ]] \times [[A]]$ ; environment extension is this product pairing. Induct on the typing derivation. Variables are projections and numerals are constant maps.

For abstraction, the body induction hypothesis is a continuous map $h : [[Γ]] \times [[A]] ⟶ [[B]] .$ Its curry is continuous by lemma 24.16, and is exactly the stated lambda clause. For application, pair the two continuous induction hypotheses and compose with continuous evaluation from the same lemma.

For successor, compose with ${succ}_{⊥}$ . For a zero test, the three induction hypotheses give continuous maps for the scrutinee, the zero branch, and the successor body. Curry the successor-body map to obtain $η \mapsto (d \mapsto [[e_{s} {]]}_{η [x \mapsto d]}) .$ Pair these three maps and compose with ${case}_{[[A]]}$ , which is continuous by lemma 24.31.

In P-Fix the body induction hypothesis gives a continuous map $Φ : [[Γ]] \times [[A]] ⟶ [[A]], Φ (η, d) = [[e {]]}_{η [x \mapsto d]} .$ The fixed-point clause is the parameterized map $η \mapsto lfp (d \mapsto Φ (η, d))$ , continuous by lemma 24.21. Hence each typing rule determines a well-defined continuous denotation of its conclusion. ◻

Lemma 24.34 — Semantic substitution and reduction invariance ¶

If $Γ, x : A ⊢ e : B$ , $Γ ⊢ d : A$ , and $η \in [[Γ]]$ , then $[[e [d / x] {]]}_{η} = [[e {]]}_{η [x \mapsto [[d {]]}_{η}]} .$ If $Γ ⊢ e : A$ and $e ⟼ e^{'}$ , then $[[e {]]}_{η} = [[e^{'} {]]}_{η}$ .

Referenced from 4 locations

Proof of Lemma 24.34 — Semantic substitution and reduction invariance

Proof. The first claim is induction on $e$ , alpha-renaming the lambda, predecessor, and fixed-point binders. In the fixed-point case choose the recursive binder $y \notin FV (d) \cup {x}$ ; the denotation of $d$ is then unchanged when the environment is extended at $y$ . The two continuous functionals are pointwise equal by the induction hypothesis, so their Kleene chains and least fixed points coincide.

For reduction invariance, inspect the five roots. Beta and the successor branch of the zero test use semantic substitution. Zero and successor compute by the defining clauses of ${case}_{D}$ . For P-Unroll, fixedness from theorem 24.17 gives $lfp F = F (lfp F) = [[e [fix x : A . e / x] {]]}_{η} .$ Context cases follow from compositionality. ◻

For a closed term, write $[[e]]$ for its denotation at the unique empty environment. Operational convergence implies the expected denotation: if $e ⇓ n$ , repeated use of reduction invariance gives $[[e]] = n$ . The converse is the substantive direction. A denotation could otherwise predict a numeral that no evaluation reaches.

Adequacy by logical approximation

A family of relations defined by recursion on types, with the arrow case testing all related arguments, is called logical. Here it connects semantic approximations to operational programs. Typing preserves this connection, and its instance at $N$ turns a numeral denotation into an operational evaluation to that numeral.

Bare induction on the typing derivation is too weak at application. Separate hypotheses saying only that $e_{1}$ and $e_{2}$ approximate their denotations do not say how the denotation of $e_{1}$ acts on the argument denotation: $d_{1} R_{A \to B} e_{1}, d_{2} R_{A} e_{2} ⟹̸ d_{1} (d_{2}) R_{B} e_{1} e_{2}$ for an unstructured family $R$ . The repair is to define the arrow clause by testing every related argument. The fixpoint proof also begins at bottom, so $⊥$ must relate to every natural-number computation.

Definition 24.35 — Logical approximation ¶

For a semantic element $d \in [[A]]$ and a closed PCF term $e : A$ , define $d R_{A} e$ by induction on $A$ : $\begin{array}{rcl} ⊥ R_{N} e & always, \\ n R_{N} e & iff & e ⇓ n, \\ f R_{A \to B} e & iff & for every d R_{A} a, f (d) R_{B} e a . \end{array}$

Referenced from 2 locations

Recursive Types, Domains, and General Recursion

Lemma 24.36 — Finite anti-reduction ¶

If $e ⟼^{*} e^{'}$ and $d R_{A} e^{'}$ , then $d R_{A} e$ .

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.36 — Finite anti-reduction

Proof. Induct on $A$ . At naturals, compose the prefix $e ⟼^{*} e^{'}$ with the reduction required by the relation: if $d = n$ , then $e^{'} ⇓ n$ , hence $e ⇓ n$ ; the bottom case is immediate. At an arrow $A = C \to B$ , for arbitrary $d_{0} R_{C} a$ , lift $e ⟼^{*} e^{'}$ to $e a ⟼^{*} e^{'} a$ and apply the codomain induction hypothesis to $d (d_{0}) R_{B} e^{'} a$ . ◻

Lemma 24.37 — Admissibility of logical approximation ¶

For fixed closed $e : A$ , the predicate $d \mapsto d R_{A} e$ contains bottom and is closed under least upper bounds of omega-chains.

Referenced from 5 locations

Proof of Lemma 24.37 — Admissibility of logical approximation

Proof. Induct on $A$ . At $N$ , bottom is related by definition. If $⨆_{i} d_{i} = n$ , flatness implies that some $d_{j} = n$ ; otherwise every member would be bottom and so would the lub. The premise for $d_{j}$ gives $e ⇓ n$ .

At $A \to B$ , bottom is the constant-bottom map and the induction hypothesis at $B$ gives $⊥ R_{B} e a$ for every $d R_{A} a$ . For a chain $(f_{i})$ , take arbitrary $d R_{A} a$ . The sequence $(f_{i} (d))$ is a chain, each member is related to $e a$ , and the codomain induction hypothesis gives $⨆_{i} f_{i} (d) R_{B} e a$ . Pointwise function-space lubs satisfy $⨆_{i} f_{i} (d) = (⨆_{i} f_{i}) (d)$ . ◻

An environment $η$ and a closing substitution $γ$ are related at $Γ$ , written $η R_{Γ} γ$ , when $η (x) R_{A} γ (x)$ for every $x : A \in Γ$ .

Theorem 24.38 — Fundamental approximation ¶

If $Γ ⊢ e : A$ and $η R_{Γ} γ$ , then $[[e {]]}_{η} R_{A} e [γ] .$

Referenced from 5 locations

Proof of Theorem 24.38 — Fundamental approximation

Proof. Induct on the typing derivation. For a variable $x$ , the premise is $η (x) R_{A} γ (x)$ ; a numeral evaluates to itself. In an application, the operator induction hypothesis is quantified over every related argument, so instantiate it with the argument induction hypothesis. For lambda, take arbitrary $d R_{A} a$ , extend both environments by $x \mapsto d$ and $x \mapsto a$ , and apply the body induction hypothesis to the closed body. The beta step $(λ x . e [γ]) a ⟼ e [γ, a / x]$ and lemma 24.36 give the arrow clause.

For successor, the bottom semantic case is immediate. In the numeral case, the scrutinee induction hypothesis gives evaluation to $n$ , after which P-SuccN gives $n + 1$ . The zero-test case splits the semantic scrutinee. At bottom, the conclusion follows uniformly because bottom is related at every type by lemma 24.37. At zero use the first branch induction hypothesis and P-IfZ; at $n + 1$ , extend the environments by the related predecessor $n$ and use P-IfS.

For P-Fix, let $F (d) = [[e {]]}_{η [x \mapsto d]}, q = fix x : A . e [γ] .$ We prove $F^{k} ⊥ R_{A} q$ by induction on $k$ . The base is bottom. For the step, extend the semantic environment by $x \mapsto F^{k} ⊥$ and the term substitution by $x \mapsto q$ . The body induction hypothesis gives $F^{k + 1} ⊥ R_{A} e [γ, q / x] .$ Rule P-Unroll takes $q$ to that term, so anti-reduction relates the same element to $q$ . Finally, lemma 24.37 closes the chain and relates $⨆_{k} F^{k} ⊥ = lfp F$ to $q$ . This is the only place where ordinary induction on term syntax is insufficient; admissibility turns all finite unfoldings into the recursive result. ◻

Theorem 24.39 — Computational adequacy for closed naturals ¶

If $\cdot ⊢ e : N$ , then for every numeral $n$ , $e ⇓ n ⟺ [[e]] = n .$ Moreover, $[[e]] = ⊥$ exactly when $e ⟼^{ω}$ .

Referenced from 4 locations

Proof of Theorem 24.39 — Computational adequacy for closed naturals

Proof. For $(\Rightarrow)$ , use lemma 24.34’s reduction-invariance clause along every step of $e ⟼^{*} n$ , obtaining $[[e]] = [[n]] = n$ . For $(\Leftarrow)$ , use the fundamental approximation theorem, theorem 24.38, with empty environments. If the denotation is $n$ , the base clause is exactly $n R_{N} e ⟺ e ⇓ n .$

By lemma 24.12, a closed natural term either evaluates to a unique numeral or has an infinite reduction. The established equivalence is $[[e]] = n ⟺ e ⇓ n$ . Since every element of $N_{⊥}$ is $⊥$ or a numeral, $[[e]] = ⊥$ is therefore equivalent to $e ⟼^{ω}$ . ◻

Exercise 24.8 ¶

★★☆ Reprove only the P-Fix case of theorem 24.38. State the relation between the semantic and term environments at each finite iterate, identify the use of anti-reduction, and name the admissibility hypothesis used at the limit.

Referenced from 3 locations

Recursive reasoning one finite observation at a time

The denotational proof handles a fixed point by finite approximants. The same well-founded idea can compare values at a recursive type directly. A naive definition $fold v \approx_{μ X . A} fold w iff v \approx_{A [μ X . A / X]} w$ is circular. An observation index changes the recursive call from $n + 1$ to $n$ .

Convention 24.40 — The indexed call-by-value fragment ¶

Step-indexed equivalence uses the eager fold calculus without Booleans. The retained terms are variables, unit, numerals, lambdas and application, pairs and projections, sums and case, and fold and unfold. Their evaluation contexts are $\begin{aligned} K ::= & [] ∣ K e ∣ v K ∣ ⟨ K, e ⟩ ∣ ⟨ v, K ⟩ ∣ fst K ∣ snd K \\ ∣ inl K ∣ inr K ∣ case K of {inl x \mapsto e_{0}; inr y \mapsto e_{1}} \\ ∣ {fold}_{μ X . A} K ∣ unfold K . \end{aligned}$ The root contractions are call-by-value beta, the two projections, the two sum cases, and E-UnfoldFold. These contexts evaluate an application operator, then its argument, and then contract beta.

Referenced from 7 locations

Definition 24.41 — Step-indexed equivalence ¶

For closed, equally typed terms of the fragment in convention 24.40, define value relations $v \approx_{n}^{A} w$ and term relations $e E_{n}^{A} d$ simultaneously. At index zero every pair of closed well-typed values is related. At $n + 1$ , the value clauses are $\begin{array}{rcl} unit \approx_{n + 1}^{1} unit & always, \\ k \approx_{n + 1}^{N} ℓ & ⟺ & k = ℓ, \\ ⟨ v_{1}, v_{2} ⟩ \approx_{n + 1}^{A \times B} ⟨ w_{1}, w_{2} ⟩ & ⟺ & v_{1} \approx_{n + 1}^{A} w_{1} and v_{2} \approx_{n + 1}^{B} w_{2}, \\ inl v \approx_{n + 1}^{A + B} inl w & ⟺ & v \approx_{n + 1}^{A} w, \\ inr v \approx_{n + 1}^{A + B} inr w & ⟺ & v \approx_{n + 1}^{B} w . \end{array}$ Values with different sum tags are not related. At arrows, $f \approx_{n + 1}^{A \to B} g$ when for every $j \leq n + 1$ and $v \approx_{j}^{A} w$ , $f v E_{j}^{B} g w$ . The only circular-looking clause consumes an index: ${fold}_{μ X . A} v \approx_{n + 1}^{μ X . A} {fold}_{μ X . A} w ⟺ v \approx_{n}^{A [μ X . A / X]} w .$ To verify that the simultaneous definition is well founded, let $| A |$ count one node for each base or type constructor: $\begin{aligned} | N | = | 1 | = | X | & = 1, \\ | A \circ B | & = 1 + | A | + | B | & (\circ \in {\to, \times, +}), \\ | μ X . A | & = 1 + | A | . \end{aligned}$ Put $ρ = 0$ for value relations and $ρ = 1$ for term relations. Order recursive calls lexicographically by $(n, | A |, ρ)$ . The recursive-type clause changes $n + 1$ to $n$ . In the arrow clause, a test at $j < n + 1$ lowers the index; a test at $j = n + 1$ recurses on the proper component $A$ or $B$ . At a zero-step endpoint, the term relation calls the value relation at the same index and type, which lowers the phase. Thus every recursive call strictly decreases the lexicographic measure. The quantifier $j \leq n + 1$ ranges over every smaller observation index required by the arrow clause.

Write $e ⟼^{j} v$ for exactly $j$ steps to a value. Then $e E_{n}^{A} d$ iff both of the following hold for every $j < n$ : $\begin{array}{ll} e ⟼^{j} v & ⟹ \exists w . d ⟼^{*} w and v \approx_{n - j}^{A} w, \\ d ⟼^{j} w & ⟹ \exists v . e ⟼^{*} v and v \approx_{n - j}^{A} w . \end{array}$ All quantified endpoints $v, w$ are values. For a context $Γ$ , write $γ \approx_{n}^{Γ} δ$ when the two closing substitutions map every $x : A \in Γ$ to values related by $\approx_{n}^{A}$ .

Referenced from 5 locations

Recursive Types, Domains, and General Recursion

Lemma 24.42 — Unique indexed decomposition ¶

Every closed, well-typed nonvalue in the indexed fragment has a unique decomposition $K [r]$ , where $K$ is an evaluation context from convention 24.40 and $r$ is one of that convention’s root redexes. Consequently it has exactly one one-step reduct.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.42 — Unique indexed decomposition

Proof. Proceed by the outer syntax. An application first selects a nonvalue operator, then a nonvalue argument once the operator is a value, and otherwise has a beta root; closed canonical forms force an arrow-typed operator value to be a lambda. A pair selects its left component before its right. A projection or case selects only its scrutinee; once that scrutinee is a value, product or sum canonical forms select exactly one root rule. Injections, folds, and unfolds each select their sole payload, except that an unfold of a folded value is the E-UnfoldFold root. These cases are disjoint, and the induction hypothesis makes the selected subterm decomposition unique. Existence is the progress clause of theorem 24.5; disjoint context positions and root patterns supply uniqueness. ◻

Lemma 24.43 — Terminating-trace decomposition ¶

Reduction in the indexed fragment is deterministic. Every terminating trace has the decomposition forced by its outer constructor. In particular:

if $e_{1} e_{2} ⟼^{r} v$ , then uniquely $\begin{matrix} e_{1} ⟼^{r_{1}} λ x : A . b, e_{2} ⟼^{r_{2}} u, b [u / x] ⟼^{r_{3}} v, \\ r = r_{1} + r_{2} + 1 + r_{3}; \end{matrix}$
a trace from $⟨ e_{1}, e_{2} ⟩$ to a value consists of $e_{1} ⟼^{r_{1}} v_{1}$ , followed by $e_{2} ⟼^{r_{2}} v_{2}$ , and has length $r_{1} + r_{2}$ ;
a projection trace first reaches a pair and then takes its one root step; a sum-case trace first reaches one injection, takes its one root step, and continues in the selected substituted branch;
a fold trace evaluates only its payload, while an unfold trace first reaches a folded value and then takes its one E-UnfoldFold step.

Injection traces have the same one-payload form as folds.

Referenced from 4 locations

Proof of Lemma 24.43 — Terminating-trace decomposition

Proof. One-step reduction is deterministic by lemma 24.42. Induct on the length of a terminating trace. For an application, steps stay in the operator until it is a lambda, then stay in the argument until it is a value, then take the unique beta step; all remaining steps are in the substituted body. This gives item 1 and its length equation. Pair contexts first select the left component and then the right, giving item 2. Projection and case contexts select only the scrutinee before their root step, while fold, unfold, and injection contexts select only their payload. The grammar of convention 24.40 assigns each constructor exactly one of these decompositions. ◻

Lemma 24.44 — Indexed downward closure and anti-reduction ¶

The following hold for the relations of definition 24.41.

If $m \leq n$ , either relation at $n$ implies the corresponding relation at $m$ .
If $v \approx_{n}^{A} w$ , then $v E_{n}^{A} w$ . If $e ⟼^{*} e^{'}$ , $d ⟼^{*} d^{'}$ , and $e^{'} E_{n}^{A} d^{'}$ , then $e E_{n}^{A} d$ .

Referenced from 4 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.44 — Indexed downward closure and anti-reduction

Proof. Downward closure. For downward closure, use the lexicographic measure $(n, | A |, ρ)$ established in definition 24.41, with value phase $ρ = 0$ and term phase $ρ = 1$ . Products and sums recurse on proper component types. At a recursive type, the payload relation is at the smaller index. At an arrow, every test index allowed at $m$ is already allowed at $n$ . For terms, $j < m$ implies $j < n$ , and downward closure of values changes the residual relation from $n - j$ to $m - j$ .

Values and anti-reduction. At index zero the term relation is vacuous. At a positive index a value has only its zero-step terminating trace, so $v \approx_{n}^{A} w$ gives $v E_{n}^{A} w$ .

For anti-reduction, suppose $e ⟼^{r} e^{'}$ and $e ⟼^{j} v$ , where $j < n$ . Determinism from lemma 24.43 gives $j \geq r$ and $e^{'} ⟼^{j - r} v$ . From $e^{'} E_{n}^{A} d^{'}$ , obtain a value reachable from $d^{'}$ and related to $v$ at index $n - (j - r)$ . Downward closure changes that index to $n - j$ , and the prefix $d ⟼^{*} d^{'}$ gives the required trace from $d$ . Interchanging the two terms proves the other observation clause. ◻

Lemma 24.45 — Indexed fundamental lemma ¶

If $Γ ⊢ e : A$ and $γ \approx_{n}^{Γ} δ$ , then $e [γ] E_{n}^{A} e [δ]$ .

Referenced from 4 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.45 — Indexed fundamental lemma

Proof. Use downward closure, value inclusion, and anti-reduction from lemma 24.44. The only budget calculation not immediate from a constructor is application.

Application budget. Suppose a left application reaches a value in $r < n$ steps. Its unique trace decomposition has lengths $r = r_{1} + r_{2} + 1 + r_{3}$ for operator evaluation, argument evaluation, beta, and body evaluation. By the first implication in the operator term relation, the right operator reaches a lambda related to the left lambda at $q = n - r_{1}$ . Since $r_{2} + 1 + r_{3} < q$ , the first implication in the argument term relation gives a reachable right argument value; downward closure relates the argument values at $s = q - r_{2} .$ The arrow clause at $q$ applies at $s \leq q$ . The left beta redex then takes $1 + r_{3} < s$ steps, leaving the result index $s - (1 + r_{3}) = n - r .$ Thus $\begin{matrix} r = r_{1} + r_{2} + 1 + r_{3} < n, q = n - r_{1}, s = q - r_{2}, \\ 1 + r_{3} < s \leq q, s - (1 + r_{3}) = n - r . \end{matrix}$ Prepending the matching operator and argument traces gives the right application trace. The symmetric calculation gives the other observation clause.

Other constructors. For a pair trace of length $r_{1} + r_{2} < n$ , the first component is matched at $n - r_{1}$ , then lowered to $n - r_{1} - r_{2}$ ; the second is matched directly at that final index. The product value clause combines them. An injection is the one-component calculation. A fold payload matched at $n - r > 0$ is lowered once for the recursive-value clause; at index zero every pair of folded values is related.

A projection or unfold spends one root step after its scrutinee trace. If the scrutinees are pairs related at $q$ , their selected components are related at $q$ , hence at $q - 1$ by downward closure. If they are folds related at $q$ , the recursive-value clause relates their payloads at $q - 1$ . A case trace spends its root step and then $r_{b}$ steps in a branch. Matching injections have payloads related at $q$ ; downward closure derives their relation at $q - 1$ , and the branch relation leaves $q - 1 - r_{b}$ , the index required by the whole trace. Each calculation is symmetric in the two terms.

Related substitution. For related substitution, induct on typing with the index universally quantified in every induction hypothesis. A variable selects its related pair from $γ \approx_{n}^{Γ} δ$ ; unit and numerals are related values. Applying the product, sum, fold/unfold, projection, and application budget equations to the corresponding induction hypotheses derives their term relations at index $n$ .

For a lambda at index $n + 1$ , choose $j \leq n + 1$ and values $v \approx_{j}^{A} w$ . Downward closure derives $γ \approx_{j}^{Γ} δ$ ; extending by $x \mapsto v$ and $x \mapsto w$ gives related substitutions for the body, whose induction hypothesis relates the two closed bodies at $j$ . The use is valid even when $j = n + 1$ : the induction decreases the body typing derivation, not the index. One beta step on each side and anti-reduction therefore relate the applications at $j$ , which is the arrow value clause. Value inclusion gives the required term relation.

For a sum case, the scrutinee calculation gives equal injection tags and a payload relation at the remaining index. Extending the substitutions by those payloads satisfies the selected branch hypothesis; one case root step and anti-reduction give the required term relation. The unselected branch is not evaluated. ◻

Lemma 24.46 — Indexed evaluation-context compatibility ¶

If $K [-]$ is a well-typed closing evaluation context from $A$ to $B$ and $e E_{n}^{A} d$ , then $K [e] E_{n}^{B} K [d]$ .

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proof of Lemma 24.46 — Indexed evaluation-context compatibility

Proof. Evaluation contexts. For evaluation contexts, induct on $K$ . The hole is the identity case. In $K e_{0}$ and $v K$ , the fixed operand is self-related by lemma 24.45, and the application calculation composes it with the hole relation. Pair, injection, and fold contexts use their payload calculations; projection and unfold use their one-scrutinee calculations. A case context uses the case calculation with each fixed branch self-related under its payload binder. Thus every context constructor composes the hole relation without changing the outer index $n$ . ◻

Lemma 24.47 — Indexed structural package ¶

The following hold for the relations of definition 24.41.

If $m \leq n$ , either relation at $n$ implies the corresponding relation at $m$ .
If $v \approx_{n}^{A} w$ , then $v E_{n}^{A} w$ . If $e ⟼^{*} e^{'}$ , $d ⟼^{*} d^{'}$ , and $e^{'} E_{n}^{A} d^{'}$ , then $e E_{n}^{A} d$ .
If $Γ ⊢ e : A$ and $γ \approx_{n}^{Γ} δ$ , then $e [γ] E_{n}^{A} e [δ]$ .
If $K [-]$ is a well-typed closing evaluation context from $A$ to $B$ and $e E_{n}^{A} d$ , then $K [e] E_{n}^{B} K [d]$ .

Referenced from 4 locations

Proof of Lemma 24.47 — Indexed structural package

Proof. Clauses 1–2 are lemma 24.44; clause 3 is lemma 24.45; clause 4 is lemma 24.46. ◻

Definition 24.48 — An eta-delayed call-by-value fixed point ¶

For types $A, B$ , put $\begin{aligned} R_{A, B} & : = μ X . (X \to A \to B), \\ θ_{f} & : = λ x : R_{A, B} . λ y : A . f ((unfold x) x) y, \\ Z_{A, B} & : = λ f : (A \to B) \to A \to B . θ_{f} ({fold}_{R_{A, B}} θ_{f}) . \end{aligned}$ Thus $Z_{A, B} : ((A \to B) \to A \to B) \to A \to B$ . For a closed value $f$ , evaluation of $Z_{A, B} f$ reaches a lambda before evaluating its recursive call: $Z_{A, B} f ⟼^{*} λ y : A . f ((unfold (fold θ_{f})) (fold θ_{f})) y .$ When evaluation of the body demands the recursive function, the parenthesized term takes two steps back to the same lambda. Eta-delay, absent from ${Fix}_{A}$ , is the load-bearing call-by-value repair.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proposition 24.49 — The eta-delayed equation is pointwise ¶

Let $f : (A \to B) \to A \to B$ and $a : A$ be closed values. Then $Z_{A, B} f a and f (Z_{A, B} f) a$ reduce to a common term. At function type the corresponding contextual-equivalence statement can fail.

Referenced from 3 locations

Proof of Proposition 24.49 — The eta-delayed equation is pointwise

Proof. Put $h = {fold}_{R_{A, B}} θ_{f}$ and $g = λ y : A . f ((unfold h) h) y .$ Then $Z_{A, B} f ⟼^{*} g, (unfold h) h ⟼^{2} g .$ The left term reduces through $g a$ , then uses $(unfold h) h ⟼^{2} g$ to reach $f g a$ . The right term first evaluates its argument $Z_{A, B} f$ to $g$ , and reaches the same term.

For the qualification, recall the two-step loop at an arbitrary type: $\begin{aligned} D_{C} & = μ X . (X \to C), \\ δ_{C} & = λ x : D_{C} . (unfold x) x, \\ Ω_{C} & = δ_{C} ({fold}_{D_{C}} δ_{C}) : C . \end{aligned}$ Take $C = A \to B$ and $f = λ c : A \to B . Ω_{C}$ . Then $Z_{A, B} f$ reaches the value $g$ , while $f (Z_{A, B} f)$ reaches $Ω_{C}$ and diverges. The closing context $(λ h : A \to B .0) [-]$ evaluates its hole under call by value, so it distinguishes the two function terms. ◻

Define a recursive list copier inside the eager calculus by $\begin{aligned} copy & : = θ_{copyBody} ({fold}_{R_{ListNat, ListNat}} θ_{copyBody}), \\ copyBody & : = λ c : ListNat \to ListNat . λ x s : ListNat . caseList x s of \\ {nil \mapsto nil; cons (n, y s) \mapsto cons n (c y s)} . \end{aligned}$ This is the first beta reduct of $Z_{ListNat, ListNat} copyBody$ ; in the cons branch, $n : N$ and $y s : ListNat$ .

Lemma 24.50 — Structural convergence of the copier ¶

For every closed value $v : ListNat$ , $copy v ⟼^{*} v .$

Referenced from 5 locations

Proof of Lemma 24.50 — Structural convergence of the copier

Proof. Write $θ = θ_{copyBody}, h = {fold}_{R_{ListNat, ListNat}} θ, r = (unfold h) h,$ and put $g = λ x s : ListNat . copyBody r x s .$ Abbreviate the body after its two binders by $C (c, x s) : = caseList x s of {nil \mapsto nil; cons (n, y s) \mapsto cons n (c y s)} .$ The recursive argument has the two explicit steps $r = (unfold h) h \overset{E - U n f o l d F o l d}{⟼} θ h \overset{β}{⟼} g, copy = θ h \overset{β}{⟼} g .$

We prove $g v ⟼^{*} v$ by structural induction on the canonical list value $v$ . Folded, sum, and product canonical forms give $nil$ or $cell (k, y s)$ . The nil trace is $\begin{aligned} g nil & \overset{β}{⟼} copyBody r nil \\ \overset{E - U n f o l d F o l d}{⟼} copyBody (θ h) nil \overset{β}{⟼} copyBody g nil \\ \overset{β}{⟼} (λ x s . C (g, x s)) nil \overset{β}{⟼} C (g, nil) \\ = case (unfold ({fold}_{ListNat} (inl unit)); u . nil; z . cons (fst z) (g (snd z))) \\ \overset{E - U n f o l d F o l d}{⟼} case (inl unit; u . nil; z . cons (fst z) (g (snd z))) \overset{l e f t s u m - β}{⟼} nil . \end{aligned}$ For $p = ⟨ k, y s ⟩$ , the cons prefix is $\begin{aligned} g cell (k, y s) & \overset{β}{⟼} copyBody r cell (k, y s) \\ \overset{E - U n f o l d F o l d}{⟼} copyBody (θ h) cell (k, y s) \\ \overset{β}{⟼} copyBody g cell (k, y s) \\ \overset{β}{⟼} (λ x s . C (g, x s)) cell (k, y s) \\ \overset{β}{⟼} C (g, cell (k, y s)) . \end{aligned}$ Put $ℓ_{k} = λ z s : ListNat . cell (k, z s), B_{g} (z) = cons (fst z) (g (snd z)) .$ The remaining steps are $\begin{aligned} C (g, cell (k, y s)) & = case (unfold ({fold}_{ListNat} (inr p)); u . nil; z . B_{g} (z)) \\ \overset{E - U n f o l d F o l d}{⟼} case (inr p; u . nil; z . B_{g} (z)) \\ \overset{r i g h t s u m - β}{⟼} B_{g} (p) \\ = cons (fst p) (g (snd p)) \\ \overset{fst - β}{⟼} cons k (g (snd p)) \\ \overset{β f o r cons k}{⟼} ℓ_{k} (g (snd p)) \\ \overset{snd - β}{⟼} ℓ_{k} (g y s) \\ \overset{i n d u c t i o n h y p o t h e s i s}{⟼^{*}} ℓ_{k} y s \\ \overset{β}{⟼} cell (k, y s) . \end{aligned}$ Therefore $copy v ⟼ g v ⟼^{*} v$ . ◻

Theorem 24.51 — Recursive list copy ¶

For every closed value $v : ListNat$ and every $n$ , $copy v E_{n}^{ListNat} v .$ Consequently, for every closing well-typed evaluation context $K [-]$ of natural result type and every numeral $m$ , $K [copy v] ⟼^{*} m ⟺ K [v] ⟼^{*} m .$ The equivalence does not assert that either plugged term converges.

Referenced from 5 locations

Proof of Theorem 24.51 — Recursive list copy

Proof. Item 3 of lemma 24.47, with equal empty substitutions, gives $v E_{n}^{ListNat} v$ . Lemma 24.50 gives $copy v ⟼^{*} v$ ; indexed anti-reduction, item 2 of the same package, gives $copy v E_{n}^{ListNat} v$ .

Item 4 lifts this relation through $K [-]$ . If either plugged term reaches a numeral in $j$ steps, choose $n > j$ . The corresponding observation clause gives a numeral on the other side related at positive index $n - j$ . The natural-number value clause relates only identical numerals, so the other result is $m$ . Apply the symmetric observation clause for the reverse implication. If the context diverges before producing a natural value, neither observation antecedent holds; no convergence claim follows. ◻

Exercise 24.9 ¶

★★☆ Prove downward closure for the $μ$ -value and arrow clauses. Then expand the $cons$ trace in lemma 24.50: name the two reductions $r ⟼^{2} g$ , the right sum-case root, and the exact point where the structural induction hypothesis is lifted through the cons contexts. Finally, use indexed anti-reduction to derive $copy v E_{n} v$ at an arbitrary $n$ .

Referenced from 3 locations

Safety, correctness, termination, productivity, and totality

These five guarantees have different witnesses: finite reduction prefixes, returned numerals, and finite observations of a domain element.

Definition 24.52 — Finite tail observation ¶

For $d, d^{'} \in L$ , the judgment $d \overset{k}{⇝} d^{'}$ says that $k$ consecutive cons cells can be observed and leave tail $d^{'}$ . It is generated by

d \overset{0}{⇝} d

Obs-Zero

out (d) = ↑ (inr (n, d_{1}))

d_{1} \overset{k}{⇝} d^{'}

d \overset{k + 1}{⇝} d^{'}

Obs-Cons

In particular, neither a hole nor $nil$ admits an Obs-Cons step.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Definition 24.53 — Safety, correctness, termination, productivity, totality ¶

For the deterministic closed calculi of this chapter:

a term is safe at $A$ when every finite reduct remains typed at $A$ , and every irreducible reduct is a value;
a natural computation is partially correct for $Q$ when the PCF judgment $e ⇓ n$ implies $Q (n)$ ;
it terminates when the PCF judgment $e ⇓ n$ holds for some $n$ ;
an element $d \in L$ is productive when, for every $k$ , some $d_{k}$ satisfies $d \overset{k}{⇝} d_{k}$ according to definition 24.52; and
a natural computation is total for $Q$ when it terminates and is partially correct for $Q$ .

The productivity clause is a property of the lazy-list domain developed here, not a claim that an eager term returns an infinite value.

Referenced from 3 locations

Proposition 24.54 — The five notions separate ¶

The term $Ω_{D}$ is safe and has an infinite eager reduction. The all-zero infinite element of $L$ is productive and lies outside the image of the finite eager-list embedding. For all numerals $m, n$ , $plus m n ⇓ m + n,$ so closed addition is total for the mathematical-sum postcondition. Partial correctness alone entails none of these termination or productivity claims.

Referenced from 3 locations

Proof of Proposition 24.54 — The five notions separate

Proof. Safety of $Ω_{D}$ is theorem 24.5; iterating its two-step cycle gives an infinite reduction. If $z$ is the all-zero infinite element, then $out (z) = ↑ (inr (0, z))$ . Induction on $k$ , using Obs-Zero and Obs-Cons, gives $z \overset{k}{⇝} z$ ; hence $z$ is productive. It is not in the image of the finite embedding of proposition 24.29.

For addition, induct on $m$ . At zero, one unrolling, two beta steps, and the zero root select the zero branch and return $n$ . At $m + 1$ , the successor branch reduces to $succ (plus m n)$ ; the induction hypothesis and P-SuccN give $m + n + 1$ . Any diverging well-typed term is partially correct for the false postcondition vacuously, showing why partial correctness entails no termination fact. ◻

Exercise 24.10 ¶

★☆☆ Classify the following claims as safety, partial correctness, termination, productivity, or totality: the type of $Ω_{D}$ is preserved; a division routine returns the quotient if it returns and its divisor is nonzero; every recursive call to $plus$ returns; each observation of the all-zero lazy list reveals a cons; and $plus$ returns the mathematical sum for all inputs. Justify each classification by the definitions in this chapter.

Referenced from 3 locations

Definition 24.55 — The unrestricted proof-recursion extension ¶

Suppose simple types are read as propositions and include an empty type $0$ , with no introduction rule. The unrestricted recursion extension adds, at every proposition $P$ ,

Γ, p : P ⊢ e : P

Γ ⊢ fix p : P . e : P

Pr-Fix

fix p : P . e ⇝_{0} e [fix p : P . e / p]

Pr-Unroll

The propositions-as-types reading counts every closed inhabitant $\cdot ⊢ q : P$ as a proof of $P$ ; it cannot inspect whether $q$ later terminates.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Theorem 24.56 — Unrestricted recursion is not a total proof principle ¶

In the extension of definition 24.55, every proposition $P$ has a closed inhabitant $ω_{P} : = fix p : P . p : P .$ Moreover $ω_{P} ⇝_{0} ω_{P}$ . In particular, $ω_{0} : 0$ refutes the syntactic-consistency statement that the empty type has no closed inhabitant, even though no empty-type value is produced.

Referenced from 3 locations

Recursive Types, Domains, and General Recursion

Proof of Theorem 24.56 — Unrestricted recursion is not a total proof principle

Proof. Under $p : P$ , the variable rule derives $p : P$ ; Pr-Fix therefore derives $\cdot ⊢ ω_{P} : P$ . Substituting $ω_{P}$ for $p$ in the body $p$ , rule Pr-Unroll gives the one-step self-loop. Specializing to $P = 0$ gives a closed inhabitant of the empty type. Preservation may still retain its type and progress may still give its successor step, so operational safety does not repair the failed proof reading. ◻

Exercise 24.11 ¶

★☆☆ Prove preservation for the single root Pr-Unroll using term substitution. Then explain, using theorem 24.56, why that preservation proof does not establish either normalization or consistency-as-uninhabited- $0$ .

Referenced from 3 locations

General recursion therefore defines partial computations, not total proofs. A propositions-as-types core must reject Pr-Fix, restrict it by a termination argument, or segregate partial programs from proof terms. No dependent repair is being assumed here.

Suggested first pass.

Begin with exercise 24.12, exercise 24.13, exercise 24.14; then use the remaining problems to reconstruct adequacy and compare explicit with equi-recursive reasoning.

Exercise 24.12 ¶

★★☆ Let $v_{0} = nil, v_{1} = cell (0, nil), v_{2} = cell (1, nil),$ and $v_{3} = cell (0, cell (1, nil)), v_{4} = cell (0, cell (2, nil)) .$ For the pairs $(v_{0}, v_{1})$ , $(v_{1}, v_{2})$ , and $(v_{3}, v_{4})$ , determine the least positive index at which the two members are not related by $\approx_{n}^{ListNat}$ . Display the fold, sum, product, and natural-number clauses traversed by the calculation.

Referenced from 4 locations

Exercise 24.13 ¶

★★☆ Define a continuous map $Φ : N_{⊥} \times N_{⊥} ⟶ N_{⊥}$ by $Φ (p, d) = {case}_{N_{⊥}} (p, 0, n \mapsto {succ}_{⊥} (d)) .$ Compute every Kleene iterate of $F_{p} (d) = Φ (p, d)$ for $p = ⊥$ , $p = 0$ , and $p = k + 1$ . Hence compute $μ Φ (p)$ in all three cases and verify directly the continuity conclusion of lemma 24.21.

Referenced from 4 locations

Exercise 24.14 ¶

★☆☆ Let $K [-] = (λ x s : ListNat . Ω_{D}) [-] .$ Show that both $K [v]$ and $K [copy v]$ diverge for every closed list value $v$ . Explain why this example satisfies the biconditional in theorem 24.51 but refutes the stronger assertion that both plugged terms must converge.

Referenced from 4 locations

Exercise 24.15 ¶

★☆☆ Calculate the denotation of $Ω_{N} = fix x : N . x$ from the Kleene chain of the identity map. Then use each direction of theorem 24.39 separately to recover the operational facts about $Ω_{N}$ and about the displayed run $plus 2 1 ⇓ 3$ .

Referenced from 3 locations

Exercise 24.16 ¶

★★☆ For $L = μ X . (1 + N \times X),$ let $p : 1 + N \times L$ be a closed value. Write the explicit iso-recursive typing and reduction of $unfold ({fold}_{L} p)$ . Then run the equi-recursive worklist on $L$ and $1 + N \times L$ . State precisely which step is an operational contraction and which is a type-equality decision; do not use one as a premise for the other.

Referenced from 3 locations

Exercise 24.17 ¶

★★★ Practical project.recursion-bisimulation-lab Implement an explicit fold/unfold evaluator and a separate regular-tree equality worklist. Maintain the invariant that operational roots are never consumed as type-equality evidence and that each equality-cache entry records a pair of unfolded regular nodes. Test a nil observation, a nonempty-list observation, one fold/unfold root, equal and unequal regular trees, and a fuel-bounded PCF run. Then disable guardedness, conflate fold reduction with type equality, and treat fuel exhaustion as convergence in three independent variants; each variant must falsify its corresponding case. The PCF fuel result is an observation, not a proof of divergence. Appendix E records the acceptance commands, and appendix F develops both machines.

Referenced from 4 locations

Sources.

Harper gives the fold/unfold and fixed-point mechanisms for FPC in Chapter 20, printed pp. 177–183, and PCF in Chapter 19, printed pp. 168–176 [Har16]. The eager list encoding and the terms $Ω_{D}$ , ${Fix}_{A}$ , and $Z_{A, B}$ instantiate those mechanisms at, respectively, $N$ , $(A \to A) \to A$ , and $((A \to B) \to A \to B) \to A \to B$ .

Abramsky and Jung define directed completeness and continuity in Definitions 2.1.13 and 2.1.17, prove continuity of function spaces and the fixed-point operator in Proposition 2.1.18 and Theorem 2.1.19, state admissible induction in Lemma 2.1.20, and define compactness in Definition 2.2.1, printed pp. 15–18 [AJ94]. The omega-chain calculations in theorem 24.17, proposition 24.28 give the fixed point and list equation used here.

Amadio and Cardelli give tree expansion and the trail algorithm in Sections 3.3–4.3, printed pp. 11–24 [AC93]. The worklist in definition 24.7 is its closed, contractive equality specialization.