Lambda calculus

The lambda calculus is the smallest model of computation that's still universal. There are no numbers, no if, no data structures — just three things: variables, abstraction (build a function), and application (call a function). From that, you can encode anything a Turing machine can do. Functional programming languages are syntactic sugar over this core.

The three forms

That's the entire grammar. Every program is built from these three forms. Application associates left: f x y means (f x) y.

Reduction: β

β-reduction is the one computational rule: substituting a function's argument for its parameter in the body.

(λx. x + 1) 5   →β   5 + 1   →   6

In Clojure terms: ((fn [x] (+ x 1)) 5) → (+ 5 1) → 6. β-reduction is function call.

A simpler example, no arithmetic needed:

(λx. λy. x) a b
  →β  (λy. a) b      ;; substitute x := a
  →β  a              ;; substitute y := b (y not in body, so just drop it)

That term λx. λy. x is the K combinator — "ignore the second argument and return the first." (See the SKI topic for more.)

You can encode anything

The lambda calculus has no booleans, no numbers, no pairs — but you can represent them as functions. Here are the Church booleans:

T = λx. λy. x   ;; "pick first"
F = λx. λy. y   ;; "pick second"

if c then a else b   ≡   c a b

T a b → a, F a b → b. The "if" disappears: a boolean is the choice it makes. In Clojure:

Numbers can be encoded too (Church numerals: n = "apply f n times"), pairs as λs. s a b, lists as nested pairs. The lambda calculus is the minimal substrate; everything else is a library on top of it.

α-conversion (renaming) and free vs bound variables

A variable is bound if it appears under a λ that mentions it, and free otherwise:

λx. x + y      ;; x is bound, y is free

You can rename bound variables freely: λx. x and λz. z are the same function. This is α-conversion. It matters because before substituting into a λ's body you may need to rename bound variables to avoid capturing free ones — the rule that makes β-reduction safe.

Why the lambda calculus matters

• It's the mother of functional programming. Every FP language (Haskell, ML, Clojure, Scheme) is a lambda calculus with extra features.
• It's the substrate for type theory (the next conceptual layer — see the Curry-Howard topic).
• It's how you understand evaluation strategies (call-by-value vs call-by-name vs lazy) precisely.
• Combinators (S, K, I — next topic) are a point-free presentation of the same calculus, illuminating what variables are really doing.

Check yourself

Exercise

Reduce by hand:

((λf. λx. f (f x)) (λy. y + 1)) 3

(Hint: that first λf. λx. f (f x) is the Church numeral 2 — "do it twice".) Expected final value: 5.