ch:recursive-types: ch:recursive-types

Put $L=\mu X.(\mathsf{Unit}+\mathsf{Nat}\times X)$. The empty list has the derivation $$\frac{{\displaystyle \frac{\cdot ⊢\mathsf{unit}:\mathsf{Unit}}{\cdot ⊢\mathsf{inl}\mathsf{unit}:\mathsf{Unit}+\mathsf{Nat}\times L}}\mathrm{T}-\mathrm{Inl}}{\cdot ⊢\mathsf{nil}:L}\mathrm{T}-\mathrm{Fold}.$$ Under $n:\mathsf{Nat},xs:L$, pairing and right injection give $$⟨n,xs⟩:\mathsf{Nat}\times L,\mathsf{inr}⟨n,xs⟩:\mathsf{Unit}+\mathsf{Nat}\times L.$$ Rule T-Fold, followed by two lambda rules, therefore derives $$\cdot ⊢\mathsf{cons}:\mathsf{Nat}\to L\to L.$$ The two applications complete the requested derivation: $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\cdot ⊢\mathsf{cons}:\mathsf{Nat}\to L\to L\\ \cdot ⊢3:\mathsf{Nat}\end{array}}{\cdot ⊢\mathsf{cons}3:L\to L}}\mathrm{T}-\mathrm{App}\\ \cdot ⊢\mathsf{nil}:L\end{array}}{\cdot ⊢\mathsf{cons}3\mathsf{nil}:L}\mathrm{T}-\mathrm{App}.$$

To keep the trace within the measure, first expose the two abbreviations: Thus $c=\mathsf{cons}$, and $C[-]$ is exactly the displayed list case. Every reduction is The third reduction is the unique use of E-UnfoldFold.

Let $$T=\mu X.(\mathsf{Nat}\times X+\mathsf{Unit}).$$ The substitution instance in the fold premise is $$(\mathsf{Nat}\times X+\mathsf{Unit})[T/X]=\mathsf{Nat}\times T+\mathsf{Unit}.$$ If $\cdot ⊢v:\mathsf{Nat}\times T+\mathsf{Unit}$, the redex is typed by $$\frac{{\displaystyle \frac{\cdot ⊢v:\mathsf{Nat}\times T+\mathsf{Unit}}{\cdot ⊢{\mathsf{fold}}_{T}v:T}}\mathrm{T}-\mathrm{Fold}}{\cdot ⊢\mathsf{unfold}({\mathsf{fold}}_{T}v):\mathsf{Nat}\times T+\mathsf{Unit}}\mathrm{T}-\mathrm{Unfold}.$$ Rule E-UnfoldFold contracts this term to $v$, which already has the type on the conclusion. No type-equality rule occurs: the common type is obtained by the displayed capture-avoiding substitution in the premises of T-Fold and T-Unfold.

For $D=\mu X.(X\to \mathsf{Nat})$, the derivation under $x:D$ is $$\frac{\begin{array}{c}{\displaystyle \frac{x:D⊢x:D}{x:D⊢\mathsf{unfold}x:D\to \mathsf{Nat}}}\mathrm{T}-\mathrm{Unfold}\\ x:D⊢x:D\end{array}}{x:D⊢(\mathsf{unfold}x)x:\mathsf{Nat}}\mathrm{T}-\mathrm{App}.$$ Consequently $$\cdot ⊢\delta :D\to \mathsf{Nat},\cdot ⊢{\mathsf{fold}}_D\delta :D,$$ and one application derives $\cdot ⊢{\mathrm{\Omega }}_D:\mathsf{Nat}$.

The displayed beta step followed by E-UnfoldFold gives ${\mathrm{\Omega }}_D{⟼}^2{\mathrm{\Omega }}_D$. Induct on $k$. The case $k=0$ is the empty trace. If ${\mathrm{\Omega }}_D{⟼}^{2k}{\mathrm{\Omega }}_D$, append the two-step cycle to obtain ${\mathrm{\Omega }}_D{⟼}^{2k+2}{\mathrm{\Omega }}_D$. Hence a return trace exists for every $2k$, and the deterministic term never reaches a value.

