Lambda Calculus

Key objectives:
- Define syntax and reduction rules of $\lambda$-calculus.
- Define $\lambda$-definable functions.
- Show that primitive recursive functions are $\lambda$-definable.
- Show that $\mu$-recursive (partial recursive) functions are $\lambda$-definable.
- Show that $\lambda$-definable functions are Turing-computable.
- Conclusion: $\lambda$-definable = partial recursive = Turing-computable.

Syntax of Lambda Terms

Alphabet: Variables $x, y, z, \dots$, abstraction $\lambda$, application (juxtaposition), parentheses.
Syntax (BNF): $$ M, N ::= x \mid \lambda x.M \mid M N $$
- $x$: variable
- $\lambda x.M$: abstraction (function with parameter $x$ and body $M$)
- $M N$: application of $M$ to $N$ (left-associative)
Free and bound variables: In $\lambda x.M$, $x$ is bound in $M$. Occurrences not bound are free.
$\alpha$-conversion: Renaming bound variables: $\lambda x.M \equiv_\alpha \lambda y.(M[x := y])$ if $y$ is fresh (capture-avoiding).

$\beta$-reduction (one step): $$ (\lambda x.M)N \rightarrow_\beta M[x := N] $$ where $M[x := N]$ is the substitution of $N$ for free occurrences of $x$ in $M$ (with $\alpha$-conversion to avoid capture).
- The subterm $(\lambda x.M)N$ is called a redex.
Context closure: Reduction can occur in any context $C[\cdot]$. $$ C[(\lambda x.M)N] \rightarrow_\beta C[M[x := N]] $$
Many-step $\beta$-reduction: $\rightarrow_\beta^*$ denotes zero, one, or more steps.
Normal form: A $\lambda$-term that contains no redex (cannot be reduced further).

Encoding natural numbers: $$ \underline{0} := \lambda f x. x $$ $$ \underline{1} := \lambda f x. f x $$ $$ \underline{2} := \lambda f x. f (f x) $$ $$ \underline{n} := \lambda f x. f^n x $$
Intuition: A numeral $\underline{n}$ applies its first argument $f$ to its second argument $x$ exactly $n$ times.

Total function $f: \mathbb{N}^n \to \mathbb{N}$: A $\lambda$-term $M_f$ represents $f$ if for all $m_1, \dots, m_n$: $$ M_f \, \underline{m_1} \, \underline{m_2} \dots \underline{m_n} \rightarrow_\beta^* \underline{f(m_1, \dots, m_n)} $$ $f$ is $\lambda$-definable if such $M_f$ exists.
Partial function $f: \mathbb{N}^n \rightharpoonup \mathbb{N}$: A $\lambda$-term $M_f$ represents $f$ if:
- If $f(m_1, \dots, m_n) \downarrow$ (defined), then $M_f \, \underline{m_1} \dots \underline{m_n} \rightarrow_\beta^* \underline{f(\dots)}$.
- If $f(m_1, \dots, m_n) \uparrow$ (undefined), then $M_f \, \underline{m_1} \dots \underline{m_n}$ has no normal form (non-terminating reduction).

Successor: $$ M_{\text{succ}} := \lambda n f x. f (n f x) $$
Addition: $$ M_+ := \lambda m n f x. m f (n f x) $$
Multiplication: $$ M_\times := \lambda m n f x. m (n f) x $$
Exponentiation: $$ M_E := \lambda m n f x. n m f x \quad (\text{or } \lambda m n. n m) $$
Constant zero: $$ M_{c_0} := \lambda m. \underline{0} $$
Projection $\pi_i^n$: $$ M_{\pi_i^n} := \lambda x_1 \dots x_n. x_i $$

True and False: $$ \text{true} := \lambda x y. x $$ $$ \text{false} := \lambda x y. y $$
If-then-else: $$ \text{if } P \text{ then } Q \text{ else } R := P Q R $$
- If $P = \text{true}$, then $\text{true} \, Q \, R \rightarrow_\beta^* Q$.
- If $P = \text{false}$, then $\text{false} \, Q \, R \rightarrow_\beta^* R$.
Zero test: $$ \text{zero?} := \lambda n. n (\lambda y. \text{false}) \, \text{true} $$
- $\text{zero?} \, \underline{0} \rightarrow_\beta^* \text{true}$
- $\text{zero?} \, \underline{n+1} \rightarrow_\beta^* \text{false}$

Theorem: Every primitive recursive function is $\lambda$-definable.
Proof sketch (primitive recursion case): Let $h = \text{pr}(f; g)$: $$ h(\vec{x}, 0) = f(\vec{x}) $$ $$ h(\vec{x}, y+1) = g(\vec{x}, h(\vec{x}, y), y) $$ Suppose $M_f, M_g$ represent $f, g$. Define: $$ \text{Init} := (\underline{0}, M_f \vec{x}) $$ $$ \text{Step} := \lambda p. (M_{\text{succ}}(\rho_1 p), \; M_g \vec{x} \, (\rho_2 p) \, (\rho_1 p)) $$ Then the representation of $h$ is: $$ M_h := \lambda \vec{x} y. \rho_2 (y \, \text{Step} \, \text{Init}) $$ This iterates $\text{Step}$ $y$ times, building successive pairs $(y, h(\vec{x}, y))$ and finally returns the second component.

Kleene's Normal Form Theorem (reminder): For every partial recursive function $h: \mathbb{N}^n \rightharpoonup \mathbb{N}$, there exist primitive recursive functions $g: \mathbb{N}^{n+1} \to \mathbb{N}$ and $f: \mathbb{N} \to \mathbb{N}$ such that: $$ h(\vec{x}) = f(\mu y. [g(\vec{x}, y) = 0]) $$ where $\mu y$ is the least $y$ with $g(\vec{x}, y) = 0$, if it exists.
Theorem: Every partial recursive function is $\lambda$-definable.
Proof idea: Let $M_g, M_f$ represent $g, f$. Define a term $W$ that searches for the least $y$ satisfying $g(\vec{x}, y) = 0$: $$ W := \lambda y. \text{if } (\text{zero?}(M_g \vec{x} y)) \text{ then } (\lambda w. M_f y) \text{ else } (\lambda w. w (M_{\text{succ}} y) w) $$ Then use the $Y$-combinator (or a self-application) to perform unbounded search: $$ M_h := \lambda \vec{x}. W \, \underline{0} \, W $$ The term $W \, \underline{0} \, W$ iterates until a zero is found, then returns $M_f$ of that index.

Theorem: Every $\lambda$-definable function is Turing-computable.
Rationale: $\lambda$-calculus can be implemented (simulated) on a Turing machine; all reduction rules are mechanical and finite.
Conclusion: The three formalisms are equivalent: $$ \text{Partial Recursive} = \lambda\text{-definable} = \text{Turing-computable} $$

Normal order reduction: Always reduce the leftmost, outermost redex (i.e., the redex whose $\lambda$ is to the left of all others).
Theorem (Normalization): If a term has a normal form, then normal order reduction will find it (i.e., normal order is normalizing). $$ M \rightarrow_\beta^ N \text{ and } N \text{ is a normal form} \implies M \xrightarrow{\text{normal order}}^ N $$

$\lambda$-calculus is a minimal, powerful model of computation based on function abstraction and application.
Church numerals encode natural numbers.
$\lambda$-definability exactly captures the notion of computable functions (partial recursive).
Equivalence with Turing machines and recursive functions confirms Church's Thesis from another angle.
Normal order reduction provides a deterministic strategy that always finds a normal form if one exists.