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

Definition 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 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 5(Definition).

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

$$(\lambda x.M)N\equiv 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=Z\mathcal{M}\\ 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 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 7(Standard combinators).

Define standard combinators

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

Theorem 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

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

such that $F(\mathbf{Y}F)=\mathbf{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.$□

Example 9(Example).

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

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

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

Note that taking $G\equiv \mathbf{YS}$ also works.

Example 10(Example).

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

Let $G\equiv \mathbf{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 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 12(Church numerals).

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

Theorem 13(Arithmetic on Church numerals).

Define

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

Then,

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

Lemma 14(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}$$ □

Proof.

test test

$$\begin{array}{rl}{\mathbf{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 14 $(1)$,

$$\begin{array}{rl}{\mathbf{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 14 $(2)$,

$$\begin{array}{rl}{\mathbf{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 })$.□

---

Booleans and conditionals

Definition 15(Definition).

$\text{true}\equiv \mathbf{K}$, $\text{false}\equiv {\mathbf{K}}_{\ast }$, where $\mathbf{K}$ and ${\mathbf{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 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.

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

Definition 17(Barendregt Numerals).

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

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

Lemma 18(Lemma).

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

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

Proof.

Take

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

Definition 19(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\lceil n_1\rceil \lceil n_2\rceil \dots \lceil n_p\rceil =\lceil \phi (n_1,n_2,\dots ,n_p)\rceil$$

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