For $D_A=\mu X.(X\to A)$, assume $f:A\to A$. Under $x:D_A$, $(\mathsf{unfold}x)x:A$, so $f((\mathsf{unfold}x)x):A$ and ${\delta }_f:D_A\to A$. Thus $${\delta }_f({\mathsf{fold}}_{D_A}{\delta }_f):A,{\mathsf{Fix}}_A:(A\to A)\to A.$$ For a closed function value $v:A\to A$, write $q_v={\delta }_v({\mathsf{fold}}_{D_A}{\delta }_v)$. The eager compatible reduction is $${\mathsf{Fix}}_{A}v⟼q_v⟼v((\mathsf{unfold}({\mathsf{fold}}_{D_A}{\delta }_v))({\mathsf{fold}}_{D_A}{\delta }_v))⟼v(q_v).$$ This is the precise unfolding equation. It does not assert that the eager application $v(q_v)$ subsequently terminates.

Write $$L=\mu X.(\mathsf{Nat}\times X+\mathsf{Unit}),B=\mathsf{Nat}\times L+\mathsf{Unit}.$$ Ignoring duplicate pairs after their first visit, a left-to-right queue run visits The last two children have already been visited, so the queue empties and the algorithm accepts.

If the right root is $B^{\prime }=\mathsf{Bool}\times L+\mathsf{Unit}$, the exposed sums still match. Their product children enqueue $(\mathsf{Nat},\mathsf{Bool})$ and $(L,L)$. The first of these is the first rejecting pair: its constructor heads are distinct base types.

Using the chapter’s abbreviations $P$ and $B$, the run is There are exactly four beta steps.

Call by name has no argument context, so $$(\lambda x:\mathsf{Nat}.0){\mathrm{\Omega }}_{\mathsf{Nat}}⟼0P-Beta.$$ Under the proposed call-by-value mutation, the beta root is unavailable until the argument is a value. The argument context lifts the self-loop ${\mathrm{\Omega }}_{\mathsf{Nat}}⟼{\mathrm{\Omega }}_{\mathsf{Nat}}$ to $$(\lambda x.0){\mathrm{\Omega }}_{\mathsf{Nat}}⟼(\lambda x.0){\mathrm{\Omega }}_{\mathsf{Nat}}.$$ Repeating this step gives an infinite sequence, so the application never reaches $0$.

Assume $F(d)=d$. Induction on $n$ gives $F^n(\mathrm{\perp }){⊑}_{\mathsf{D}}d$: the base is leastness of $\mathrm{\perp }$, and $$F^{n+1}(\mathrm{\perp })=F(F^n(\mathrm{\perp })){⊑}_{\mathsf{D}}F(d)=d$$ uses monotonicity and the fixed-point equation. Therefore $\underset{n}{⨆}{F}^n(\mathrm{\perp }){⊑}_{\mathsf{D}}d$.

For the counterexample, take the pointed omega-chain $C=\{0{⊑}_{\mathsf{D}}1{⊑}_{\mathsf{D}}\cdots {⊑}_{\mathsf{D}}\omega \}$ and define The map is monotone: all finite inputs have the same image, and that image is below $G(\omega )$. It is not continuous, since $$G(\underset{n}{⨆}n)=G(\omega )=\omega \ne 0=\underset{n}{⨆}G(n).$$ Thus monotonicity alone does not justify the join calculation in the fixed- point proof.

Let $a_0=\mathrm{\perp }$ and $a_{i+1}=\mathsf{cons}(0,a_i)$. Its lub $z$ is the infinite all-zero list. The images form $$\mathrm{\perp }{⊑}_{\mathsf{D}}\uparrow \mathsf{inr}(0,\mathrm{\perp }){⊑}_{\mathsf{D}}\uparrow \mathsf{inr}(0,\mathsf{cons}(0,\mathrm{\perp })){⊑}_{\mathsf{D}}\cdots .$$ Using the componentwise product order and the lifting lub, $$\underset{i}{⨆}\mathsf{out}(a_i)=\uparrow \mathsf{inr}(0,\underset{i}{⨆}{a}_i)=\uparrow \mathsf{inr}(0,z)=\mathsf{out}(z).$$

A chain in $\mathcal{L}$ that reaches a finite word ending in $\mathsf{nil}$ is constant from that stage onward: such a total finite word has no strict extension in the partial-list order. Equivalently, if the lub reveals nil after a finite prefix, compactness of that finite total word puts the same observation in some chain member, after which the chain is constant.

