Definition
The lambda calculus is a formal system for expressing computation based on function abstraction and application. Developed by Alonzo Church in the 1930s, it provides a minimal yet universal model of computation.
Syntax
- Variable: If , then
- Application: If , then
- Abstraction: If and , then
Free Variables
A Free Variable is a variable that is not bound by a lambda abstraction within a term. The set of free variables is defined inductively:
\text{FV}(x) &= \{x\} \\ \text{FV}(s \, t) &= \text{FV}(s) \cup \text{FV}(t) \\ \text{FV}(\lambda x. t) &= \text{FV}(t) \setminus \{x\} \end{aligned}$$ A term with no free variables is called *closed* or a *combinator*. ## Substitution [[Substitution]] $t[s/x]$ replaces all free occurrences of $x$ in $t$ with $s$. Capture-avoiding substitution is defined: $$\begin{aligned} x[s/x] &= s \\ y[s/x] &= y \quad \text{if } x \neq y \\ (t_1 \, t_2)[s/x] &= (t_1[s/x]) \, (t_2[s/x]) \\ (\lambda x. t)[s/x] &= \lambda x. t \\ (\lambda y. t)[s/x] &= \lambda y. (t[s/x]) \quad \text{if } x \neq y \text{ and } y \notin \text{FV}(s) \end{aligned}$$ ## Reduction Rules ### Beta Reduction (β-reduction) The fundamental [[Computation Rule]] of lambda calculus: $$(\lambda x. s) \, t =_\beta s[t/x]$$ A term of the form $(\lambda x. s) \, t$ is called a *redex* (reducible expression). ### Alpha Conversion (α-conversion) Renaming of [[Bound Variable|bound variables]] preserves meaning: $$\lambda x. s =_\alpha \lambda y. s[y/x]$$ provided $y \notin \text{FV}(s)$. ### Eta Equivalence (η-equivalence) The [[Eta Rule]] expresses extensionality for functions: $$\lambda x. (s \, x) =_\eta s$$ provided $x \notin \text{FV}(s)$. ## Normal Forms A term is in *normal form* if it contains no redexes and cannot be further reduced. A term is *weakly normalizing* if some reduction sequence leads to a normal form. A term is *strongly normalizing* if all reduction sequences terminate in a normal form. ## Confluence The lambda calculus satisfies the [[Church-Rosser property]]: if $s$ reduces to both $t_0$ and $t_1$, then there exists a term $u$ such that both $t_0$ and $t_1$ reduce to $u$. This ensures that if a normal form exists, it is unique (up to α-equivalence). ## Encodings ### Booleans $$\text{true} = \lambda x \, y. x \quad \text{false} = \lambda x \, y. y$$ Conditional: $\text{if } b \text{ then } s \text{ else } t = b \, s \, t$ ### Pairs $$\text{pair} = \lambda s \, t \, b. b \, s \, t$$ $$\pi_1 = \lambda p. p \, \text{true} \quad \pi_2 = \lambda p. p \, \text{false}$$ ### Church Numerals $$\begin{aligned} \overline{0} &= \lambda f \, x. x \\ \overline{n+1} &= \lambda f \, x. f \, (\overline{n} \, f \, x) \end{aligned}$$ A natural number $n$ is encoded as a function that applies $f$ exactly $n$ times to $x$. ### Y Combinator The fixed-point combinator enables recursion: $$Y = \lambda f. (\lambda x. f \, (x \, x)) \, (\lambda x. f \, (x \, x))$$ This satisfies $Y \, f =_\beta f \, (Y \, f)$, allowing recursive definitions. ## Lambda Definability A function $f : \mathbb{N}^k \to \mathbb{N}$ is *lambda-definable* if there exists a term $s \in \Lambda$ such that: $$s \, \overline{n_1} \, \cdots \, \overline{n_k} =_\beta \overline{f(n_1, \ldots, n_k)}$$ The lambda-definable functions are exactly the computable functions. ## Related Concepts - [[Type Theory]]: Lambda calculus extended with types - [[Function Type]]: The type-theoretic interpretation of lambda abstraction - [[Computation Rule]]: Beta reduction as the fundamental computation rule - [[Substitution]]: The operation underlying beta reduction - [[Free Variable]]: Variables not bound by lambda abstractions - [[Bound Variable]]: Variables introduced by lambda abstractions