Lambda Calculus

Motivation: From Python to Pure Math

In modern programming, we are used to defining named functions that operate on built-in data types. For example, in Python:

def add(x, y):
return x + y

But Python also supports anonymous functions, using the lambda keyword:

add = lambda x, y: x + y

Notice what happened here: the fundamental concept of “addition” doesn’t strictly need a name attached to it. It is just a mapping of inputs to an output.

Invented by Alonzo Church in the 1930s, the $\lambda$-calculus asks a radical question: What if we take this to the absolute extreme? What if a programming language had no built-in data types, no state, no memory, and no named functions? There are no integers, no booleans, and no variables to mutate. Everything—literally every piece of data and control flow—is represented purely by anonymous functions and how they are applied to one another.

Computation here is not “mutating a map.” It is a mechanical process of textual substitution.

1. Syntax: The Ultimate Minimalism

The syntax is remarkably tiny. Every valid expression ($e$) falls into one of three categories:

$$e ::= x \mid \lambda x. e \mid e_1 e_2$$

1. Variables ($x$): A placeholder (e.g., $x, y, z$).
2. Abstraction ($\lambda x. e$): A function definition. It binds the variable $x$ in the expression $e$. You can read this as “a function that takes an argument $x$ and returns $e$.”
3. Application ($e_1 e_2$): A function call. It means “apply the function $e_1$ to the argument $e_2$.”

(Note: Function application is left-associative, so $e_1 e_2 e_3$ means $(e_1 e_2) e_3$. Function bodies extend as far right as possible, so $\lambda x. x y$ means $\lambda x. (x y)$).

2. The Three Mechanics of Computation

A program runs by rewriting itself until it can’t be rewritten anymore (reaching “normal form”). This relies on three rules:

$\alpha$-Conversion (Renaming)

The name of a bound variable doesn’t matter. A function that takes $x$ and returns $x$ is identical to a function that takes $y$ and returns $y$.

$$\lambda x. x \equiv \lambda y. y$$

Why it matters: We need to rename variables to avoid “variable capture” (accidentally overwriting a variable from an outer scope when doing substitutions).

$\beta$-Reduction (Execution)

This is the actual engine of computation. When a function is applied to an argument, you substitute the argument into the function’s body wherever the bound variable appears.

$$(\lambda x. e_1) e_2 \rightarrow e_1[x \mapsto e_2]$$

• $e_1[x \mapsto e_2]$ reads as: “in expression $e_1$, replace all free occurrences of $x$ with $e_2$.”
• Example: $(\lambda x. x y) z \rightarrow z y$

$\eta$-Conversion (Extensionality)

Two functions are the same if they yield the same result for all arguments. If a function just wraps another function, the wrapper is redundant.

$$\lambda x. (f x) \equiv f$$

3. Operational Semantics (Evaluation Strategies)

When you have a complex expression like $(\lambda x. e) ((\lambda y. y) z)$, what do you reduce first? The function body, or the argument? Let $v$ represent a value (a fully evaluated abstraction $\lambda x. e$).

Call-by-Value (Strict / Eager)

Used by most languages (Python, Java, OCaml). You must fully evaluate the argument into a value $v$ before you substitute it into the function.

1. Evaluate left side: $\frac{e_1 \rightarrow e_1'}{e_1 e_2 \rightarrow e_1' e_2}$
2. Evaluate right side: $\frac{e_2 \rightarrow e_2'}{v_1 e_2 \rightarrow v_1 e_2'}$
3. Apply: $\frac{}{(\lambda x. e) v \rightarrow e[x \mapsto v]}$

Call-by-Name (Lazy)

Used in languages like Haskell. You pass the argument unevaluated. It only gets evaluated if the function body actually uses it.

1. Evaluate left side: $\frac{e_1 \rightarrow e_1'}{e_1 e_2 \rightarrow e_1' e_2}$
2. Apply immediately: $\frac{}{(\lambda x. e_1) e_2 \rightarrow e_1[x \mapsto e_2]}$

Example: The Infinite Loop Test

To clearly see the difference in practice, imagine a function that ignores its argument, and an argument that loops forever.

• Call-by-Value (e.g., Python):

def ignore(x):
    return 0

def loop():
    while True: pass

ignore(loop()) # The program freezes here!

Python eagerly evaluates loop() before passing its value to ignore. Since loop() never finishes, the program hangs indefinitely.