Now take a chain in $(\mathbf{1}+\mathbb{N}\times \mathcal{L}{)}_{\mathrm{\perp }}$. If it is constantly bottom, its image under $\mathsf{in}$ is constantly $\mathrm{\perp }$. Otherwise it has a first nonbottom member. The separated-sum tag cannot subsequently change. For the left tag the chain is constantly $\uparrow \mathsf{inl}(\ast )$, and the image is constantly $\mathsf{nil}$. For the right tag discreteness of $\mathbb{N}$ fixes one head $n$, while the tails form a chain $(d_i)$; hence $$\mathsf{in}(\underset{i}{⨆}\uparrow \mathsf{inr}(n,d_i))=\mathsf{cons}(n,\underset{i}{⨆}{d}_i)=\underset{i}{⨆}\mathsf{cons}(n,d_i).$$ These exhaustive cases prove that $\mathsf{in}$ preserves omega-chain lubs. The same cases prove monotonicity, so it is continuous.

Suppose the final typing rule has premise $\mathrm{\Gamma },x:A⊢e:A$, let $\eta {\mathcal{R}}_{\mathrm{\Gamma }}\gamma$, and put $$F(d)=[[e]]\eta [x\mapsto d],q=\mathsf{fix}x:A.e[\gamma ].$$ We prove $F^k(\mathrm{\perp }){\mathcal{R}}_{A}q$ by induction on $k$. Bottom is related to every closed term by admissibility’s bottom clause. At the inductive step, the exact environment invariant is $$\eta [x\mapsto F^k(\mathrm{\perp })]{\mathcal{R}}_{\mathrm{\Gamma },x:A}\gamma [x\mapsto q].$$ The body case of the fundamental induction therefore gives $$F^{k+1}(\mathrm{\perp }){\mathcal{R}}_{A}e[\gamma ,q/x].$$ But P-Unroll gives $q⟼e[\gamma ,q/x]$. Finite anti-reduction on the term argument turns the preceding judgment into $F^{k+1}(\mathrm{\perp }){\mathcal{R}}_{A}q$.

Finally, the predicate $d\mapsto d{\mathcal{R}}_{A}q$ is admissible by lemma 24.37: it contains bottom and is closed under lubs of omega-chains. Applying the lub clause to the Kleene chain gives $$\mathrm{lfp}(F)=\underset{k}{⨆}{F}^k(\mathrm{\perp }){\mathcal{R}}_{A}q,$$ which is exactly the P-Fix conclusion.

For recursive values, suppose $\mathsf{fold}v{\approx }_{n+1}^{\mu X.A}\mathsf{fold}w$. The defining clause gives $v{\approx }_n^{A[\mu X.A/X]}w$. At target index zero the value relation is universal. At target $m+1\le n+1$, we have $m\le n$, so the induction hypothesis gives $v{\approx }_m^{A[\mu X.A/X]}w$, and the recursive clause restores $\mathsf{fold}v{\approx }_{m+1}^{\mu X.A}\mathsf{fold}w$.

For arrows, suppose $f{\approx }_{n+1}^{A\to B}g$. Again index zero is immediate. If $m+1\le n+1$, take any $j\le m+1$ and any $a{\approx }_j^{A}b$. Since also $j\le n+1$, the original arrow clause already gives $fa{\mathcal{E}}_j^{B}gb$. This is precisely the arrow clause at $m+1$.

For the copier, retain the chapter’s abbreviations $$h=\mathsf{fold}\theta ,r=(\mathsf{unfold}h)h,g=\lambda xs.\mathsf{copyBody}rxs.$$ The promised two steps are $$r=(\mathsf{unfold}(\mathsf{fold}\theta ))h⟼\theta h⟼g,$$ first by E-UnfoldFold, then by call-by-value beta. For a cons value, the remaining administrative betas expose $$\mathsf{caseList}(\mathsf{cons}kys)\mathsf{of}\{\cdots \}{⟼}^{\ast }\mathsf{cons}k(gys).$$ This prefix evaluates $r$ to $g$, unfolds the folded input by E-UnfoldFold, and then uses the right sum-case root. The structural induction hypothesis is used exactly on $gys{⟼}^{\ast }ys$; compatible closure lifts that sequence through the argument position of $\mathsf{cons}k[-]$, equivalently through the pair, right-injection, and fold constructor contexts. Thus $$\mathsf{cons}k(gys){⟼}^{\ast }\mathsf{cons}kys.$$

