Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 76 (The Lambda Calculus)

Write ${\to }^{\ast }$ for the reflexive closure of the transitive closure of a relation $\to$, and ${\leftrightarrow }^{\ast }$ for its generated equivalence relation. The diamond property requires every pair $a\to b,a\to c$ to admit a one-step join $b\to d\leftarrow c$. The Church-Rosser property requires a possibly longer join whenever $b{\leftrightarrow }^{\ast }c$. Equivalently, every pair of finite reductions with the same source has a common finite reduct. Identity steps may be included in the diamond convention without affecting the counterexample below.

Let $A=(\lambda z.z)y$ and consider the lambda term $M=(\lambda x.xx)A$. Contracting its outer beta-redex gives $AA$, whereas contracting the inner beta-redex gives $(\lambda x.xx)y$. The only one-step reducts of $AA$ are $yA$ and $Ay$; the other branch has the sole one-step reduct $yy$. These terms are different even under alpha equivalence. Thus one-step beta reduction has no diamond property. Both branches do reach $yy$ by finite beta reduction.

For the positive result, use parallel beta reduction $\Rightarrow$, with rulesStructural induction, renaming binders to avoid capture, proves the substitution lemma: $P\Rightarrow P^{\prime }$ and $Q\Rightarrow Q^{\prime }$ imply $P[x:=Q]\Rightarrow P^{\prime }[x:=Q^{\prime }]$. Define the complete development of a lambda term byand $(PQ{)}^{\bullet }=P^{\bullet }{Q}^{\bullet }$ when the application is not initially a root beta-redex. Induction on a parallel derivation, using the substitution lemma in the contracting case, provesConsequently any two parallel reducts have the common successor $M^{\bullet }$. The ordinary one-step relation is included in the parallel relation, and every parallel step expands into finitely many ordinary steps; their finite closures therefore coincide. A finite grid of parallel diamonds joins any two finite parallel reductions. Finally a finite zigzag of forward and backward reductions can be joined inductively using that confluence. Hence beta reduction has the Church-Rosser property, although its individual steps do not have the diamond property.

A fixed-point combinator is a closed lambda term $Z$ such that $ZF{\equiv }_{\beta }F(ZF)$ for every lambda term $F$. It suffices to check this for a fresh free variable $f$, since capture-avoiding substitution then gives every instance. TakeIf $GZ{\equiv }_{\beta }Z$, applying both sides to $f$ gives $Zf{\equiv }_{\beta }f(Zf)$. Conversely suppose $Z$ is a fixed-point combinator. Its application to a fresh $f$ has a head normal form, because it is beta equivalent to $f(Zf)$. Since $Z$ is closed, head reduction of $Zf$ must first expose a lambda abstraction in $Z$ itself. Thus $Z{\to }_{\beta }^{\ast }\lambda u.P$, andThis establishes the needed abstraction equality by beta reduction, without assuming eta conversion. Abstracting $Zf{\equiv }_{\beta }f(Zf)$ now gives $Z{\equiv }_{\beta }\lambda f.f(Zf){\equiv }_{\beta }GZ$.

Two examples are the Curry fixed-point combinator and the Turing fixed-point combinator:Writing $A_f=\lambda x.f(xx)$, we have $Yf{\to }_{\beta }{A}_f{A}_f{\to }_{\beta }f(A_f{A}_f){\equiv }_{\beta }f(Yf)$, while $\Theta f{\to }_{\beta }^{2}f(\Theta f)$. Different displayed syntax alone would not prove that the two combinators are distinct under beta equivalence. Here is a reduct invariant that does. Every finite reduct of $Y$ is $\lambda f.f^n(A_f{A}_f)$, up to alpha equivalence: $A_f$ is beta-normal and the one remaining beta-redex is its self-application. No such reduct contains the closed subterm $DD$.

Every finite reduct of $\Theta$, in contrast, retains a closed subterm $DD$. The contraction $DD\to \lambda f.f(DDf)$ recreates one. The only other redexes created by these expansions are abstractions applied to variables; contracting them substitutes a variable, so preserves any closed $DD$ inside their bodies. This describes all redexes inductively: expansion inserts only a variable-headed application and a copy of $DD$, and a variable substitution preserves that description. Thus every finite reduct contains $DD$. A common reduct of $Y$ and $\Theta$ is impossible, so the Church-Rosser theorem proves $Y/{\equiv }_{\beta }\Theta$.

