Past exam of the mathematics course of the University of Cambridge / 2007 / iii / Paper 87 (Lambda--calculus)

A lambda term is built recursively as a variable $x$, an application $MN$, or a lambda abstraction $\lambda x.M$. Application associates to the left and abstraction binds occurrences of its variable. We identify consistent renamings of bound variables by alpha equivalence. A beta reduction contracts $(\lambda x.M)N$ to the capture-avoiding substitution $M[x:=N]$, at any subterm. Write ${\to }_{\beta }^{\ast }$ for finitely many such steps, including none. Beta equivalence is the reflexive, symmetric, transitive closure of reduction, so it is represented by a finite zigzag of forward and backward steps.

To prove the Church-Rosser theorem, introduce parallel beta reduction $\Rightarrow$ by the four rulesBy structural induction every term parallel-reduces to itself. Each ordinary step is a parallel step. Conversely, each parallel step can be performed by an ordinary finite sequence: reduce the displayed subterms recursively, and in the fourth rule contract the root last. Hence ${\Rightarrow }^{\ast }$ and ${\to }_{\beta }^{\ast }$ are the same relation.

The substitution lemma isProve it by induction on the parallel-reduction derivation for $M$. The variable case separates $M=x$ from other variables; application and abstraction follow from their inductive hypotheses. For abstraction, rename its binder fresh for $x,N,N^{\prime }$ before substituting. For a contracted redex, choose its binder $y$ distinct from $x$ and fresh for $N,N^{\prime }$. The substitution identity $P[y:=Q][x:=N]=P[x:=N][y:=Q[x:=N]]$ follows by structural induction with fresh binders; the variable cases use $y\notin FV(N)$, and application and abstraction preserve the identity. Apply the hypotheses to the body and argument, then the parallel contraction rule and this identity. This proves the lemma for every derivation, including simultaneous contractions inside a redex.

Define the complete development of a lambda term byOnly a root redex already present in the source application is contracted by this clause; a newly created root redex need not be contracted.

We claim that $M\Rightarrow N$ implies $N\Rightarrow M^{\bullet }$. Induct on the derivation. The variable and abstraction cases are immediate. In the ordinary application rule, use the inductive developments of both components. If its original function is an abstraction, also contract the resulting root redex by the parallel contraction rule; otherwise just use the application rule, even if the reduct has acquired a new root redex. In the contraction rule, the reduct has form $P^{\prime }[x:=Q^{\prime }]$, and the substitution lemma with $P^{\prime }\Rightarrow P^{\bullet }$, $Q^{\prime }\Rightarrow Q^{\bullet }$ gives $P^{\prime }[x:=Q^{\prime }]\Rightarrow P^{\bullet }[x:=Q^{\bullet }]$. This establishes the claim.

Consequently, any two parallel reducts $N,P$ of $M$ each parallel-reduce to $M^{\bullet }$. Thus parallel reduction has the one-step diamond property. Its finite transitive closure is confluent: fill a finite grid of elementary diamonds to join two finite reduction paths from the same term. Since its closure equals ordinary finite beta reduction,A finite conversion zigzag now also has a common reduct, by induction along it. If the next zigzag step points forward from a term already having a common reduct, join its two outgoing paths by confluence; if it points backward, compose the new forward path to that common reduct. The reverse implication is immediate because two paths to a common reduct form a conversion zigzag. This proves

A beta-normal form contains no beta-redex, so its only finite reduct is itself. If two normal forms are beta-equivalent, their common reduct must equal both. Hence a term has at most one beta-normal form up to alpha equivalence. The qualification about bound-variable names is essential.

For an example without normal form, take the Omega combinatorIts only redex is the root, and contracting it reproduces $\Omega$. Every finite reduct is therefore $\Omega$, which is not a beta-normal form. By the theorem it cannot even be beta-equivalent to any normal form.