At an arbitrary $n$, fundamental reflexivity with equal empty substitutions gives $v{\mathcal{E}}_n^{\mathsf{ListNat}}v$. Structural convergence gives $\mathsf{copy}v{⟼}^{\ast }v$. Apply the two-sided anti-reduction clause with this left prefix and an empty right prefix to obtain $\mathsf{copy}v{\mathcal{E}}_n^{\mathsf{ListNat}}v$.

The classifications are:

1. Preservation of the type of ${\mathrm{\Omega }}_D$ is a safety claim. It constrains every finite reduct but does not assert that a value appears.

2. A division procedure that returns the quotient whenever it returns with a nonzero divisor satisfies partial correctness. Termination is not part of that implication.

3. The assertion that every recursive call to $\mathsf{plus}$ returns is a termination claim.

4. The assertion that every finite observation of the all-zero lazy list reveals another cons cell is productivity.

5. The assertion that $\mathsf{plus}$ terminates on all numeral inputs and returns their mathematical sum is totality: termination and partial correctness are both present.

The examples are deliberately not interchangeable. In particular, ${\mathrm{\Omega }}_D$ is safe without terminating, while productivity describes all finite tail observations of a domain element rather than return of an eager infinite value.

Inverting a typed Pr-Unroll redex gives $$\mathrm{\Gamma },p:P⊢e:P,\mathrm{\Gamma }⊢\mathsf{fix}p:P.e:P.$$ Term substitution with the second judgment in the first yields $$\mathrm{\Gamma }⊢e[\mathsf{fix}p:P.e/p]:P,$$ which is the type of the reduct. This proves preservation for the root.

Preservation says only that a step retains its type. For ${\omega }_P=\mathsf{fix}p:P.p$, Pr-Unroll is the self-loop ${\omega }_P⟼{\omega }_P$, so normalization fails despite preservation. At $P=\mathbf{0}$, rule Pr-Fix derives the closed inhabitant ${\omega }_{\mathbf{0}}:\mathbf{0}$. Thus the syntactic consistency statement “there is no closed term of type $\mathbf{0}$” is already false even though evaluation produces no empty-type value.

At index zero every pair of closed values of the same type is related. A list fold at index $n+1$ consumes one index and compares its sum payload at index $n$.

For $(v_0,v_1)$, index one reaches payload index zero, so the different $\mathsf{inl}$ and $\mathsf{inr}$ payloads are still related. At index two the fold clause reaches the sum clause at index one; the tags differ, so the pair is not related. The least index is $2$.

For $(v_1,v_2)$, index two follows $$\text{fold at }2⟶\text{right sum at }1⟶\text{product at }1⟶0{\approx }_1^{\mathsf{Nat}}1,$$ and the last judgment is false. Index one again stops at the universal payload relation, so the least index is $2$.

For $(v_3,v_4)$, index two compares the common outer head $0$ and their tails at list index one, which consumes to payload index zero; hence they are related. At index three the clauses traverse The final natural clause fails. Thus the least distinguishing index is $3$.

For $p=\mathrm{\perp }$, strict case analysis makes $F_p$ the constant-bottom map, so $F_p^i(\mathrm{\perp })=\mathrm{\perp }$ for every $i$ and $\mu \mathrm{\Phi }(\mathrm{\perp })=\mathrm{\perp }$. For $p=0$, $F_p$ is the constant-zero map: $$F_0^0(\mathrm{\perp })=\mathrm{\perp },F_0^i(\mathrm{\perp })=0(i\ge 1),\mu \mathrm{\Phi }(0)=0.$$ For $p=k+1$, $F_p={\mathsf{succ}}_{\mathrm{\perp }}$. Because this operation is strict, every iterate starting at bottom is bottom, and therefore $\mu \mathrm{\Phi }(k+1)=\mathrm{\perp }$.

