Recursive Domain Semantics and Computational Adequacy

Proof. Induction on the typing derivation of $M$. For each term former, the grammar of $E$ contains exactly one clause with a hole in the position that the transition rules inspect, and the side conditions ($V$ before $E$ in $⟨V,E⟩$ and $VE$) make the decomposition deterministic. If the inspected subterm is already a value, the term itself is a redex or a value, which is the base case; if it is not, the induction hypothesis decomposes it and the surrounding former extends the context. Type preservation is checked clause by clause: each redex transition replaces a term by one of the same type, substitution preserves typing, and the operation clause returns an argument of the same type as the whole. ◻

Proof. Define computability predicates on closed terms by induction on types. A value of type $\iota$, $o$ or $\mathbf{1}$ is computable. A value $⟨V,V^{\prime }⟩$ is computable when $V$ and $V^{\prime }$ are. A value $\lambda (x:\sigma ).M$ is computable when $M[V/x]$ is computable for every computable value $V:\sigma$. A closed term is computable when every transition sequence from it terminates in a computable value or in a term $E⟨a()⟩$.

Two facts are proved simultaneously by induction on typing derivations: every closed well-typed term is computable, and every well-typed term with free variables is computable under substitution of computable values. The cases for $0$, $\mathsf{tt}$, $\star$ and pairs are immediate. For $\mathsf{succ}$, $\mathsf{pred}$, $\mathsf{zero}$, ${\mathsf{pr}}_i$ and the conditional, the induction hypothesis gives that the scrutinee’s transition sequences terminate; by lemma 154.3 the surrounding context then exposes a redex whose transition is one of the displayed clauses, and the result is again computable, in the conditional case by the induction hypothesis for the chosen branch. For application, the induction hypothesis makes the function’s sequences terminate at a computable $\lambda (x:\sigma ).M$ and the argument’s at a computable $V$, and computability of the abstraction gives computability of $M[V/x]$. For $f(M_1,\dots ,M_n)$, the term is already a redex: each labelled transition leads to some $M_i$, computable by hypothesis, and the branching is finite because $\mathrm{ar}(f)$ is. Since every branch is finite and branching is finite, König’s lemma gives that the whole tree is finite. ◻

Proof. $(\Rightarrow )$ Induction on the finite transition tree of $M$, whose finiteness is theorem 154.5; each clause of definition 154.4 matches one rule. $(\Leftarrow )$ Induction on the derivation of $M\Downarrow t$: each rule has strictly smaller subderivations for the continuations, and the second rule reduces the term, so the derivation exhibits a finite tree and the value it computes is exactly $|M|$. Determinacy of the first two cases is lemma 154.3. ◻

Proof. Monotonicity of $e_k$ is immediate. For $p_k$, truncation is defined by recursion on depth and preserves the three order clauses. The first equation holds because truncating at depth $k$ an element already of depth at most $k$ changes nothing. For the inequality, truncation only replaces subtrees by $\mathrm{\perp }$, which is smaller. ◻

Proof. Dcppo. A directed set of sequences has componentwise suprema, and each $T_k$ is a finite-height poset in which every directed subset with a common shape has a supremum: two elements of $T_k$ with an upper bound have the same head, so a directed subset is either $\{\mathrm{\perp }\}$-cofinal or has a common head, and the supremum is computed headwise by induction on $k$. Compatibility with $p_k$ is preserved by suprema because $p_k$ is monotone and, being defined by truncation, preserves the headwise suprema just described. The constantly-$\mathrm{\perp }$ sequence is least.

Isomorphism. A compatible sequence $(t_k)$ has $t_0=\mathrm{\perp }$ and, if $t_1\ne \mathrm{\perp }$, a determined head that is either an element of $X$ — in which case every later component is that element — or an operation symbol $f$, in which case the components of the $n$ argument sequences are $t_{k+1}$’s arguments and are themselves compatible. This is exactly the inverse of $\mathrm{\Theta }$, and both directions are monotone.

Freeness. Given $h:X\to D$ define $\hat{h}(t):=\underset{k}{⨆}{h}_k(t_k)$ where $h_k:T_k\to D$ is defined by $h_0(\mathrm{\perp })=\mathrm{\perp }$, $h_{k+1}(\mathrm{\perp })=\mathrm{\perp }$, $h_{k+1}(x)=h(x)$ and $h_{k+1}(f(\overrightarrow{t}))=f_D(h_k(t_1),\dots ,h_k(t_n))$. Each $h_k$ is monotone and $h_k=h_{k+1}\circ e_k$, so the family is increasing along the sequence and the supremum exists. Strictness and preservation of the operations are read off from the clauses, and continuity holds because directed suprema in ${\mathrm{CT}}_{\mathrm{\Sigma }}(X)$ are computed componentwise and each $f_D$ is continuous. Uniqueness: a strict continuous homomorphism $g$ with $g\circ \eta =h$ agrees with $\hat{h}$ on every element of finite depth by induction on that depth, and every $t$ is the directed supremum $\underset{k}{⨆}\mathrm{\Theta }$-image of its truncations, so continuity forces $g=\hat{h}$. ◻

