lambda-calculus

An Introduction to Lambda Calculus

Section 1. The Story of Lambda Calculus

The origins of lambda calculus are rooted in one of the most profound quests of early 20th-century mathematics: David Hilbert’s program. Hilbert envisioned a complete and consistent foundation for all of mathematics, where every mathematical truth could be derived by a finite set of axioms and rules of inference. To realize this vision, it was essential to formalize the very notion of computation and proof.

Enter Kurt Gödel. In 1931, Gödel shattered Hilbert’s dream with his incompleteness theorems. He proved that in any sufficiently expressive formal system (like arithmetic), there exist true statements that cannot be proven within that system. Furthermore, the system cannot prove its own consistency. This was a turning point: mathematics, it seemed, had limits.

However, Hilbert’s challenge had an unintended consequence. It gave birth to multiple models of computation. Around the same time, Alonzo Church introduced lambda calculus to formalize functions and computation. Independently, Alan Turing developed his model using Turing machines.

Church and Turing eventually proved that their models are equivalent in expressive power, forming the basis for what we now call computability theory. This equivalence led to the Church-Turing thesis: anything computable can be computed by a Turing machine (or, equivalently, via lambda calculus).

Lambda calculus didn’t stop there. It evolved into the foundation of type theory and functional programming languages like Haskell. Through the Curry-Howard correspondence, lambda terms correspond to proofs in logic, and types correspond to propositions. This opened the door to dependent type theory (where types can depend on values) and even deeper connections in mathematics through Homotopy Type Theory (HoTT), blending algebraic topology and logic into one framework.

From a simple notation for defining functions, lambda calculus has grown into a bridge between logic, computation, and the foundations of mathematics.

Section 2. Basics of Lambda Calculus

Lambda calculus has only three syntactic constructs:

Variables: x, y, z, …
Abstraction (function definition): λx. M means a function that maps input x to output M.
Application (function application): M N means apply function M to argument N.

Notation:

Parentheses are used to disambiguate: (λx. x) y applies the identity function to y.

Evaluation Rules:

β-reduction (function application):
- (λx. M) N reduces to M[x := N] (substitute all free occurrences of x in M with N).
α-conversion (renaming bound variables):
- λx. x is the same as λl. l.

These rules form the core of computation in lambda calculus.

Section 3. Encoding Natural Numbers

In lambda calculus, we can encode natural numbers using Church numerals. A natural number n is encoded as a function that applies a given function f to an argument x, n times.

Definitions:

0 := λf. λx. x
1 := λf. λx. f x
2 := λf. λx. f (f x)
3 := λf. λx. f (f (f x))

We can define addition, multiplication, and exponentiation:

Addition: plus = λm. λn. λf. λx. m f (n f x)
Multiplication: mult = λm. λn. λf. m (n f)
Exponentiation: exp = λm. λn. n m

These encodings show the expressive power of pure functions without numbers.

Section 4. Functions with Two Variables

In classical mathematics, a function of two variables like
f(x, y) = x and f(y, x) = x are the same.

In lambda calculus, λxy. x = λx. (λy. x) and λyx. x = λy. (λx. x) are different.

In lambda calculus, functions are curried: they take arguments one at a time.

Example 1:

f = λx. λy. x

This is a function that:

Takes input x,
Returns a function that takes input y,
And returns x (ignoring y).

Example 2:

g = λy. λx. x

This function:

Takes y,
Returns a function that takes x,
And returns x (ignoring y).

They look similar, but behave differently when applied:

(f A B) = A
(g A B) = B

Thus, λx. λy. x ≠ λy. λx. x in lambda calculus. Order matters because arguments are applied one at a time, and each abstraction introduces scope.

This subtlety is crucial for understanding computation, binding, and evaluation in functional languages.

Conclusion

Lambda calculus began as a quest to understand the foundations of mathematics and evolved into one of the most elegant models of computation. Its minimalist design belies a deep expressive power: numbers, logic, data structures, and even mathematical proofs can be represented purely as functions.

Beyond computation, lambda calculus forms the backbone of modern type theory, programming language semantics, and formal verification. Understanding it opens the door to appreciating functional programming, proof assistants like Coq and Agda, and the deep unity between mathematics and computation through the Curry-Howard correspondence.

In its simplicity lies its strength. Lambda calculus invites us to rethink computation from first principles—one function at a time.