TCS: Programming in Lambda Calculus

Programming in Lambda Calculus

Reduction and Normal Forms

A $\beta$-redex is a subterm of the form $(\lambda x.M)N$. Contracting it replaces that subterm by $M[N/x]$, using capture-avoiding substitution

For example, $\mathbf S\mathbf K\mathbf K$ implements identity

$$\mathbf S\mathbf K\mathbf K \to_\beta^*\lambda z.\mathbf Kz(\mathbf Kz) \to_\beta^*\lambda z.z =\mathbf I$$

Three Termination Properties

• A term is in normal form when it contains no $\beta$-redex
• A term is normalizable when at least one reduction sequence reaches a normal form
• A term is strongly normalizable when every reduction sequence terminates

The distinction is visible in $(\lambda x.\mathbf I)\Omega$. Contracting the outer redex immediately produces $\mathbf I$, but repeatedly reducing the argument $\Omega$ gives an infinite sequence

This theorem explains why evaluating an unused argument first can lose termination. Programming-language call-by-name is related to normal order, but usually stops before reducing beneath an unapplied abstraction

Church-Rosser Theorem

Different choices of redex can produce different intermediate terms. Confluence says that these choices remain compatible

Confluence does not assert termination. The term $\Omega$ still has an infinite reduction sequence and no normal form

One-step reduction itself need not have the diamond property. Contracting a redex may duplicate an argument, after which reducing its two copies requires two steps rather than one

Parallel Reduction

The proof introduces $\Rightarrow$, which contracts several redexes together

$$\frac{}{x\Rightarrow x} \qquad \frac{M\Rightarrow M'}{\lambda x.M\Rightarrow\lambda x.M'}$$

$$\frac{M\Rightarrow M'\quad N\Rightarrow N'}{MN\Rightarrow M'N'} \qquad \frac{M\Rightarrow M'\quad N\Rightarrow N'} {(\lambda x.M)N\Rightarrow M'[N'/x]}$$

Two ingredients make the argument work

1. Substitution respects parallel reduction: if $M\Rightarrow M'$ and $N\Rightarrow N'$, then $M[N/x]\Rightarrow M'[N'/x]$
2. Parallel reduction has the diamond property, proved by structural induction and a case analysis of the application rules

The substitution lemma handles the case where one derivation contracts an outer redex while the other reduces its body or argument. The induction hypothesis provides compatible reducts of the subterms

Finally,

$$\to_\beta\ \subseteq\ \Rightarrow\ \subseteq\ \to_\beta^*$$

Thus the two relations have the same reflexive transitive closure, and the diamond property of parallel reduction yields confluence of $\beta$-reduction

As an application, $z$ and $\lambda u.zu$ are distinct $\beta$-normal forms when $u\ne z$. They are not $\beta$-equal, although the $\eta$ rule identifies them. Therefore $\eta$ is an additional equation

Encoding Booleans

A Boolean can be represented as a function choosing between two arguments

Then $\mathbf{if}\,\mathbf T\,M\,N\to_\beta^*M$ and $\mathbf{if}\,\mathbf F\,M\,N\to_\beta^*N$. The selector itself implements branching

Boolean operators can be defined without new syntax

$$\begin{aligned} \mathbf{not}&=\lambda b.b\mathbf F\mathbf T\\ \mathbf{and}&=\lambda ab.ab\mathbf F\\ \mathbf{or}&=\lambda ab.a\mathbf T b \end{aligned}$$

For instance, $\mathbf{and}\,\mathbf F\,N$ selects $\mathbf F$ without needing to evaluate $N$ under normal order

Church Numerals

The numeral for $n$ applies a function $n$ times to an initial value

The same term can serve different encodings: $\overline0$ and $\mathbf F$ are $\alpha$-equivalent. In the untyped calculus, the surrounding program determines the intended interpretation

Arithmetic by Iteration

$$\begin{aligned} \mathbf{succ}&=\lambda nfx.f(nfx)\\ \mathbf{add}&=\lambda mnfx.mf(nfx)\\ \mathbf{mult}&=\lambda mnfx.m(nf)x \end{aligned}$$

Successor adds one application of $f$. Addition composes $m$ applications with $n$ applications. Multiplication iterates the function $nf$, which itself performs $n$ applications, a total of $m$ times

For example,

$$\mathbf{add}\,\overline2\,\overline3 \to_\beta^*\lambda fx.f(f(f(f(fx)))) =\overline5$$

Exponentiation reverses the order in which the numerals are applied

$$\mathbf{pow}=\lambda mnfx.nmfx$$

On Church numerals, $\mathbf{pow}\,\overline m\,\overline n\to_\beta^*\overline{m^n}$, taking $m^0=1$, including the convention $0^0=1$ for this operation

Zero Test and Predecessor

A zero test starts with true and replaces it by false whenever the numeral performs an iteration

$$\mathbf{iszero}=\lambda n.n(\lambda u.\mathbf F)\mathbf T$$

For predecessor, keep a pair of consecutive values. Starting from $(0,0)$, repeatedly update $(a,b)$ to $(b,b+1)$. After $n$ iterations the first component is $\max(n-1,0)$

Using the pair operations developed in Lecture 3, this gives

$$\begin{aligned} \mathbf{step}&=\lambda p.\mathbf{pair}\,(\mathbf{snd}\,p) (\mathbf{succ}\,(\mathbf{snd}\,p))\\ \mathbf{pred}&=\lambda n.\mathbf{fst}\, (n\,\mathbf{step}\,(\mathbf{pair}\,\overline0\,\overline0)) \end{aligned}$$

Currying and Representation

Every abstraction binds one variable. A function of several arguments is represented by nested abstractions, so applying it to fewer arguments returns another function

$$\mathbf{add}\,\overline4 \to_\beta^*\lambda nfx.\overline4f(nfx)$$

This is partial application: the resulting term adds four to its next numeral argument

More generally, a term $M$ represents $f:\mathbb N^k\to\mathbb N$ when, for every input tuple,

$$M\overline{n_1}\cdots\overline{n_k} \to_\beta^*\overline{f(n_1,\ldots,n_k)}$$

Correctness therefore connects an operation on encoded values with ordinary mathematical computation