Proof. Exhaustiveness and exclusivity: by lemma 154.3 the $⟶$-chain from $M$ is deterministic, so it is either infinite — the fourth case — or ends in a value, a labelled redex, or a constant, which are the first three. Compatibility: truncating $|M{|}^{(k+1)}$ at depth $k$ gives $|M{|}^{(k)}$ by induction on $k$, since each clause applies the same case analysis one level down. The displayed equation is the case analysis read at the level of the whole tree, using that unlabelled steps do not change the medium-step behaviour. Leastness: let $g$ be any solution of the displayed equation. Then $|M{|}^{(k)}{⊑}_{\mathsf{D}}g(M)$ for every $k$, by induction on $k$: at $k=0$ because $\mathrm{\perp }$ is least, and at $k+1$ because the clause defining $|M{|}^{(k+1)}$ and the clause of the equation for $g$ have the same head, with the induction hypothesis applied to the arguments. Hence $|M|=\underset{k}{⨆}|M{|}^{(k)}{⊑}_{\mathsf{D}}g(M)$. ◻

Proof. Induction on $V$. The constants $0$, $\mathsf{tt}$, $\mathsf{ff}$, $\star$ are interpreted by $\eta$ after a map into the corresponding object. $\mathsf{succ}(V)$ is $\eta \circ s$ applied to the factorization for $V$. A pair is the pairing of two factorizations followed by $\eta$, using that $\eta$ is monoidal for the strength. An abstraction is interpreted by $\eta$ after currying, since currying produces a $\mathcal{C}$-map into the exponential. No clause introduces $(-{)}^{†}$, and $f_x$ occurs in no value. ◻

Proof. Each $\beta$-equation is verified by unfolding the clauses of definition 154.14 and using the monad laws; lemma 154.15 is what makes the substitution $M[V/x]$ correspond to precomposition rather than to a Kleisli extension. The algebraicity schema is exactly the naturality assumption of convention 154.13: interpreting an evaluation context yields a Kleisli map $g$, and the schema becomes $g^{†}\circ f=f\circ (g^{†}{)}^n$. The unfolding equation holds because $Y(G)=G(Y(G))$ for the least fixed point of a continuous $G$, and $G$ is continuous since composition and currying are continuous in the enrichment. ◻

Proof. By theorem 154.5 and proposition 154.6, $M\Downarrow |M|$. An induction on that derivation, using the corresponding equations of lemma 154.16 at each rule, gives $⊢M=|M|:\sigma$ in the equational theory; and lemma 154.16 turns that into $[[M]]=[[|M|]]$. ◻

Proof. ${\mathcal{C}}_T(1,[[\sigma ]])$ is a dcppo by convention 154.13 and carries a continuous $\mathrm{ar}(f)$-ary operation for each $f$, induced by $f_{[[\sigma ]]}$; so it is a continuous $\mathrm{\Sigma }$-algebra. Apply the freeness clause of theorem 154.10 to $h(V):=[[V]]$. ◻

Proof. Induction on $k$. For $k=0$ the left side is $\mathrm{\perp }$. For $k+1$ examine the four cases of definition 154.11. If $M\Downarrow V$ then $M{⟶}^{\ast }V$, and each unlabelled step is an instance of an equation of lemma 154.16, so $[[M]]=[[V]]$. If $M{\Downarrow }^{f_i}{N}_i$ then likewise $[[M]]=[[f(N_1,\dots ,N_n)]]=f_{[[\sigma ]]}([[N_1]],\dots ,[[N_n]])$, and the induction hypothesis together with monotonicity of $f_{[[\sigma ]]}$ gives the claim. If $M{\Downarrow }_a$ then $[[M]]=[[a()]]$. If $M\uparrow$ the left side is $\mathrm{\perp }$. The final statement follows because $[[-]]$ is continuous by lemma 154.18 and $|M|=\underset{k}{⨆}|M{|}^{(k)}$. ◻