It remains to check preservation of chain lubs by the resulting parameter map. A chain in the flat domain either remains bottom, or reaches one fixed numeral and is constant thereafter. In the first case both sides of the continuity equation are bottom. If the numeral is zero, the image chain is eventually zero and has lub zero. If it is positive, the image chain is constantly bottom. In all cases $$\mu \mathrm{\Phi }(\underset{i}{⨆}{p}_i)=\underset{i}{⨆}\mu \mathrm{\Phi }(p_i),$$ which directly verifies the conclusion of the parameterized fixed-point lemma for this $\mathrm{\Phi }$.

For a closed list value $v$, call by value gives $$K[v]=(\lambda xs.{\mathrm{\Omega }}_D)v⟼{\mathrm{\Omega }}_D,$$ after which the two-step cycle repeats forever. For the copied argument, the argument position is evaluated first. Structural convergence supplies $$K[\mathsf{copy}v]{⟼}^{\ast }(\lambda xs.{\mathrm{\Omega }}_D)v⟼{\mathrm{\Omega }}_D,$$ so this term also diverges.

For every numeral $m$, neither plugged term satisfies $\Downarrow m$. The contextual biconditional of theorem 24.51 is therefore $\mathsf{false}⟺\mathsf{false}$, and is true. The stronger assertion that both terms converge is false. Observational equivalence preserves any numeral that is produced; it does not manufacture convergence inside a diverging context.

The body of ${\mathrm{\Omega }}_{\mathsf{Nat}}$ denotes the identity map on ${\mathbb{N}}_{\mathrm{\perp }}$. Its Kleene chain is $$\mathrm{\perp }{⊑}_{\mathsf{D}}\mathsf{id}(\mathrm{\perp })=\mathrm{\perp }{⊑}_{\mathsf{D}}{\mathsf{id}}^2(\mathrm{\perp })=\mathrm{\perp }{⊑}_{\mathsf{D}}\cdots ,$$ so $[[{\mathrm{\Omega }}_{\mathsf{Nat}}]]=\mathrm{\perp }$. If this closed typed term converged to a numeral $n$, the operational-to-denotational direction of adequacy would give $\mathrm{\perp }=n$, impossible in the flat domain. Progress and determinism leave an infinite reduction, which is the operational self-loop already displayed.

For addition, its semantic functional is $$H(f)(m)(n)={\mathsf{case}}_{{\mathbb{N}}_{\mathrm{\perp }}}(m,n,k\mapsto {\mathsf{succ}}_{\mathrm{\perp }}(f(k)(n))).$$ The third finite approximant already gives $$H^3(\mathrm{\perp })(2)(1)={\mathsf{succ}}_{\mathrm{\perp }}(H^2(\mathrm{\perp })(1)(1))={\mathsf{succ}}_{\mathrm{\perp }}(2)=3.$$ Later approximants agree there, so $[[\mathsf{plus}21]]=3$. The denotational-to- operational direction of adequacy recovers $\mathsf{plus}21\Downarrow 3$. Conversely, applying the operational- to-denotational direction to the chapter’s displayed run recovers the same semantic equality. The two uses are logically distinct.

Put $B=\mathsf{Unit}+\mathsf{Nat}\times L$. From $\cdot ⊢p:B$, the iso-recursive derivation is $$\frac{{\displaystyle \frac{\cdot ⊢p:B}{\cdot ⊢{\mathsf{fold}}_{L}p:L}}\mathrm{T}-\mathrm{Fold}}{\cdot ⊢\mathsf{unfold}({\mathsf{fold}}_{L}p):B}\mathrm{T}-\mathrm{Unfold}.$$ Since $p$ is a value, $$\mathsf{unfold}({\mathsf{fold}}_{L}p)⟼pE-UnfoldFold.$$ This is an object-language operational contraction.

For equi-recursive equality, initialize the worklist by $(L,B)$. Exposing the left root gives $B$, so the matching sum heads enqueue $(\mathsf{Unit},\mathsf{Unit})$ and $(\mathsf{Nat}\times L,\mathsf{Nat}\times L)$. The product pair enqueues $(\mathsf{Nat},\mathsf{Nat})$ and $(L,L)$. Exposing $(L,L)$ only recreates already visited pairs, so the worklist empties and the algorithm accepts $L{\equiv }_{\mu }B$. This is a metalevel type-equality decision on finite graphs. It is neither a term reduction nor a premise used by T-Fold, T-Unfold, or E-UnfoldFold in the iso-recursive calculus.