Some terms can reduce to terms that themselves are reducible. e.g. $(\lambda a.ac)(\lambda b.bd){\to }_{\beta }((\lambda b.bd)c){\to }_{b}cd$ e.g. $(\lambda a.ac)(\lambda b.bd){\to }_{\beta }^{\ast }cd$

Normal forms

When do we stop applying $\beta$-reductions?

1. Normal form: stop when there are no more redexes left to reduce.
2. Weak-head normal form: stop when all redexes are under an abstraction.

Some terms do not have a normal term such as $(\lambda q.qq)(\lambda q.qq)=Q$ hence $Q{\to }_{\beta }Q$. Such terms represent non-terminating computations.

Confluence

$\lambda$-terms can have multiple redexes, and therefore multiple $\beta$-reductions.

$\beta$-reductions are confluent. If $M{\to }_{\beta }^{\ast }{M}_1$ and $M{\to }_{\beta }^{\ast }{M}_2$ then there exists a term $M_3$ such that $M_1{\to }_{\beta }^{\ast }{M}_3$ and $M_2{\to }_{\beta }^{\ast }{M}_3$. (Church-Rosser Theorem)

Confluence implies unicity of normal forms: each $\lambda$-term has at most one normal term.

Reduction strategies

Reduction strategy can make a difference in the efficiency of computation, as the number of reduction steps may be different. We could do outermost vs. innermost or leftmost vs. rightmost.

Examples

Arithmetic

To represent numbers and arithmetic, we don’t need to introduce new digits or operators. Natural numbers can be represented with the Church Numerals:

\overline 0 &= \lambda xy.y \\ \overline 1 &= \lambda xy.xy \\ \overline 2 &= \lambda xy.x(xy) \\ \overline 3 &= \lambda xy.x(x(xy)) \\ \ldots \end{aligned}$$ We use $\overline n$ to denote the Church Numeral representing the number $n$. We can define the successor function, the function that takes a number $\overline n$ and returns $\overline {n+1}$. $$S = \lambda xyz. y(xyz)$$ We can define addition: $$\textsf{ADD} = \lambda xyab. (xa) (yab)$$ ### Boolean Boolean values and operators can also be encoded in pure Lambda Calculus. $$\begin{aligned}\textsf{FALSE} &= \lambda xy. y \\ \textsf{TRUE} &= \lambda xy. x\end{aligned}$$ We can define the NOT operation as follows: $$\textsf{NOT} = \lambda x.x \, \textsf{FALSE} \, \textsf{TRUE}$$ ### Recursion (Haskell) Curry's fixed point combinator is defined as follows: $$Y = \lambda f. (\lambda x. f(x \, x)) \lambda x. f(x \, x)))$$ This combinator is the basis of recursion in Lambda Calculus. > [!example] Example of application of $\textsf{Y}$. > > $$\begin{aligned} > YM &= \lambda f. (\lambda x. f(x \, x)) \lambda x. f(x \, x))) (M) \\ > &\rightarrow_\beta {\color{orange}(\lambda x. M(x \, x)) \lambda x. M(x \, x)))} \\ > &\rightarrow_\beta M({\color{orange}(\lambda x. M(x \, x)) \lambda x. M(x \, x)))}) \\ > &= M(YM) \\ > &= M(M(YM)) \\ > &= \ldots > \end{aligned}$$