Lambda terms, beta reduction, and the partial functions they represent

The lambda terms are the finite expressions built from variables by the rules $x,(MN),(\lambda x\mathrm{.}M)\mathrm{.}$ Because they are finite strings over a fixed finite syntax, they admit effective coding.

A beta reduction is one application of the rewrite rule $(\lambda x\mathrm{.}M)N{\to }_{\beta }M[x:=N],$ where $M[x:=N]$ denotes capture-avoiding substitution: before substituting, bound variables of $M$ are alpha-renamed when necessary so that no free variable of $N$ becomes bound. Terms that differ only by such a consistent renaming of bound variables are identified up to alpha-equivalence. The relation ${\to }_{\beta }^{\ast }$ denotes the reflexive transitive closure of beta reduction modulo alpha-equivalence.

For each $n\in \mathbb{N}$, let $\bar{n}$ be the Church numeral for $n$. A lambda term $F$ represents a partial function $f:{\mathbb{N}}^k\rightharpoonup \mathbb{N}$ when:

• for every $(n_1,\dots ,n_k)$ in the domain of $f$, $F\overline{n_1}\cdots \overline{n_k}{\to }_{\beta }^{\ast }\overline{f(n_1,\dots ,n_k)},$
• and for every input tuple outside the domain, the term $F\overline{n_1}\cdots \overline{n_k}$ never reaches a Church numeral by beta reduction.

Such a function is called lambda-definable.

• The represented object is a partial function on natural numbers, not the term itself.

• The chosen convention is extensional: different lambda terms may represent the same partial function.