• Call-by-Name / Lazy (e.g., Haskell):

ignore x = 0
loop = loop

main = print (ignore loop) -- Instantly prints 0

Haskell passes the unevaluated loop expression directly into ignore. Because the body of ignore never actually uses x, loop is never evaluated, and the program terminates instantly!

4. Church Encodings: Creating Data from Nothing

How is this Turing complete if there are no booleans or numbers? We “fake” them by defining behaviors using pure functions.

Booleans

A boolean represents a choice between two things. So, we define TRUE as a function that takes two arguments and returns the first. FALSE takes two arguments and returns the second.

• $\text{TRUE} \equiv \lambda x. \lambda y. x$
• $\text{FALSE} \equiv \lambda x. \lambda y. y$

An IF-statement is just applying the boolean to the two branches:

• $\text{IF} \equiv \lambda b. \lambda t. \lambda f. b t f$

Example: IF TRUE M N $\rightarrow$ TRUE M N $\rightarrow (\lambda x. \lambda y. x) M N \rightarrow (\lambda y. M) N \rightarrow M$. The control flow emerges entirely from substitution!

Church Numerals

How do we represent numbers? A number $n$ is represented by a function that takes another function $f$ and an argument $x$, and applies $f$ to $x$ exactly $n$ times.

• $0 \equiv \lambda f. \lambda x. x$ (apply $f$ zero times)
• $1 \equiv \lambda f. \lambda x. f x$ (apply $f$ once)
• $2 \equiv \lambda f. \lambda x. f (f x)$ (apply $f$ twice)
• $3 \equiv \lambda f. \lambda x. f (f (f x))$

We can even define a Successor function (SUCC) that takes a Church numeral $n$ and returns $n+1$:

• $\text{SUCC} \equiv \lambda n. \lambda f. \lambda x. f (n f x)$ (Read as: take a number $n$, and apply $f$ one more time to the result of applying $f$ $n$ times to $x$.)

5. Recursion and the Y-Combinator

Here is the ultimate puzzle: How do you write a recursive function (like factorial) if functions don’t have names? You can’t call yourself if you don’t know who you are.

The trick is to pass the function to itself as an argument. To standardize this, logician Haskell¹ Curry discovered the Y-Combinator², a “fixed-point combinator”:

$$Y \equiv \lambda f. (\lambda x. f (x x)) (\lambda x. f (x x))$$

What happens if we apply $Y$ to some function $g$? Let’s $\beta$-reduce it:

1. $Y g = (\lambda f. (\lambda x. f (x x)) (\lambda x. f (x x))) g$
2. Substitute $g$ for $f$: $\rightarrow (\lambda x. g (x x)) (\lambda x. g (x x))$
3. Substitute the right block for $x$ in the left block: $\rightarrow g ((\lambda x. g (x x)) (\lambda x. g (x x)))$

Notice that the giant block inside the parenthesis is exactly step 2 again! So:

$$Y g \rightarrow g (Y g)$$

The Magic: $Y g$ evaluates to $g$ wrapped around another copy of $Y g$. If $g$ is a step in a recursive function (like one iteration of factorial), $Y$ automatically unpacks an infinite supply of $g$‘s whenever needed, effectively creating a while loop or recursion out of thin air, using purely anonymous textual substitution.

Footnotes

1. The Man With Three Languages: Haskell Curry is such a foundational figure in programming language theory that he has three different programming languages named after him: Haskell, Brooks (his middle name), and Curry. Aside from his work on combinatory logic, he is most famous for “Currying”—the technique of transforming a function that takes multiple arguments into a sequence of functions that each take a single argument (e.g., converting f(x, y) into f(x)(y)). If you’ve ever wondered why the $\lambda$-calculus only deals with single-argument functions, Currying is the mathematical justification that proves a single argument is all you ever really need! ↩

2. The Startup Connection: If “Y Combinator” sounds familiar outside of academic computer science, it’s because Paul Graham chose it as the name for his legendary Silicon Valley startup accelerator (the “wet dream” of many founders, having backed Airbnb, Stripe, Reddit, etc.). The metaphor is intentional: just as the mathematical Y-combinator calculates a “fixed point” that allows a program to bootstrap its own execution out of purely anonymous functions, the accelerator aims to act as the ultimate bootstrap mechanism for startups, helping a company create itself from nothing. ↩