Finally put $P=ZK$, with $K=\lambda xy.x$. The fixed-point combinator equation giveswhere $y$ is fresh. If $P$ had a head normal form with $n$ leading abstractions, then $\lambda y.P$ would have one with $n+1$. A reduct of a head normal form preserves its initial abstraction count and variable-headed spine: only its argument subterms can still contract. These two head normal forms therefore cannot have a common reduct, contradicting the Church-Rosser theorem. Hence $ZK$ is unsolvable.

Let $x_1,\dots ,x_s$ contain all free variables of $M$. The lambda term $M$ is a solvable lambda term if there are closed lambda terms $P_1,\dots ,P_k$ such thatAdditional arguments beyond the first $s$ are allowed. A head normal form is a term $\lambda u_1\cdots u_n.y{M}_1\cdots M_r$ with a variable at the head; its arguments need not be beta-normal.

If $M$ reduces to this head normal form, close its free variables and supply every resulting initial binder with the same closed projection(take $P=I$ when $r=0$). The head variable becomes $P$ and discards all $r$ argument terms, even divergent ones, leaving $I$. Thus a head normal form implies solvability.

Conversely suppose a closure and applications of $M$ yield $I$. The standardization theorem for beta reduction supplies a finite successful head-reduction sequence. Until $M$ exposes a head variable, its head contractions lie within $M$: a closing substitution cannot create a new head redex there, and supplied arguments cannot be used until an initial abstraction is exposed. Each such contraction commutes with the closing capture-avoiding substitution. Project the successful head computation back onto $M$, ignoring contractions in supplied arguments and the consumption of its initial binders. If this projected head computation did not reach a variable-headed spine, the full computation could not reach $I$ either. It therefore gives a finite head reduction of $M$ to a head normal form. ConsequentlyThe same head-trace argument shows that an unsolvable lambda term stays unsolvable under substitution and application. This also justifies the unsolvability conclusion in the preceding solution.

An easy lambda term must be equatable consistently with every closed lambda term. Choose the proposed equation $I=K$. Applying it to $I$ gives $I=\lambda y.I$. Applying that equation to an arbitrary closed $V$ gives $V=I$. In particular the two Church Booleans become equal; then applying them to arbitrary $A,B$ gives $A=B$. The extended equational theory is trivial, hence inconsistent in the required sense. Therefore $I$ is not easy.

Fix a closed $T$ and an arbitrary closed target $M$. If $S$ is an easy lambda term, the extension by $S=\lambda x.M$, with fresh $x$, is consistent. In that extensionThe theory obtained by adding only $ST=M$ is a subtheory of this consistent extension, so it is consistent too. Thus $ST$ is easy for every closed $T$. The printed unrestricted wording requires this qualification because easiness was defined only for closed terms: if $T$ is open, $ST$ need not be closed. With easiness extended to equations between open terms, the same argument works for arbitrary $T$.

If an easy closed $S$ were a solvable lambda term, some finite sequence of closed arguments would give $S{P}_1\cdots P_k{\equiv }_{\beta }I$. Repeated application of the result above would make this term easy. Easiness is invariant under beta equivalence, so $I$ would be easy, contrary to the preceding calculation. Hence every easy term is unsolvable.

Use Church numeralsExplicit lambda terms for the successor and zero test areDirect beta reduction gives $\mathsf{Succ}{c}_n{\equiv }_{\beta }{c}_{n+1}$, and the Church numeral zero test returns $\mathsf{T}$ exactly at zero. For the predecessor, use the Church pair operationsand setAfter $j$ iterations this pair holds $(c_j,c_{\max (j-1,0)})$: the initial pair gives the case $j=0$, and one step moves the old first coordinate into the second and increments the first. This proves the predecessor equation, including $\mathsf{Pred}{c}_0{\equiv }_{\beta }{c}_0$.

A total function is a lambda-definable function when a closed lambda term sends each tuple of numerals to the numeral of its value. Suppose $G,H$ represent total $g,h$, andFor lambda definition of primitive recursion by pair iteration, putOn numeral inputs, induction gives the pair $(c_j,c_{r(\mathbf{x},j)})$ after $j$ iterations. The base case is the equation for $G$, and the induction step is exactly the equation for $H$. Hence $R$ represents $r$, proving closure of total lambda-definable functions under primitive recursion.