Proof. Repeat the computability argument of theorem 154.5, saying now that a closed term is computable when every transition sequence from it terminates in a computable value or in a term $E⟨a()⟩$ or $E⟨{\mathrm{\Omega }}_{\tau }⟩$. The only new cases are the two ${\mathsf{Rec}}_n$ clauses. For ${\mathsf{Rec}}_0$ the reduct is an abstraction whose body is ${\mathrm{\Omega }}_{\tau }$, computable because every sequence from ${\mathrm{\Omega }}_{\tau }$ is already stuck in the required form. For ${\mathsf{Rec}}_{n+1}$ the reduct is an abstraction whose body mentions ${\mathsf{Rec}}_n$, computable by an inner induction on $n$. ◻

Proof. Induction on the derivation of $M^{\prime }\prec M$. The relation is defined by compatible closure, so a value on the left forces the same outermost former on the right except in the two base cases, and $\mathrm{\Omega }$ is not a value. For the second clause, the grammar of evaluation contexts is the same in both languages, so the unique decomposition of lemma 154.3 on the left is matched on the right former by former. The transition clauses are checked one by one; the only interesting one is ${\mathsf{Rec}}_{n+1}(f,x.M^{\prime })⟶\lambda (x:\sigma ).M^{\prime }[{\mathsf{Rec}}_n/f]$, whose right-hand counterpart unfolds $\mathsf{Rec}$ once, and ${\mathsf{Rec}}_n\prec \mathsf{Rec}$ holds by definition, so the substituted bodies remain related because $\prec$ is closed under substitution of related terms. ◻

Proof. The inequality is proved by induction on the length of the terminating $\mathcal{A}$-sequence supplied by lemma 154.21, using lemma 154.22 at each step: a value on the left forces the same value on the right; a stuck $\mathrm{\Omega }$ contributes $\mathrm{\perp }$; and a labelled step is matched, so the heads agree and the induction hypothesis applies to the arguments. Directedness: given $M_1^{\prime },M_2^{\prime }\prec M$, replace every ${\mathsf{Rec}}_{n_i}$ by ${\mathsf{Rec}}_{max(n_1,n_2)}$ and every $\mathrm{\Omega }$ by the corresponding subterm of the other approximant where it is not $\mathrm{\Omega }$; the result is an upper bound below $M$. For the supremum, it suffices to produce, for each $k$, an $M^{\prime }\prec M$ with $|M{|}^{(k)}{⊑}_{\mathsf{D}}|M^{\prime }|$; take $M^{\prime }$ to be $M$ with every $\mathsf{Rec}$ replaced by ${\mathsf{Rec}}_k$, which by lemma 154.22 matches the first $k$ levels of the transition tree. ◻

Proof. $[[|M|]]{⊑}_{\mathsf{D}}[[M]]$ is lemma 154.19. For the converse, definition 154.14 interprets each $\mathsf{Rec}$ by a directed supremum of its approximants, and composition, pairing, currying and $(-{)}^{†}$ are continuous in the enrichment of convention 154.13; hence $$[[M]]=⨆\{[[M^{\prime }]]\mid M^{\prime }\prec M\text{closed}\}.$$ Each $M^{\prime }$ is a term of $\mathcal{A}$, which is recursion-free by lemma 154.21, so theorem 154.17 applies verbatim with the extra clause $[[{\mathrm{\Omega }}_{\sigma }]]=\mathrm{\perp }=[[|{\mathrm{\Omega }}_{\sigma }|]]$ and gives $[[M^{\prime }]]=[[|M^{\prime }|]]$. By proposition 154.23 the family $\{|M^{\prime }|\}$ is directed with supremum $|M|$, and $[[-]]$ on trees is continuous by lemma 154.18. Combining, $$[[M]]=\underset{M^{\prime }\prec M}{⨆}[[M^{\prime }]]=\underset{M^{\prime }\prec M}{⨆}[[|M^{\prime }|]]=[[\underset{M^{\prime }\prec M}{⨆}|M^{\prime }|]]=[[|M|]].$$ ◻

Proof. $[[M]](\ast )=[[|M|]](\ast )$ by theorem 154.17. Since $[[-]]$ on effect values is the unique $\mathrm{\Sigma }$-homomorphism and $\mathsf{or}$ is union, $[[t]](\ast )=\bigcup _{V\in h(t)}[[V]](\ast )$ by induction on $t$. Finally $h(|M|)=\{V\mid M{\Downarrow }_{\mathsf{n}}V\}$ by example 154.25. ◻

Proof. At a ground type distinct values have distinct denotations and every element of the interpreting set is the denotation of exactly one value, so the $\mathrm{\Sigma }$-homomorphism of lemma 154.18 sends a tree to the set of values labelling its leaves, with $\mathrm{\perp }$ contributing nothing. Now apply theorem 154.24 and read off both directions. ◻