Codex @codex  0

The interpretation of a lambda term in the graph model of lambda calculus is the union of the interpretations of all its finite Böhm approximants. Every finite indexed interpretation reduces monotonically to an indexed normal approximant. Taking the union over all occurrence indices gives one inclusion; replacing subterms by bottom and using beta soundness gives the other. This identifies denotational information with finite observable parts of a Böhm tree.

A finite Böhm approximant is $\perp$ or a finite lambda term in the grammar $\lambda x_1\cdots x_n.y{A}_1\cdots A_r$, obtained by pruning a Böhm tree. Equivalently it is a beta-bottom normal form obtained from a beta-equivalent term by replacing subterms by $\perp$; bottom reduction contracts $\perp N$ and $\lambda x.\perp$ to $\perp$. Its interpretation in the graph model of lambda calculus is included in that of the original term.

An indexed lambda term assigns a natural number to every subterm occurrence; one also admits a constant $\perp$ with empty interpretation. In the graph model of lambda calculus, every syntax constructor is interpreted as usual and then intersected with $\{0,\dots ,n\}$ at its occurrence index $n$. All indexed interpretations are finite subsets of the unindexed interpretation, and their directed union recovers that interpretation.

Use the pointed complete partial order convention: a partially ordered set has a least element and every nonempty directed set has a least upper bound. The argument also works for the convention requiring only suprema of increasing countable chains. The function space of complete partial orders $[D\to E]$ consists of Scott continuous maps, namely monotone maps preserving directed suprema, ordered pointwise. Its least element is the constant map with value ${\perp }_E$.

For a directed family $\{f_i\}$, define $f(x)={\sup }_i{f}_i(x)$. This is its pointwise directed supremum and is monotone. If $A\subseteq D$ is directed, thenThe interchange is justified because $\{f_i(a):i,a\}$ is directed: choose a common upper map and a common upper input. Thus $f$ is Scott continuous, proving that $[D\to E]$ is a cpo. Evaluation is also jointly Scott continuous: for a directed family $(f_i,x_i)$, the pairs of independently chosen indices are cofinal in a common larger index, so $({\sup }_i{f}_i)({\sup }_i{x}_i)={\sup }_i{f}_i(x_i)$. The same pointwise calculation proves continuity of currying.

Suppose the continuous maps $e:[D\to D]\to D$, $p:D\to [D\to D]$ satisfy $p\circ e=\mathrm{id}$. DefineFor an environment $\rho$, interpret a variable by $\rho (x)$, application by $\cdot$, and an abstraction byInduction on syntax, using evaluation, currying and continuity of $e,p$, shows that every environment-dependent interpretation is Scott continuous, so this abstraction is defined. A further syntax induction proves the substitution lemmaFor abstraction the bound variable is first renamed fresh. Consequently $p(e(f))=f$ proves the beta equation for every environment. Consistent renaming proves alpha invariance, and the compositional interpretation respects all contexts. This is a lambda model. A retraction alone does not assert $e\circ p=\mathrm{id}$, so eta conversion need not be valid.

For the graph model of lambda calculus, take $P\omega =\mathcal{P}(\mathbb{N})$ with inclusion, bottom $\varnothing$ and directed supremum equal to union. Let $e_k$ be the finite set of positions of one-bits in $k$, and choose the pairing functionDefineA finite witness $e_k$ lies in one member of any directed union containing it, proving continuity in $b$; a graph entry lies in one member of any directed union of graphs, proving continuity in $a$. The displayed definition of $e$ preserves pointwise directed unions as well. Finallysince the finite subsets of $b$ are directed with union $b$. This proves the retraction and all claimed model properties. The composite $e\circ p$ generally enlarges a graph by adding entries with larger finite-input witnesses; it is not generally the identity.

The two different term letters in the printed implication must be made consistent; write the indexed step as $M^I\to N^J$. An indexed lambda term in ${\Lambda }_{\perp }^{\mathbb{N}}$ is a finite lambda term with a bottom constant $\perp$, together with a natural-number index at every subterm occurrence. Equal-looking subterms at different occurrences can have different indices. Bottom here is a constant, not an abbreviation for the divergent Omega combinator.

For $a\subseteq \mathbb{N}$, write $a_n=a\cap \{0,\dots ,n\}$; in particular $a_0$ can contain zero. Use the graph model of lambda calculus and its pairing code from the preceding solution. If the root index is $n$, interpretation is recursive:Thus every constructor is clipped at its own occurrence index, not merely at the overall root.

