Lambda Calculus II

Recap

• Term $\Lambda$:

$$\begin{array}{rlr}& (var)& x\\ & (app)& st\\ & (abs)& \lambda x.s\end{array}$$

• $\alpha$ convertible: $\lambda x.x{\equiv }_{\alpha }\lambda y.y$
• $\beta$ convertible: substitution
• $\lambda$ theory
• Fixed-point conbinator: $Y$ combinator, …

Programming in $\lambda$ calculus

There are no loops, no classes, no objects — only functions. And yet, from this minimalism, entire worlds of computation unfold.

$\beta$ reduction

The key idea is substitution implement the computation.

Example

$$\begin{array}{c}\begin{array}{rl}\mathbf{skk}& \equiv (\lambda xyz.(xz)(yz))\mathbf{kk}\\ & {\to }_{\beta }\lambda yz.(\mathbf{k}z)(yz)\mathbf{k}\\ & {\to }_{\beta }\lambda z.(\mathbf{k}z)(\mathbf{k}z)\\ & \equiv \lambda z.((\lambda xy.x)z)(\mathbf{k}z)\\ & {\to }_{\beta }\lambda z.(\lambda y.z)(\mathbf{k}z)\\ & {\to }_{\beta }\lambda z.z\\ & \equiv \mathbf{i}.\end{array}\end{array}$$

Normal Form

• $s$ is in normal form if there is no term $t$ s.t. $s{\to }_{\beta }t$
• $s$ has a normal form or is normalizable if there is a term $t$ in normal form s.t. $s{\twoheadrightarrow }_{\beta }t$
• $s$ is strongly normalizable if there does not exist an infinite sequence s.t. $s{\to }_{\beta }{t}_1{\to }_{\beta }{t}_2{\to }_{\beta }\dots$

Example

• $\lambda x.x$ is in normal form.
• $(\lambda x.x)(\lambda x.x)$ has a normal form and is strongly normalizable.
• $\mathbf{\Omega }=(\lambda x.xx)(\lambda x.xx)$ is not normalizable, because when trying reduce it, it reduces to itself!
• $\mathbf{f\Omega i}$ is normalizable but not strongly normalizable:
  • if we reduce $\mathbf{f}$ first, it reduces into $\mathbf{i}$, which is in normal form
  • but as mentioned above, if we try to reduce $\mathbf{\Omega }$, it reduces to itself.

Theorem

Leftmost reduction always finds the normal form if it exists.

• The proof is complicated

Church-Rosser Property

Is it possible that a term has two different normal form?

Definition

• Relation $\to$ has diamond property if $s\to u,s\to v$ implies $u\to t,v\to t$ for some $t$
• Relation $\to$ is Church-Rosser if $\twoheadrightarrow$ has diamond property
• Relation $\to$ has unique normal form if $s\twoheadrightarrow t_1,s\twoheadrightarrow t_2$ implies $t_1\equiv t_2$ if $t_1,t_2$ are in normal form.

Lemma 1

If $\to$ is CR, then it has unique normal form property.

Proof is easy. if there are two normal forms $u,v$ of $s$, then there must exists a term $t$, $u\to t,v\to t$, which is impossible because a term in normal form cannot reduce anymore.

Lemma 2

If $\to$ is diamond, then $\twoheadrightarrow$ is diamond.

Can be proved by a diagram:

Obviously, any two terms reduced by the original one can reduce into the same term, which is equivalent to the statement.

Lemma 3

If $\to$ is CR and $=$ is its refl, sym and trans closure, then $s=t$ iff $s\twoheadrightarrow u,t\twoheadrightarrow u$ for some $u$.

$s\twoheadrightarrow u,t\twoheadrightarrow u\Rightarrow s=t$ is trivial.

For the other direction, we illustrate it with a diagram:

$s=t$ implies that $s$ and $t$ are linked by some kind of route in the diagram, and because $\twoheadrightarrow$ has the diamond property, we can always find a $u$, $s\twoheadrightarrow u,t\twoheadrightarrow u$

Corollary

If $\to$ is CR, $s,t$ are normal forms for $\to$ and $s=t$, then $s\equiv t$.

Now if $\beta$ reduction is CR, then we can say $\eta$ rule does not follow from $\beta$ :

Terms $x$ and $\lambda y.xy$ are not $\beta$ convertible as they are normal forms but not $\alpha$ convertible.

Church-Rosser for $\beta$ reduction

Theorem

A fundamental result is that $\beta$ reduction has CR property.

$$\begin{array}{rl}\text{(refl)}& \frac{}{s{\to }_{\parallel }s}\\ \text{(abs)}& \frac{s{\to }_{\parallel }{s}^{\prime }}{\lambda x.s{\to }_{\parallel }\lambda x.s^{\prime }}\\ \text{(∥-app)}& \frac{s{\to }_{\parallel }{s}^{\prime }t{\to }_{\parallel }{t}^{\prime }}{st{\to }_{\parallel }{s}^{\prime }{t}^{\prime }}\\ \text{(∥-β)}& \frac{s{\to }_{\parallel }{s}^{\prime }t{\to }_{\parallel }{t}^{\prime }}{(\lambda x.s)t{\to }_{\parallel }{s}^{\prime }[t^{\prime }/x]}\end{array}$$

