Intro to Lambda Calculus

Preliminaries

$\lambda$ Calculus is a formal system for expressing computation in terms of function application and abstraction.

Info

Vanilla $\lambda$ calculus is untyped (or type-free), that is, any function can be applied to any term. It is Turing complete (being allowed to consider expressions like $FF$ allows us to simulate recursion), but you can easily write meaningless or non-terminating terms, like $(\lambda x.xx)(\lambda x.xx)$.

Application and abstraction are the two basic operations of the $\lambda$ Calculus.

The expression $FA$ denotes $F$ being considered as an operator being applied to $A$ being considered as data.

The other basic operation is abstraction: If $M\equiv M[x]$ is an expression containing $x$, then $\lambda x.M[x]$ denotes the function $x\mapsto M[x]$.

Notation

$M[x]$ denotes an expression $M$ containing variable $x$.

Abstraction binds the variables of the local scope.

• It is a notational convention that the bound variables that occur in an expression are always different form the free ones.
• Expressions that differ only in the names of bound variables are identical.

Iterated application uses association to the left

$$F{M}_1\dots M_n\text{ denotes }(\dots (F{M}_1)\dots M_n).$$

Dually, iterated abstraction used association to the right:

$$\lambda x_1\dots x_n.f(x_1,\dots ,x_n)\text{ denotes }\lambda x_1.(\lambda x_2.(\dots (\lambda x_n.f(x_1,\dots ,x_n))\dots )).$$

For $n$ arguments, we have (recall currying):

$$(\lambda x_1\dots x_n.f(x_1,\dots ,x_n))x_1\dots x_n=f(x_1,\dots ,x_n).$$

Using vector notation, we have

$$(\lambda \mathbf{x}.f(\mathbf{x}))\mathbf{x}=f(\mathbf{x}).$$

However, considering our notational convention from above, it would be more appropriate to write

$$(\lambda \mathbf{x}.f(\mathbf{x}))\mathbf{N}=f(\mathbf{N}).$$

---

The formal definitions

Definition 66.1($\lambda$ terms).

The set of $\lambda$-terms, denoted by $\Lambda$, is built up from an infinite set of variables $V=\{v,v^{\prime },v^{\prime \prime },\dots \}$ using application and abstraction:

$$\begin{array}{rl}x\in V& ⟹x\in \Lambda ,\\ M,N\in \Lambda & ⟹(MN)\in \Lambda ,\\ M\in \Lambda ,x\in V& ⟹\lambda x.M\in \Lambda .\end{array}$$

It is a convention that lower case letters denote variables and upper case letters denote $\lambda$-terms. $M\equiv N$ denotes that $M$ and $N$ are the same term or can be obtained from each other by renaming bound variables. We also associate iterated application to the left and iterated abstraction to the right.

Definition 66.2(free variables).

The set of free variables of $M$, denoted by $FV(M)$, is defined inductively as follows:

$$\begin{array}{rl}FV(x)& \equiv \{x\},\\ FV(MN)& \equiv FV(M)\cup FV(N),\\ FV(\lambda x.M)& \equiv FV(M)\setminus \{x\}.\end{array}$$

A variable in $M$ is said to be bound if it is not free.

8db839

Definition 66.3(Combinator).

$M$ is a closed $\lambda$-term (or combinator) if $FV(M)=\varnothing$. The set of closed $\lambda$-terms is denoted by ${\Lambda }^{\circ }$.

Variable convention: If $M_1,\dots ,M_n$ occur in a certain mathematical context, then in these terms all bound variables are chosen to be different from the free variables.

Definition 66.4(Definition).

The result of substituting $N$ for the free occurrences of $x$ in $M$, denoted by $M[x:=N]$, is defined as follows:

