Y combinator

A lambda term Y with Y f = f (Y f) for every f, which gives recursion to a language with no named definitions. Under call-by-value it loops before f is ever called; the Z combinator puts the self-application behind a lambda and works in strict languages.

Y = λ f . (λ x . f (x x)) (λ x . f (x x))

Two β-steps show that it is a fixed-point combinator:

Y g \to_{β} (λ x . g (x x)) (λ x . g (x x)) \to_{β} g ((λ x . g (x x)) (λ x . g (x x))) =_{β} g (Y g)

Recursion then needs no names. Factorial is $Y$ applied to a function that receives factorial as its first argument:

fact = Y (λ s . λn . if n = 0 then 1 else n \times s (n - 1))

Under call-by-value an argument is evaluated before the call. In $g (x x)$ the argument $x x$ is $Y g$ again, so evaluation unfolds $Y g \to g (Y g) \to g (g (Y g)) \to \dots$ without ever entering $g$ . The Z combinator η-expands the self-application:

Z = λ f . (λ x . f (λ v . x x v)) (λ x . f (λ v . x x v))

$λ v . x x v$ is a value, so it is passed to $f$ unevaluated, and the self-application happens only when $f$ calls it with an argument.

In OCaml. x x has no simple type, so self-application goes through a recursive datatype; with that in place, Y and Z differ by one η-expansion.

(* Self-application needs a recursive type: a value that can be applied to itself. *)
type 'a fix = Fix of ('a fix -> 'a)
 
(* Y: fine under call-by-name, loops under call-by-value. *)
let y f = let g (Fix x as fx) = f (x fx) in g (Fix g)
 
(* Z: the self-application is under a lambda, so it waits for an argument. *)
let z f = let g (Fix x as fx) = f (fun v -> x fx v) in g (Fix g)
 
let fact = z (fun self n -> if n = 0 then 1 else n * self (n - 1))
let fib = z (fun self n -> if n < 2 then n else self (n - 1) + self (n - 2))

Running it.

fact 10       ->  3628800
fib 20        ->  6765
y ... 10      ->  exception Stack_overflow

No fixed-point combinator has a type in the simply typed λ-calculus, where every term normalizes. Typed languages add recursion as a primitive instead, let rec or a fix constant. Read as logic, the same term is Curry's paradox: with an unrestricted fixed point every proposition has a proof.