• ${\twoheadrightarrow }_{\beta }$ is the transitive closure of ${\to }_{\parallel }$

Then we prove ${\to }_{\parallel }$ has diamond property, which means that if $s{\to }_{\parallel }u,s{\to }_{\parallel }v$, then $u{\to }_{\parallel }t,v{\to }_{\parallel }t$ for some $t$.

Proof

Case 1. $s{\to }_{\parallel }u$ is by (refl), then $u\equiv s$. Take $t\equiv v$, then $u{\to }_{\parallel }t,v{\to }_{\parallel }t$

Case 2. $s{\to }_{\parallel }u$ and $s{\to }_{\parallel }v$ are by (app).

Case 3. $s{\to }_{\parallel }u$ is by (app) and $s{\to }_{\parallel }v$ is by ($\beta$).

Case 4. $s{\to }_{\parallel }u,s{\to }_{\parallel }v$ both use (abs).

Case 5. Both use ($\beta$).

Here I omit the detailed proof…

$\lambda$ calc as a Programming Language

Boolean

true and false:

$$\begin{array}{rl}\mathbf{t}& \equiv \lambda xy.x\\ \mathbf{f}& \equiv \lambda xy.y\end{array}$$

Then define $\mathbf{and}=\lambda ab.ab\mathbf{f}$

We can simply verify it.

$$\begin{array}{r}\mathbf{and}\mathbf{tt}\equiv \mathbf{ttf}{\to }_{\beta }\mathbf{t}\\ \mathbf{and}\mathbf{tf}\equiv \mathbf{tff}{\to }_{\beta }\mathbf{f}\\ \mathbf{and}\mathbf{ft}\equiv \mathbf{ftf}{\to }_{\beta }\mathbf{f}\\ \mathbf{and}\mathbf{ff}\equiv \mathbf{fff}{\to }_{\beta }\mathbf{f}\end{array}$$

Then define $\mathbf{ite}=\lambda x.x$ (if then else)

$$\mathbf{ite}\mathbf{t}st=\mathbf{t}st=s$$ $$\mathbf{ite}\mathbf{f}st=\mathbf{f}st=t$$

Interestingly, $\mathbf{ite}$ can always be omited.

Natual Numbers

$$\overline{n}=\lambda fx.f^{n}x$$ $$\begin{array}{rl}\overline{0}& \equiv \lambda fx.x\equiv \mathbf{f}\\ \overline{1}& \equiv \lambda fx.fx\\ \overline{2}& \equiv \lambda fx.f(fx)\end{array}$$

define successor $\mathbf{succ}=\lambda nfx.f(nfx)$

$$\begin{array}{rl}\mathbf{succ}\overline{n}& \equiv \lambda nfx.f(nfx)\overline{n}\\ & {\to }_{\beta }\lambda fx.f(\overline{n}fx)\\ & \equiv \overline{n+1}\end{array}$$

Then we can define add and multiply.

$$\mathbf{add}\equiv \lambda nmfx.nf(mfx)$$ $$\mathbf{mult}\equiv \lambda nmf.n(mf)$$ $$\mathbf{add}\overline{n}\overline{m}\equiv \lambda fx.\overline{n}f(\overline{m}fx){\to }_{\beta }\lambda fx.f^{n+m}x\equiv \overline{n+m}$$ $$\begin{array}{rl}\mathbf{mult}\overline{n}\overline{m}& \equiv \lambda f.\overline{n}(\overline{m}f)\\ & {\to }_{\beta }\lambda f.\overline{n}(\lambda x.f^{m}x)\\ & {\to }_{\beta }\lambda fx.(\lambda x.f^{m}x{)}^{n}x\\ & {\to }_{\beta }\lambda fx.f^{mn}x\\ & \equiv \overline{mn}\end{array}$$

Currying

In $\lambda$ calc, a function with multiple arguments can take fewer arguments, transforming into another function, while in traditional calc can not.

In the example of $\mathbf{mult}$, we use the idea of currying.

General Function

A term $s$ represents a function $f$ iff

$$s\overline{n_1}\overline{n_2}\dots \overline{n_k}=\overline{f(n_1,\dots ,n_k)}$$

We can define $\mathbf{iszero}=\lambda nxy.n(\lambda z.y)x$:

$$\begin{array}{rl}\mathbf{iszero}\overline{0}& \equiv (\lambda nxy.n(\lambda z.y)x)\overline{0}\\ & {\to }_{\beta }\lambda xy.\overline{0}(\lambda z.y)x\\ & {\twoheadrightarrow }_{\beta }\lambda xy.x\\ & \equiv \mathbf{t}\end{array}$$ $$\begin{array}{rl}\mathbf{iszero}\overline{n}& \equiv (\lambda nxy.n(\lambda z.y)x)\overline{n}\\ & {\to }_{\beta }\lambda xy.\overline{n}(\lambda z.y)x\\ & {\to }_{\beta }\lambda xy.(\lambda z.y{)}^{n}x\\ & {\to }_{\beta }\lambda xy.y\\ & \equiv \mathbf{f}\end{array}$$

The difference is that $\overline{0}$ ignore the input of $\lambda z.y$, avoiding $x$ turn into $y$.

A more complicated example:

$$pred(n)=\{\begin{array}{rlrl}& 0& & ,\text{if n = 0}\\ & n-1& & ,\text{otherwise}\end{array}$$