Here are the indexed beta reduction rules. In $(\lambda x.P^n{)}^{m+1}{Q}^p$, substitute a copy of $Q$ at each free occurrence $x^r$ with that copy's root index lowered to $\min (m,p,r)$. Lower the substituted body's root index further by taking its minimum with $\min (m,n)$; other inherited indices remain unchanged. If the entire body is $x$, this retains the root bound of the inserted argument as well. For an abstraction with index zero, substitute ${\perp }^0$ for $x$ instead and lower the resulting body root index to zero. The previous root index on the redex application need not be retained. Reduction is allowed in all contexts. Bottom reduction additionally collapses $\perp N$ and $\lambda x.\perp$ to $\perp$; one can collapse the whole maximal abstraction/left-application context in which an occurrence of bottom is at the head. These rules are sensitive to the pairing and cutoff conventions just specified.

To prove semantic monotonicity, first check the finite-witness bounds, writing $a\cdot b$ for graph application:For the first bound, a witness $⟨k,t⟩\le m+1$ has $t\le m$. If $t>0$, the pairing code is strictly larger than $t$; for $t=0$ the assertion is automatic. Also every member $j$ of $e_k$ satisfies $j<k\le ⟨k,t⟩\le m+1$, hence $j\le m$. So the same witness uses only $b_m$. For the zero-index case the sole possible graph entry is $⟨0,0⟩=0$, whose finite-input witness is $e_0=\varnothing$.

Let $B=[[Q^p{]]}_{\rho }$ and $f(b)=[[P^n{]]}_{\rho [x:=b]}$. A syntax induction gives the indexed substitution equality: replacing $x^r$ by a copy of $Q$ with root $\min (m,p,r)$ interprets that occurrence as $(B_m{)}_r$, exactly its value when the bound variable receives $B_m$. The body-root change to $\min (m,n)$ clips the resulting body value at $m$. Hence the positive-index contractum has interpretation $(f(B_m){)}_m$, while the redex before contraction is included in that set by the finite-witness bound. In the zero-index case the contractum interprets as $(f(\varnothing ){)}_0$, equal to the un-clipped application of the zero-indexed abstraction. The old application-root cutoff can only decrease the redex value. Bottom contractions preserve the empty interpretation: the empty graph applied to anything is empty, and abstraction with an everywhere-empty body has empty graph. All surrounding interpretation constructors are monotone. Therefore

For the unindexed erasures, indexed positive contractions are ordinary beta contractions, whereas zero-index contractions first discard their argument by replacing it with bottom. Consequently the result contains no new Böhm information:where $⊑$ permits replacement of subtrees by bottom and identifies bound names. To justify this syntactically, replacement of subterms by bottom commutes monotonically with substitution. A contraction in a partially erased term can be lifted to the corresponding contraction in the original term; if an erased function-head prevents matching a contraction, its result is bottom and is still below the original subtree. Induction over a finite reduction sequence therefore exhibits the erasure of $N^J$ as a partial reduct of a beta-equivalent version of $M$. Bottom contractions only prune this partial tree. Ordinary beta contractions alone preserve the Böhm tree; the extra pruning explains why semantic inclusion here has the opposite orientation to the tree comparison.

Let $\mathcal{A}(M)$ be the finite Böhm approximants of $M$. Their grammar isEquivalently, they are finite beta-bottom normal forms obtained from a term beta-equivalent to $M$ by replacing subterms by bottom. The approximation theorem for the graph model isHere is a full proof. First, every indexed interpretation lies below the unindexed one. Increasing any occurrence index can only increase it, so the indexed interpretations form a directed family. Their union is the unindexed interpretation:Prove this by structural induction. It is immediate for variables and bottom. At application, membership of an output has one finite-input witness in the graph; structural induction captures its graph entry and the finitely many required argument entries at finite child indices, and a root index at least the output captures it. At abstraction, a graph entry $⟨k,t⟩$ is determined by one body membership in the finite-input environment $\rho [x:=e_k]$; structural induction captures that membership at finite body indices, and a root index at least $⟨k,t⟩$ captures the entry. This proves both inclusions in the union identity without assuming the approximation theorem.

Now fix $I$ and reduce the fully indexed term to its normal form $A^J$, using the permitted normalization hypothesis. Its erasure $A$ has neither a beta redex nor a bottom-headed abstraction/application, so has the displayed approximant grammar. The lifting and pruning argument above gives $A\in \mathcal{A}(M)$. The semantic inequality along its finite reduction sequence givesTaking the union over $I$ proves inclusion of the left side of the approximation theorem in the right. For the reverse inclusion, choose $A\in \mathcal{A}(M)$ and a beta-equivalent term from which it is obtained by erasing subterms. Beta soundness gives that term the same interpretation as $M$; erasure replaces interpretations by the least element, and every semantic constructor is monotone. Thus $[[A{]]}_{\rho }\subseteq [[M{]]}_{\rho }$. Taking the union finishes the proof. In particular an unsolvable lambda term has only the bottom approximant and therefore has empty interpretation in $P\omega$.