Basics of the Untyped Lambda Calculus

1Introduction

This lecture explains the syntax and beta-reduction of the untyped lambda calculus. It reviews free variables and alpha-equivalence before beta-reduction because substitution must avoid variable capture. No typing judgment is introduced here.

21. Syntax and association conventions

Let the set of variables be countably infinite. Lambda terms $t$t are defined inductively by

The term $\lambda x.t$\lambda x.t is a lambda abstraction that binds $x$x, and $ts$t\;s is an application. Application associates to the left, and the body of an abstraction extends as far right as possible. Thus $tuv=\left(tu\right)v$t\;u\;v=(t\;u)\;v and $\lambda x.tu=\lambda x.\left(tu\right)$\lambda x.t\;u=\lambda x.(t\;u).

32. Free variables and alpha-equivalence

The set $\mathrm{F}\mathrm{V}\left(t\right)$\mathrm{FV}(t) of free variables is defined by

Terms that differ only by a consistent renaming of bound variables are alpha-equivalent. For example, $\lambda x.x{=}_{\alpha }\lambda z.z$\lambda x.x =_\alpha \lambda z.z. A binder cannot, however, be renamed to $z$z when $z$z occurs free in its body.

43. Capture-avoiding substitution

The term $t[x:=s]$t[x:=s] replaces every free occurrence of $x$x in $t$t with $s$s. If $x\notin \mathrm{F}\mathrm{V}\left(t\right)$x\notin\mathrm{FV}(t), then $t[x:=s]=t$t[x:=s]=t. Its variable and application cases follow the term structure. The abstraction case is

where the last case chooses a fresh variable $z$z that differs from $x$x and does not occur anywhere in either $t$t or $s$s. For example, directly producing $\lambda y.y$\lambda y.y from $(\lambda y.x)[x:=y]$(\lambda y.x)[x:=y] would capture the free $y$y of the substituted term. Alpha-renaming first gives $(\lambda y.x)[x:=y]{=}_{\alpha }(\lambda z.x)[x:=y]=\lambda z.y$(\lambda y.x)[x:=y]=_\alpha(\lambda z.x)[x:=y]=\lambda z.y.

54. Beta-reduction and normal forms

A subterm of the form $(\lambda x.t)s$(\lambda x.t)\;s is a beta-redex. Capture-avoiding substitution contracts it as follows:

A beta-redex at any position in a term may be contracted in one step. A term containing no beta-redex is a beta-normal form.

In contrast, the only beta-redex of $\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$\Omega=(\lambda x.x\;x)(\lambda x.x\;x) is the whole term, and contracting it returns $\mathrm{\Omega }{\to }_{\beta }\mathrm{\Omega }$\Omega\to_\beta\Omega. Hence no reduction sequence reaches a beta-normal form. The untyped lambda calculus does not guarantee termination in general.

65. Evaluation strategies

Beta-reduction does not prescribe an order for selecting redexes. Normal order selects the leftmost outermost redex, whereas applicative order selects the leftmost innermost redex; the two strategies can have different termination behavior. Consider

Normal order contracts the outer redex first and reaches $a$a. Applicative order repeatedly reduces $\mathrm{\Omega }$\Omega and does not terminate. This is a difference in strategy termination, not a difference in the beta-reduction rule. If a term has a beta-normal form, normal-order reduction reaches it.

76. Distinguishing eta-conversion

When $x\notin \mathrm{F}\mathrm{V}\left(f\right)$x\notin\mathrm{FV}(f), the eta-conversion $\lambda x.fx{=}_{\eta }f$\lambda x.f\;x=_\eta f expresses extensional identification of functions. It is distinct from beta-reduction, which performs function application.

8Summary

Computation in the untyped lambda calculus is beta-reduction by capture-avoiding substitution, considered modulo alpha-equivalence. The existence of a normal form must be distinguished from termination under a particular evaluation strategy.