TCS: Lambda Calculus

Lambda Calculus

Terms and Binding

The untyped $\lambda$-calculus builds programs from variables, function abstraction and function application. Functions are themselves values, so a function can receive another function, return one, or be applied to itself

These are inductive rules: $\Lambda$ contains exactly the terms obtainable by finitely many applications of the constructors. This gives a structural induction principle: prove a property for variables, and show that abstraction and application preserve it

The corresponding inference rules can be written with the premises above a horizontal line

$$\frac{}{x\in\Lambda}\;(x\in\mathcal V) \qquad \frac{M\in\Lambda}{\lambda x.M\in\Lambda} \qquad \frac{M\in\Lambda\quad N\in\Lambda}{MN\in\Lambda}$$

A rule with no premises is an axiom. When additional conditions appear beside a rule, they must also hold before the rule can be applied

Subterms

The immediate subterms of $MN$ are $M$ and $N$, and the immediate subterm of $\lambda x.M$ is $M$. All subterms are obtained recursively, including the whole term itself

Abbreviations

The fully parenthesized syntax makes the structure explicit, but we usually shorten terms using the following conventions

For example, combining these conventions gives

$$z\lambda xy.xz \equiv z(\lambda x.(\lambda y.(xz)))$$

Parentheses remain necessary in $(\lambda x.M)N$: removing them would put $N$ inside the abstraction’s body and change the term

Free Variables

Binding is a property of an occurrence. In $(\lambda x.x)y$, the occurrence of $x$ in the body is bound, while $y$ is free. In $x(\lambda x.x)$, the first $x$ is free and the last $x$ is bound

Some useful closed terms are

$$\begin{aligned} \mathbf I&=\lambda x.x\\ \mathbf K&=\lambda xy.x\\ \mathbf S&=\lambda xyz.xz(yz) \end{aligned}$$

Alpha-Conversion and Substitution

Renaming Bound Variables

The choice of a bound variable’s name carries no computational information

$$\lambda x.x\equiv_\alpha\lambda u.u$$

An $\alpha$-conversion must preserve binding. For example, $\lambda x.y$ cannot be renamed to $\lambda y.y$: the free $y$ would become bound

We normally identify terms up to $\alpha$-equivalence and rename bound variables to fresh names whenever necessary

Capture-Avoiding Substitution

Write $M[N/x]$ for the term obtained by replacing the free occurrences of $x$ in $M$ with $N$

For example, consider substituting $y$ for $x$ in $\lambda y.xy$. The binder would capture the inserted $y$, so rename it first

$$(\lambda y.xy)[y/x] \equiv_\alpha(\lambda z.xz)[y/x] =\lambda z.yz$$

The result is not $\lambda y.yy$. Its free occurrence of $y$ must remain free

Beta-Conversion and Equational Reasoning

Applying an abstraction evaluates its body with the argument substituted for its parameter

For example, assuming $z$ is fresh for $P$, the constant function discards its second argument

$$(\lambda xz.x)PQ =_\beta(\lambda z.P)Q =_\beta P$$

An equation is established by a finite derivation from the equality rules and the $\beta$ rule. The notation $\lambda\beta\vdash M=N$ records that the equation is derivable in this theory

Equality and computation serve different purposes. Equality allows a step in either direction, whereas an evaluation step contracts an application of an abstraction. We will make this directed relation precise in Lecture 2

The Eta Rule

The term $\lambda x.Mx$ passes its argument directly to $M$. When $x$ does not occur freely in $M$, the $\eta$ rule identifies these terms

$$\lambda x.Mx=_\eta M \qquad x\notin\operatorname{FV}(M)$$

The side condition matters: $\lambda x.xx$ is not an $\eta$-expansion of $x$. Adding this rule gives the theory $\lambda\beta\eta$, expressing an extensional view of functions

Fixed Points and Self-Application

A fixed point of a term $F$ is a term $U$ satisfying $FU=_\beta U$. In the untyped calculus, every term has such a fixed point

To verify the equation, put $W=\lambda x.F(xx)$. Both sides reduce to the same term

$$\begin{aligned} \mathbf YF&\to_\beta WW\to_\beta F(WW)\\ F(\mathbf YF)&\to_\beta F(WW) \end{aligned}$$

The useful idea is to turn a request for self-reference into self-application. If $U$ should satisfy $U=FU$, define $W$ so that $Wx=F(xx)$ and then apply $W$ to itself

Turing’s combinator offers a related construction

$$\begin{aligned} A&=\lambda xy.y(xxy)\\ \mathbf\Theta&=AA \end{aligned}$$

It satisfies the directed unfolding $\mathbf\Theta F\to_\beta^*F(\mathbf\Theta F)$. For $\mathbf Y$, the fixed-point equation above is stated as $\beta$-equality; its displayed derivation uses a common reduct

Self-application also explains why evaluation may fail to terminate

$$\Omega=(\lambda x.xx)(\lambda x.xx) \to_\beta\Omega$$

The syntax allows recursion and divergence without introducing a separate recursion operator. We will use fixed points to construct recursive programs in Lecture 3