A combinatory logic term over free variables $X$ is formed from variables in $X$, the constants $S,K,I$, and application, with no abstraction binder. We may regard $I$ as primitive, or as the abbreviation $SKK$. Application associates to the left. Weak combinatory reduction contractsin any application context. Weak equivalence is the equivalence relation generated by these reductions. There is no additional rule identifying terms merely because they behave alike after application to a fresh argument.

Define bracket abstraction on combinatory terms by the following ordered clauses:They cover every term: after excluding the variable case and the case with no free $x$, the term must be an application. Induction gives $FV([x]T)=FV(T)\setminus \{x\}$; no other variable is introduced or removed. For every argument $A$, the same induction gives $([x]T)A{\to }^{\ast }T[x:=A]$: the three cases use respectively the $I$, $K$, and $S$ reductions.

The required translation isIt has exactly the same set of free variables as the original lambda term, by the bracket-abstraction identity.

To compare the two reductions, expand the constants into lambda terms:and expand variables and applications homomorphically. Every weak combinatory contraction becomes a finite sequence of beta reductions, so weakly equivalent terms have beta-equivalent lambda expansions. We also haveFor $T=x$, this is the expansion of $I$. For $x\notin FV(T)$, the expansion of $KT$ beta-reduces to $\lambda x.T^{\lambda }$, after choosing the binder fresh. For an application, expanding $S([x]P)([x]Q)$ givesby induction and beta contraction. Thus, induction on the lambda syntax gives $(M^{\ast }{)}^{\lambda }{\equiv }_{\beta }M$. Combining these facts proves

The reverse implication fails for this intensional translation. The beta-equivalent lambda terms $M=\lambda x.x$ and $N=\lambda x.((\lambda y.y)x)$ translate respectively toBoth are weak normal forms: $I$ has no argument, $KI$ has too few arguments to contract, and the outer $S$ has only two arguments. They are syntactically distinct. By the assumed Church–Rosser property of weak combinatory reduction, two distinct weak normal forms cannot be weakly equivalent. The same argument works with $I=SKK$, because both fully expanded terms remain distinct weak normal forms. Hence beta-equivalent lambda terms need not have weakly equivalent combinatory translations.

Here a pointed complete partial order is a partially ordered set $D$ with a least element ${\perp }_D$ in which every nonempty directed set has a least upper bound. Directed means that every pair of its elements has an upper bound within that set. A Scott continuous map is monotone and preserves these directed suprema. It is not required to preserve the least element; restricting to strict maps would change the categorical claim. If completeness is instead formulated only for increasing countable chains, the same arguments below work with those chains.

Order the function space of complete partial orders $[D\to E]$ pointwise: $f\le g$ means $f(x)\le g(x)$ for every $x$. Its least element is the constant function with value ${\perp }_E$. For a directed family $\mathcal{F}$ of continuous maps, define $h(x)={\sup }_{f\in \mathcal{F}}f(x)$. This is well-defined and is its pointwise least upper bound. It is monotone. For any directed $A\subseteq D$,The interchange is valid because the combined family $\{f(a):f\in \mathcal{F},a\in A\}$ is directed, and either iterated supremum is its least upper bound. Thus $h$ is a Scott continuous map, proving that $[D\to E]$ is a pointed complete partial order.

Finite products carry the product order, componentwise suprema and least element $({\perp }_D,{\perp }_E)$. The one-element order is a terminal object. For the exponential, use the function space with evaluation $\mathrm{ev}(f,x)=f(x)$. To check joint continuity, take a directed family of pairs $(f_i,x_i)$. ThenIndeed, directedness supplies a $k$ above the pairs indexed by both $i$ and $j$, giving $f_i(x_j)\le f_k(x_k)$. Thus the diagonal values are cofinal in the double family, and evaluation preserves its supremum.