For unbounded minimization, the careful closure statement is partial: if total $f(\mathbf{x},n)$ is lambda-definable, thenis a lambda-definable partial function, defined when a zero exists and otherwise undefined. It need not be total. With $F$ representing $f$, use a fixed-point combinator to defineEach test terminates because $f$ is total. Normal-order beta reduction chooses the return branch at the first zero and does not evaluate the discarded branch. If there is no zero, the required head computation passes through tests for all $n$, never exposing a numeral; standardization theorem for beta reduction rules out a hidden numeral reduct. For partial $f$, the usual mu operator is defined only if all earlier tests terminate and the successful test is zero. This stronger partial closure requires representatives that diverge on undefined inputs, or an explicit strict evaluator; the weaker condition of producing no numeral on undefined inputs alone must not be used as a test for convergence.

The zero function, successor, and projections have immediate numeral representations; function composition in recursion theory is implemented by substitution on total inputs. Thus every primitive recursive function is lambda-definable. The Kleene normal form theorem writes every partial recursive function as a total primitive-recursive decoding after a single minimization of a total primitive-recursive computation-history predicate. The search above consequently represents every partial recursive function, diverging when no successful history exists. Conversely a machine can effectively enumerate the beta reductions of a fixed representing lambda term on numeral inputs until it finds a Church numeral; distinct numerals cannot be beta-equivalent by the Church-Rosser theorem. It computes exactly the represented partial function. Therefore lambda-definable partial functions are precisely partial computable functions, and the total ones are precisely total computable functions.

This also gives the full partial minimization closure without assuming that an arbitrary weak representative diverges on every undefined input. Run its effective numeral evaluator successively at $n=0,1,2,\dots$; stop at the first zero, and run forever if an earlier evaluation fails to terminate or no zero is found. This is exactly the sequential-domain convention for the mu operator. The resulting partial computable function has a lambda representation by the construction just proved. Thus partial lambda-definable functions are closed under partial minimization; a minimized function belongs to the total family only when the required successful search exists for every input.

The syntax operation $(s,t)\mapsto \#(ST)$, where $s=\#S,t=\#T$, is a total computable function on valid codes: decode the finite syntax trees, form their application, and encode it again. Extend it arbitrarily on invalid codes if necessary. Similarly $n\mapsto \#(c_n)$ is total computable because the finite numeral syntax can be generated effectively from $n$. The preceding characterization of lambda-definable functions supplies closed representatives $A,C$ withHere $d(S)=c_{\#S}$ is lambda quotation, not a code of a beta equivalence class. In particular $C$ quotes the syntax of the numeral itself; it is not simply successor or an identity operation.

Choose $x$ fresh for $F$ and put $H=\lambda x.F(Ax(Cx))$, $Q=Hd(H)$. The preceding coding equations giveConsequentlyThis self-quoting fixed point is valid even if $F$ has free variables, since the effective Gödel numbering codes open lambda terms too. Freshness of $x$ prevents variable capture.

For the Church numeral system already used, the discriminatorhas $D{c}_{0}UV{\to }_{\beta }^{\ast }U$ and $D{c}_{1}UV{\to }_{\beta }^{\ast }V$ by the Church numeral zero test. More generally it chooses $V$ at every positive numeral. Only its values at zero and one are needed.

There is an argument-order defect in the printed flip context: the discriminator constructed above takes its numeral first. Fix $U\in \mathcal{U},V\in \mathcal{V}$ and useEquivalently, define $E=\lambda uvn.Dnuv$ and write the context as $\lambda x.EUV(Gx)$. This is an explicit permutation of the discriminator arguments, not an assumption that $DUV(Gx)$ has the required behavior.

Let $Q{\equiv }_{\beta }Fd(Q)$ be the self-quoting fixed point. There are exactly two cases. If $Gd(Q){\equiv }_{\beta }{c}_0$, then $Q{\equiv }_{\beta }U$, so closure under beta equivalence puts $Q$ in $\mathcal{U}$ and forces $Gd(Q){\equiv }_{\beta }{c}_1$. If $Gd(Q){\equiv }_{\beta }{c}_1$, then $Q{\equiv }_{\beta }V\in \mathcal{V}$, forcing $Gd(Q){\equiv }_{\beta }{c}_0$. Both contradict the distinct beta-normal Church numerals $c_0,c_1$. Hence no such total binary lambda classifier exists.