$$\begin{array}{rl}x[x:=N]& \equiv N;\\ y[x:=N]& \equiv y,\text{if }x\not\equiv y;\\ (M_1{M}_2)[x:=N]& \equiv (M_1[x:=N])(M_2[x:=N])\\ (\lambda y.M)[x:=N]& \equiv \{\begin{array}{ll}\lambda y.(M[x:=N])& y\not\equiv x,\\ (\lambda y.M)& y\equiv x.\end{array}\end{array}$$

Note that in the fourth clause of the above definition, it is not needed to say “Provided that $y\notin FV(N)$“. By the variable convention, this is the case: $y$ is a bound variable in $(\lambda y.M)$, and hence cannot be a free variable in $N$.

Now, we can introduce the $\lambda$ calculus as a formal theory:

Definition 66.5(Definition).

The principal axiom of the $\lambda$-calculus is

$$(\lambda x.M)N=M[x:=N]$$

for all $M,N\in \Lambda$.

There are also the logical axioms:

$$\begin{array}{rl}M& =M;\\ M=N& ⟹N=M;\\ M=N,N=L& ⟹M=L;\end{array}$$

and compatibility rules:

$$\begin{array}{rl}M=M^{\prime }& ⟹MZ=M^{\prime }Z;\\ M=M^{\prime }& ⟹ZM=ZM\\ M=M^{\prime }& ⟹\lambda x.M=\lambda x.M^{\prime }.\end{array}$$

If $M=N$ is provable in the $\lambda$-calculus, then we write $\mathbf{\lambda }⊢M=N$.

Thanks to the compatibility rules, one can replace subterms by equal terms in any term context. For example, $(\lambda y.yy)x=xx$, so $\mathbf{\lambda }⊢\lambda x.x((\lambda y.yy)x)x=\lambda x.x(xx)x$.

The following lemma is clear from the principal axiom:

Lemma 66.6(Lemma).

$$\mathbf{\lambda }⊢(\lambda x_1\dots x_{n}M)X_1\dots X_n=M[x_1:=X_1]\dots [x_n:=X_n].$$

---

Fixed point theorem

Definition 66.7(Standard combinators).

Define standard combinators

$$\begin{array}{rl}\text{I}& \equiv \lambda x.x;\\ \text{K}& \equiv \lambda xy.x;\\ {\text{K}}_{\ast }& \equiv \lambda xy.y;\\ \text{S}& \equiv \lambda xyz.xz(yz).\end{array}$$

9c0469

Theorem 66.8(Fixed point theorem).

For all $F\in \Lambda$, there exists $X\in \Lambda$ such that $FX=X$. More precisely, for all $F\in \Lambda$, there exists a fixed point combinator

$$\text{Y}\equiv \lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$

such that $F(\text{Y}F)=\text{Y}F$.

Proof.

Define $W\equiv \lambda x.F(xx)$ and $X\equiv WW$. Then, $X\equiv WW=(\lambda x.F(xx))W=F(WW)=FX.$□

d18faf

Example 66.9(Example).

Show that there exists $G$ such that for all $X$, $GX=\text{S}GX$.

Let $G\equiv \text{Y}(\lambda gx.\text{S}gx)$. Then, $G$ is a fixed point of $\lambda gx.\text{S}gx$, and

$$\begin{array}{rl}& G=(\lambda gx.\text{S}gx)G\\ ⟹& G=\lambda x.\text{S}Gx\\ ⟹& Gx=\text{S}Gx\\ ⟹& GX=\text{S}GX\forall X\in \Lambda .\end{array}$$

Note that taking $G\equiv \text{Y}\text{S}$ also works.

Example 66.10(Example).

Show that there exists $G$ such that for all $X$, $GX=GG$.

Let $G\equiv \text{Y}(\lambda gx.gg)$. Then,

$$\begin{array}{rl}G& =(\lambda gx.gg)G\\ & =(\lambda x.GG),\end{array}$$

so $GX=GG$ for all $X$.

Alternatively, for a solution that does not use the fixed point combinator, let $F\equiv \lambda fx.ff$ and $G\equiv FF$:

$$\begin{array}{rl}G& =FF=\lambda x.FF=\lambda x.G\\ GG& =(\lambda x.G)G=G=(\lambda x.G)X=GX.\end{array}$$

More alternative solutions can be obtained by taking the $f$s in $F$ in powers of $2$:

$F\equiv \lambda fx.ffff$
$G\equiv FF$
$G=\lambda x.FFFF=\lambda x.GG$
$GX=(\lambda x.GG)X=GG$

$F\equiv \lambda fx.ffffffff$
$G\equiv FF$
$G=\lambda x.FFFFFFFF=\lambda x.GGGG$
$GG=GGGG$
$G=\lambda x.GG$

Note that all the proofs converge when we obtain $G=\lambda x.GG$. In general, we have:

$F\equiv \lambda fx.f^{2^k}$
$G\equiv FF$
$G=\lambda x.F^{2^k}=\lambda x.G^{2^{k-1}}$
$GG=G^{2^{k-1}}$
$G=\lambda x.GG$

---

Church numerals

Definition 66.11(Notation for repeated application).

$F^n(M)$ with $F\in \Lambda$ and $n\in \mathbb{N}$ is defined inductively as follows:

$$\begin{array}{rl}{F}^0(M)& =M;\\ F^{n+1}(M)& =F(F^n(M)).\end{array}$$

Definition 66.12(Church numerals).

The Church numerals $c_0,c_1,\dots ,$ are defined by $c_n\equiv \lambda fx.f^n(x)$.

Lemma 66.13(Lemma).

1. $(c_{n}f{)}^{m}x=f^{nm}x$

2. $(c_n{)}^{m}f=c_{n^m}f$, for $m>0$.

Proof.

Proof by induction. Note that for $m=0$, $x=x$, and for $m=1$, $(c_{n}f)x=f^{n}x$. Assume that $(1)$ holds for $m=k$, that is, $(c_{n}f{)}^{k}x=f^{nk}x$. Then, we have

$$\begin{array}{rl}(c_{n}f{)}^{k+1}x& =c_{n}f(f^{nk}x)\\ & =f^n(f^{nk}x)\\ & =f^{n(k+1)}x.\end{array}$$

Similarly, note that $(2)$ holds for $m=1$. Assume that it holds for $m=k$. Then,

$$\begin{array}{rl}(c_n{)}^{k+1}f& =c_n(c_{n^k}f)\\ & =\lambda x.(c_{n^k}f{)}^{n}x\\ & =\lambda x.f^{n^{k+1}}x\\ & =c_{n^{k+1}}f.\end{array}$$ □

ec2774

Theorem 66.14(Arithmetic on Church numerals).

Define

$$\begin{array}{rl}{\text{A}}_{+}& \equiv \lambda c_a{c}_{b}fx.c_{a}f(c_{b}fx);\\ {\text{A}}_{\ast }& \equiv \lambda c_a{c}_{b}f.c_a(c_{b}f);\\ {\text{A}}_{\exp }& \equiv \lambda c_a{c}_b.c_b{c}_a.\end{array}$$

Then,

$$\begin{array}{rl}{\text{A}}_{+}{c}_a{c}_b& =c_{a+b};\\ {\text{A}}_{\ast }{c}_a{c}_b& =c_{ab};\\ {\text{A}}_{\exp }{c}_a{c}_b& =c_{a^b},m\ne 0.\end{array}$$

Proof.

$$\begin{array}{rl}{\text{A}}_{+}{c}_a{c}_b& =\lambda fx.c_{a}f(c_{b}fx)\\ & =\lambda fx.(\lambda x.f^a(x))(f^b(x))\\ & =\lambda fx.f^a(f^b(x))\\ & =\lambda fx.f^{a+b}(x)\\ & =c_{a+b}\end{array}$$

Using Lemma 13 $(1)$,

$$\begin{array}{rl}{\text{A}}_{\ast }{c}_a{c}_b& =\lambda f.c_a(c_{b}f)\\ & =\lambda fx.(c_{b}f{)}^{a}x\\ & =\lambda fx.f^{ab}x\\ & =c_{ab}.\end{array}$$

Using Lemma 13 $(2)$,

$$\begin{array}{rl}{\text{A}}_{\exp }{c}_a{c}_b& =c_b{c}_a\\ & =\lambda x.c_a^{b}x\\ & =\lambda x.c_{a^b}x\\ & =\lambda x.(\lambda fy.f^{a^b}y)x\\ & =\lambda xy.x^{a^b}y\\ & =c_{a^b}.\end{array}$$

Note that in general, $M=\lambda x.Mx$ if $M=\lambda y.M^{\prime }[y]$ and $x\notin FV(M^{\prime })$.□

---

Lambda definability and recursive functions

Booleans and conditionals

Definition 66.15(Definition).

$\text{true}\equiv \text{K}$, $\text{false}\equiv {\text{K}}_{\ast }$, where $\text{K}$ and ${\text{K}}_{\ast }$ are the combinators defined here.

Note that if $B$ is a boolean, then

$$\text{if }B\text{ then }P\text{ else }Q$$

is equivalent to the $\lambda$-term

$$BPQ.$$

Definition 66.16(Definition).

For $M,N\in \Lambda$, define

$$[M,N]\equiv \lambda z.zMN.$$

Then, $[M,N]\text{true}=M$, and $[M,N]\text{false}=N$. $[M,N]$ can serve as an ordered pair.

Multiple fixed point theorem

Theorem 66.17(Multiple fixed point theorem).

Let $F_1,\dots ,F_n$ be $\lambda$-terms. Then, we can find $X_1,\dots ,X_n$ such that

$$\begin{array}{lcl}{X}_1& =& F_1{X}_1\dots X_n,\\ & ⋮& \\ X_n& =& F_n{X}_1\dots X_n.\end{array}$$

For $n=1$, this is the ordinary fixed point theorem.

Proof.

Consider$n=2$. By the ordinary fixed point theorem, we can find $X$ such that

$$X=[F_1(X\text{true})(X\text{false}),F_2(X\text{true})(X\text{false})].$$

Now define $X_1=X\text{true}$ and $X_2=X\text{false}$. The result follows. This can be generalized to arbitrary $n$.□

Barendregt numerals

We can use the pairing construction for an alternative representation of natural numbers.

Definition 66.18(Barendregt Numerals).

For each $n\in \mathbb{N}$, the numeral $┌n┐$ is defined inductively as follows:

$$\begin{array}{rl}┌0┐& \equiv \text{I},\\ ┌n+1┐& \equiv [\text{false},┌n┐].\end{array}$$

Lemma 66.19(Lemma).

The exist combinators ${\text{S}}^{+},{\text{P}}^{-}$, and $\text{Zero}$ such that

$$\begin{array}{rl}{\text{S}}^{+}\lceil n\rceil & =\lceil n+1\rceil ,\\ {\text{P}}^{-}\lceil n+1\rceil & =\lceil n\rceil ,\\ \text{Zero}\lceil 0\rceil & =\text{true}\\ \text{Zero}[n+1]& =\text{false}.\end{array}$$

Proof.

Take

$$\begin{array}{rl}{\text{S}}^{+}& \equiv \lambda x.[\text{false},x]\\ {\text{P}}^{-}& \equiv \lambda x.x\text{false}\\ \text{Zero}& \equiv \lambda x.x\text{true}.\end{array}$$ □

bd0c3a

Equivalence of lambda definable and recursive functions

Definition 66.20(Lambda definability).

A numeric function is a map $\phi :{\mathbb{N}}^p\to \mathbb{N}$ for some $p$. In this case, $\phi$ is called $p$-ary.
A numeric $p$-ary function $\phi$ is called $\lambda$-definable if for some combinator $F$,

$$F┌n_1┐┌n_2┐\dots ┌n_p┐=┌\phi (n_1,n_2,\dots ,n_p)┐$$

for all $n_1,\dots ,n_p\in \mathbb{N}$, in which case, $\phi$ is said to be $\lambda$-defined by $F$.

Definition 66.21(Initial functions).

The initial functions are the numeric functions $U_i^n$, $S^{+},Z$ defined by

$$\begin{array}{rl}{U}_i^n(x_1,x_2,\cdots ,x_n)& =x_i,(1\le i\le n)\\ S^{+}(n)& =n+1\\ Z(n)& =0.\end{array}$$

Notation

Let $P(n)$ be a numeric relation. $\mu m[P(m)]$ denotes the least number $m$ such that $P(m)$ holds if there is such a number; otherwise it is undefined.

We will now characterize the $\lambda$-definable functions.

Definition 66.22(Recursive functions).

The class $\mathcal{R}$ of recursive functions is the smallest class of numeric functions that contains all initial functions and is

1. closed under composition: for all $\phi$ defined by

$$\phi (\vec{n})=\chi ({\psi }_1(\vec{n}),{\psi }_2(\vec{n}),\cdots ,{\psi }_m(\vec{n}))$$

with $\chi ,{\psi }_1,\dots ,{\psi }_m\in \mathcal{R}$, one has $\phi \in \mathcal{R}$;
2. closed under primitive recursion: for all $\phi$ defined by

$$\begin{array}{rl}\phi (0,\vec{n})& =\chi (\vec{n})\\ \phi (k+1,\vec{n})& =\psi (\phi (k,\vec{n}),k,\vec{n})\end{array}$$

with $\chi ,\psi \in \mathcal{R}$, one has $\phi \in \mathcal{R}$;
3. closed under minimalization: for all $\phi$ defined by

$$\phi (\vec{n})=\mu m[\chi (\vec{n},m)=0],$$

with $\chi \in \mathcal{R}$ such that

$$\forall \vec{n}\exists m\chi (\vec{n},m)=0$$

one has $\phi \in \mathcal{R}$.

Our claim is that all recursive functions are $\lambda$-definable.

Lemma 66.23(Lemma).

The initial functions are $\lambda$-definable.

Proof.

$$\begin{array}{rl}{\text{U}}_i^n& \equiv \lambda x_1{x}_2\cdots x_n.x_i,\\ {\text{S}}^{+}& \equiv \lambda x.[\text{false},x],\\ \text{Z}& \equiv \lambda x.┌0┐.\end{array}$$

Note that ${\text{S}}^{+}$ is the same successor defined as part of the barendregt numerals interface.□

Lemma 66.24(Lemma).

The $\lambda$-definable functions are closed under composition.

97646e

$$\begin{array}{rl}\text{Add}(0,y)& =y\\ \text{Add}(x+1,y)& ={\text{S}}^{+}\text{Add}(x,y).\end{array}$$

Therefore we want a term $\text{Add}$ satisfying

$$\text{Add}xy=(\text{Zero}x)y({\text{S}}^{+}(\text{Add}({\text{P}}^{-}x)y)).$$

This equation can be solved using the fixed point combinator:

$$\begin{array}{rl}\text{Add}& =\text{Y}(\lambda axy.(\text{Zero}x)y({\text{S}}^{+}(a({\text{P}}^{-}x)y))).\end{array}$$

The general case follows.

Lemma 66.25(Lemma).

The $\lambda$-definable functions are closed under primitive recursion.

Proof.

Let$\phi$ be defined by

$$\begin{array}{rl}\phi (0,\vec{n})& =\chi (\vec{n})\\ \phi (k+1,\vec{n})& =\psi (\phi (k,\vec{n}),k,\vec{n})\end{array}$$

where $\psi ,\chi$ are $\lambda$-defined by $G,H$ respectively. Now, we require $F$ such that

$$\begin{array}{r}Fx\vec{y}=(\text{Zero}x)(H\vec{y})(G(F({\text{P}}^{-}x)\vec{y})x\vec{y})\end{array}$$

Using the fixed point combinator, we have

$$\begin{array}{r}F=\text{Y}(\lambda fx\vec{y}.(\text{Zero}x)(H\vec{y})(G(f({\text{P}}^{-}x)\vec{y})x\vec{y})).\end{array}$$ □

Lemma 66.26(Lemma).

The $\lambda$-definable functions are closed under minimalization.

Proof.

Let$\phi$ be defined by

$$\phi (\vec{n})=\mu m[\chi (\vec{n},m)=0]$$

where $\chi$ is $\lambda$-defined by $H$. Again by the fixed point theorem, there is a term $G$ such that

$$\begin{array}{rl}G\vec{x}y& =(\text{Zero}H\vec{x}y)y(G\vec{x}({\text{S}}^{+}y)).\end{array}$$

Set $F\equiv \lambda \vec{x}.G\vec{x}┌0┐$.□

Hence, we have the following theorem.

Theorem 66.27(Theorem).

All recursive functions are $\lambda$-definable.

13a977

What if we replaced Barendregt with Church numerals?

If we define analogs ${\text{S}}_c^{+}$, ${\text{P}}_c^{-}$, ${\text{Zero}}_c$ of ${\text{S}}^{+}$, ${\text{P}}^{-}$, $\text{Zero}$ for Church numerals, like so,

$$\begin{array}{rl}{\text{S}}_c^{+}& \equiv \lambda nfx.f(nfx),\\ {\text{P}}_c^{-}& \equiv \lambda nfx.{\text{K}}_{\ast }(nfx),\\ {\text{Zero}}_c& \equiv \lambda n.n(\text{K}\text{false})\text{true},\end{array}$$

then this section can be developed using Church numerals, and Theorem 27 will still hold. An alternative Proof uses translators between numerals $┌n┐$ and $c_n$: define $T,T^{-1}$ as follows:

$$\begin{array}{rl}T& \equiv \lambda x.x{\text{S}}^{+}┌0┐,\\ T^{-1}& \equiv \lambda x.(\text{Zero}x)c_0{\text{S}}_c^{+}(T^{-1}({\text{P}}^{-}x)).\end{array}$$

Then, $T{c}_n=┌n┐$, and $T^{-1}┌n┐=c_n$. Let $\phi$ be a recursive function (of arity $k$), $\lambda$-defined by $F$ with respect to the numerals $┌n┐$. Then,

$$F_c\equiv \lambda \vec{x}.T^{-1}(F(T{x}_1)(T{x}_2)\dots (T{x}_k))$$

represents $\phi$ with respect to the church numerals.

---