For a continuous $h:A\times D\to E$, its currying is $\Lambda h:A\to [D\to E]$, $(\Lambda h)(a)(d)=h(a,d)$. Each section is continuous because $d\mapsto (a,d)$ is; pointwise directed suprema in the $a$ coordinate show that $\Lambda h$ is continuous. Conversely a continuous $g:A\to [D\to E]$ gives the continuous map $\mathrm{ev}\circ (g\times {\mathrm{id}}_D)$. The two constructions are inverse, because they agree on every pair $(a,d)$. This gives the natural bijectionwith the required evaluation map. Together with the terminal object and products, it proves cartesian closure of pointed complete partial orders with non-strict continuous maps.

Choose mutually inverse maps $i:D^D\to D$ and $j:D\to D^D$. This is an extensional reflexive object in the Cartesian closed category. Define its application morphismFor endomorphisms $f,g:D\to D$, application in the underlying set $\mathrm{End}(D)$ is $f\cdot g=\mathrm{app}\circ ⟨f,g⟩$.

It is useful to define term interpretation uniformly over any context object $A$. An environment assigns each free variable $x$ a morphism $\rho (x):A\to D$. Variables are interpreted by their assigned maps, and application is interpreted by $\mathrm{app}$ and pairing. For lambda abstraction, lift the old environment along ${\pi }_A:A\times D\to A$, interpret the new variable by ${\pi }_D$, and let $h:A\times D\to D$ interpret the body. Then setTaking $A=D$ gives interpretations in the requested set of endomorphisms. Other context objects are needed in the recursive definition to handle bound variables correctly.

The beta reduction rule follows from $ji={\mathrm{id}}_{D^D}$ and the evaluation identity for currying. Applying the interpreted abstraction to a map $g:A\to D$ givesInduction on terms identifies this with interpretation of the capture-avoiding substitution of the argument for $x$.

For eta conversion, suppose $x$ is not free in $M$ and write $f:A\to D$ for the interpretation of $M$. The body $Mx$ on $A\times D$ is the uncurried form of $jf$. HenceThus beta-eta-equivalent terms have equal interpretations in $\mathrm{End}(D)$. The full isomorphism, rather than just a retract of the function object, provides the inverse law used in the eta step.

An embedding-projection pair consists of continuous maps $e:D\to E$, $p:E\to D$ with $pe={\mathrm{id}}_D$ and $ep\le {\mathrm{id}}_E$ pointwise. Thus $e$ is an order embedding and $ep$ approximates an element of the larger domain from below. Such maps are automatically strict: applying the inequality at ${\perp }_E$ gives $e({\perp }_D)\le ep({\perp }_E)\le {\perp }_E$, and applying $p$ then gives $p({\perp }_E)={\perp }_D$.

Suppose $({\varphi }_{n-1},{\psi }_{n-1})$ is such a pair. Composition with fixed continuous maps is continuous on the pointwise function space of complete partial orders, so both proposed lifted maps are continuous. Their composite on the smaller function space isWriting $q={\varphi }_{n-1}{\psi }_{n-1}\le \mathrm{id}$, the other composite is ${\varphi }_n{\psi }_n(g)=qgq\le g$: for every $x$, $q(g(qx))\le g(qx)\le g(x)$ by monotonicity. Thus the recursion produces embedding-projection pairs at every stage.

Here is an explicit inverse-limit solution of the reflexive domain equation. Formordered coordinatewise. The bottom sequence is coherent by strictness. A directed family has coordinatewise suprema, and continuity of each ${\psi }_n$ preserves the coherence condition. Thus $D_{\infty }$ is a pointed complete partial order.

Write ${\varphi }_{m,n}:D_m\to D_n$ for the composite embeddings when $m\le n$, and ${\psi }_{m,n}:D_n\to D_m$ for the corresponding composite projections, taking both as identities if $m=n$. Define $P_n:D_{\infty }\to D_n$ by $P_n(x)=x_n$, and define $E_n:D_n\to D_{\infty }$ byThe pair identities make this sequence coherent, and its coordinates are continuous. They also give $P_n{E}_n={\mathrm{id}}_{D_n}$ and $E_n{P}_n\le {\mathrm{id}}_{D_{\infty }}$. Put $Q_n=E_n{P}_n$. Since $E_n=E_{n+1}{\varphi }_n$ and $P_n={\psi }_n{P}_{n+1}$,At coordinate $m$, $Q_{n}x$ equals $x_m$ once $n\ge m$, soThis exhibits the required embedding-projection pair for every finite stage.