If beta equivalence were decidable, its decision algorithm would give a total computable function that outputs one exactly on codes of terms beta-equivalent to $I$, and zero on all other codes. Its numeral representation would be such a $G$, taking $\mathcal{U}$ to be the class of $I$ and $\mathcal{V}$ its complement. Both are nonempty: $K$ has a different beta-normal form from $I$. The contradiction proves beta equality is undecidable. It is nevertheless semidecidable, since finite conversion proofs can be effectively enumerated.

The Böhm tree $BT(M)$ is $\perp$ if $M$ is an unsolvable lambda term. Otherwise choose a head normal formIts root is labeled by the binder prefix and head variable, and its ordered children are $BT(M_1),\dots ,BT(M_m)$. Repeat recursively, possibly forever. Bound names are identified by alpha equivalence; the Church-Rosser theorem makes this tree independent of the selected head reduct. An address $\alpha$ is a finite sequence of child numbers; $M_{\alpha }$ denotes the corresponding argument term encountered after these head reductions.

A Böhm transformation is a finite composition of capture-avoiding substitutions and applications to chosen auxiliary terms. Here is a constructive Böhm-out lemma. Along the finite path to $\alpha$, choose $q$ at least the number of children of each preceding head node, and defineInitially replace all relevant free variables by $U_q$. At a head node with $n$ initial binders and $m$ children, supply its $n$ binders with $U_q$. Its head is now $U_q$ and its arguments are the substituted children $N_1,\dots ,N_m$. Apply $q-m$ extra copies of $U_q$ as padding and then $P_i^q$. Direct beta reduction givesRepeat with the next child number. The term reached at each stage is the selected original child with the accumulated substitutions for its ancestors' binders. Thus the finite composite $\pi$ satisfies $M\pi {\equiv }_{\beta }{M}_{\alpha }\sigma$ for a suitable substitution $\sigma$. The empty path uses the identity transformation. Tupling, rather than immediately replacing a head variable by a fixed projection, is important: the same variable can occur later where a different child must be selected.

For the Böhm separation theorem, two distinct closed normal forms for both beta reduction and eta conversion have finite Böhm trees with a genuine disagreement in a head label or argument structure. A Böhm transformation first extracts their common-prefix node. Projections at a differing head variable select different supplied Church Booleans; differing arities are handled by padding, with the exclusion of mere eta expansions ensuring a genuine disagreement. This yields a context separating the two normal forms. Distinct beta-normal forms that differ only by eta conversion are not covered by this separation statement.

The PDF prints a free $\alpha$ in both the definitions of $K$ and $\mathsf{T}$. Taken literally, this makes the last request impossible. To see why, suppose $M{K}_{\alpha }{\equiv }_{\beta }{K}_{\alpha }$, where $K_{\alpha }=\lambda xy.\alpha$, and choose a fresh $f$. By solvability and its stability under substitution, $Mf$ has a head normal form $\lambda x_1\cdots x_n.h{P}_1\cdots P_r$. If $h\ne f$, substituting either $K_{\alpha }$ or $S$ leaves the same variable-headed spine; it cannot be $K_{\alpha }$ in one case and $\mathsf{F}$ in the other. If $h=f$, obtaining $K_{\alpha }$ requires $r\le 2$ and $n+2-r=2$, hence $n=r$. Substituting $S=\lambda xyz.xz(yz)$ then leaves at least $n+3-r=3$ leading abstractions, whereas $\mathsf{F}$ has two. A variable-headed normal form cannot lose initial abstractions under beta reduction. The Church-Rosser theorem rules out the required equality.

For the intended closed first projection $K=\mathsf{T}=\lambda xy.x$ and $\mathsf{F}=\lambda xy.y=KI$, an explicit answer isIndeed $MK{\to }_{\beta }^{\ast }(KK)I{\to }_{\beta }K=\mathsf{T}$, whereas $MS{\to }_{\beta }^{\ast }(KK)I((KI)I){\to }_{\beta }KI=\mathsf{F}$. These computations solve the corrected closed-combinator version while identifying the obstruction in the literal printed one.

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$.