To prove the function-space isomorphism, observe that $x_{n+1}\in D_{n+1}$ is itself a continuous function $f_n:D_n\to D_n$. Coherence saysConversely such a coherent function family determines an element of $D_{\infty }$, with initial coordinate $x_0={\psi }_0(f_0)$. Define its action on the limit byThe maps inside this supremum increase: substituting coherence expresses the $n$th one as $E_{n+1}{q}_n{f}_{n+1}{q}_n{P}_{n+1}$ with $q_n={\varphi }_n{\psi }_n\le \mathrm{id}$, which is below the next map. The supremum is continuous by the function-space result in Question 3.

In the other direction, for a continuous $F:D_{\infty }\to D_{\infty }$, define $f_n=P_{n}F{E}_n$. These satisfy the same coherence equation. Hence define $\mathcal{B}(F)\in D_{\infty }$ byFor a coherent family, restricting ${\sup }_n{E}_n{f}_n{P}_n$ back to stage $m$ gives $f_m$: every term with $n\ge m$ restricts exactly to ${\psi }_{m,n}{f}_n{\varphi }_{m,n}=f_m$, and the earlier terms are below it. Thus $\mathcal{B}\mathcal{A}$ is the identity.

Conversely,For the last equality, $Q_n\uparrow \mathrm{id}$ and continuity give, at every $x$, ${\sup }_n{Q}_{n}F(Q_{n}x)={\sup }_{n,m}{Q}_{n}F(Q_{m}x)=F(x)$; the diagonal is cofinal because the double family increases in both indices. Both $\mathcal{A}$ and $\mathcal{B}$ are continuous, by coordinatewise evaluation, continuous composition and directed suprema. Thereforeas complete partial orders with continuous maps, not merely as sets. This supplies the extensional reflexive object needed for a beta-eta model, together with all the stated finite-stage pairs.

Write products of endomorphisms as composition, with the rightmost map applied first. Because $1$ is terminal, the only hom-sets that can contain multiple arrows are $\mathrm{Hom}(1,D)$ and $\mathrm{End}(D)$. If the latter contained only the identity, any point $p:1\to D$ would have $p!={\mathrm{id}}_D$, where $!:D\to 1$. Then any other point $q$ would satisfy $q=p!q=p$. Thus the category would be a preorder. The hypothesis therefore implies $|\mathrm{End}(D)|>1$.

If the product object $D\times D$ were $1$, its universal property applied to arrows from $D$ would give $\mathrm{End}(D{)}^2\cong \mathrm{Hom}(D,1)$, a singleton, which is impossible. Since there are only two objects, $D\times D=D$. Similarly, if $D^D=1$, the exponential adjunction at $1$ would giveagain impossible. Hence $D\times D=D^D=D$ as chosen objects.

Let $M=\mathrm{End}(D)$, let $\pi ,{\pi }^{\prime }$ be the product projections, and let $\epsilon :D^D\times D\to D$ be evaluation, all now endomorphisms. Pairing is $⟨-,-⟩$, and for $x:D\times D\to D$ write $x^{\ast }$ for its currying. The product identities and the two inverse exponential identities giveThis is the structure of a cartesian closed monoid.

For the converse, start only from the monoid and these identities. The first three make pairing a bijection from $M^2$ to $M$, inverse to $z\mapsto (\pi z,{\pi }^{\prime }z)$. In particularas follows by applying both projections and using uniqueness. Define $U(y)=\epsilon ⟨y\pi ,{\pi }^{\prime }⟩$. The last two identities say that $U$ and $(-{)}^{\ast }$ are inverse bijections. These facts also derive, rather than assume, the naturality lawIndeed $U(x^{\ast }z)=\epsilon ⟨x^{\ast }z\pi ,{\pi }^{\prime }⟩=U(x^{\ast })⟨z\pi ,{\pi }^{\prime }⟩=x⟨z\pi ,{\pi }^{\prime }⟩$; applying the inverse bijection proves the law.

Put $e=({\pi }^{\prime }{)}^{\ast }$. The law applied to $x={\pi }^{\prime }$ gives, for every $z\in M$,Taking $z=e$ proves $e^2=e$. This stronger absorption identity is what makes the split object terminal.

Assume first that $M$ is nontrivial; the degenerate case is handled below. Construct the required category using the two idempotents $d=1_M$ and $e$, as a two-object part of the Karoubi envelope. Call their objects $D$ and $1$. A morphism from the object with idempotent $a$ to the object with idempotent $b$ is an element $f\in M$ satisfying $bfa=f$. Composition is monoid multiplication, and the identity on each object is its idempotent. These laws are well-defined and associative. Its hom-sets are concretelyFor example, $ef=e$ for every $f$, so the condition for $D\to 1$ forces $f=e$. Thus $1$ is terminal, and the original monoid appears unchanged at $D$.

Set $D\times D=D$ with projections $\pi ,{\pi }^{\prime }$ and the given pairing. The product property works for arrows from either object: for global arrows $x,y$ satisfying $xe=x$, $ye=y$, pairing also satisfies $⟨x,y⟩e=⟨x,y⟩$. The original projection identities give existence and uniqueness. Products with $1$ are the other object, with its identity and the unique terminal arrow as projections; $1\times 1=1$.

For the exponential set $D^D=D$ with evaluation $\epsilon$. For a parameter object $D$, the given $(-{)}^{\ast }$ and $U$ already establish the universal property. We must additionally verify it for parameter object $1$. An arrow $f:1\times D=D\to D$ is an arbitrary element of $M$. Define its transpose byNaturality gives $\kappa (f)z=\kappa (f)$ for every $z$, because $f{\pi }^{\prime }⟨z\pi ,{\pi }^{\prime }⟩=f{\pi }^{\prime }$. In particular $\kappa (f)e=\kappa (f)$, so it really is an arrow $1\to D$.

Its uncurrying is $\epsilon ⟨\kappa (f),1_M⟩=f$. To see this, start from $U(\kappa (f))=f{\pi }^{\prime }$ and compose with $⟨e,1_M⟩$. Pairing naturality, ${\pi }^{\prime }⟨e,1_M⟩=1_M$, and the absorption property of $\kappa (f)$ give precisely the claimed equality. Conversely, if $g:1\to D$ satisfies $ge=g$, then $gz=gez=ge=g$ for every $z$. ThereforeThus transpose and uncurrying are inverse for the terminal parameter object too. This verifies the full exponential property, rather than only its endomorphism instance.

The remaining exponentials are $D^1=D$, $1^D=1$, and $1^1=1$, by the unit product law and terminality. Hence the constructed two-object category is cartesian closed and $\mathrm{End}(D)=M$.

For nontrivial $M$, the constructed $D$ is nonterminal because it has more than one endomorphism, and $e\ne 1_M$ by the absorption identity. This is the case corresponding to the forward non-preorder hypothesis.

If $M$ has one element, all the algebraic identities still hold, but splitting $e=1_M$ alone would make the original object terminal. To satisfy the literal converse's requirement of a nonterminal object, handle this case separately: take the two-object poset category $D<1$. Products are meets, $D^D=1$, $1^D=1$, $D^1=D$, and $1^1=1$, which verify the exponential adjunction on this two-element order. It is cartesian closed, $D$ is nonterminal, and its one-element endomorphism monoid is $M$. It is a preorder, so it does not recover the forward non-preorder setting or the self-exponential equality. Thus the converse's stated endomorphism realization works also in the degenerate case, while the stronger non-preorder reconstruction uses nontrivial $M$.