Y combinator

The Y combinator is a λ-term $Y$ such that $Y f = f (Y f)$ for every $f$ : it finds a fixed point of any function, and so gives recursion to a language that has no named definitions. Under call-by-value evaluation it loops before $f$ is ever called; the Z combinator delays the self-application behind a λ and works in strict languages. No fixed-point combinator has a type in the simply typed λ-calculus, which is why typed languages provide recursion as a primitive instead.

§ 01

Overview

A recursive definition such as $fact n = if n = 0 then 1 else n \times fact (n - 1)$ refers to its own name. The pure λ-calculus has no names for definitions, only anonymous functions, so the recursion has to be expressed differently. First abstract the recursive call into a parameter:

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

Factorial is then a function $fact$ with $fact = F fact$ : a fixed point of $F$ . A fixed-point combinator produces one for any $F$ , so $fact = Y F$ .

§ 02

Definition

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

Two β-steps show that $Y g$ is a fixed point of $g$ :

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

The equation holds up to β-equality, not by reduction of $Y g$ to $g (Y g)$ : both reduce to the same term. The self-application $x x$ is what makes it work, since it lets a function receive itself as an argument. The fixed-point theorem of the untyped λ-calculus follows: every term $F$ has a fixed point, namely $Y F$ ^[3].

Other fixed-point combinators

$Y$ is one of infinitely many. Turing's $Θ$ has the stronger property that $Θ f$ reduces to $f (Θ f)$ , not just equals it^[2]:

Θ = (λ x . λ f . f (x x f)) (λ x . λ f . f (x x f)) Θ f \to_{β}^{*} f (Θ f)

§ 03

Evaluation order

Under call-by-name, arguments are passed unevaluated, and $Y F n$ unfolds one step at a time as the body of $F$ demands its recursive call. Under call-by-value, arguments are 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$ forever, without ever entering $g$ . The Z combinator η-expands the self-application^[4]:

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

$λ v . x x v$ is a λ, so it is a value, and it is passed to $f$ unevaluated. The self-application happens only when $f$ calls it with an argument, which is exactly when a recursive call is needed.

Y, Z and Turing's combinator in OCaml. Self-application needs a recursive datatype to type-check.

(* x x has no simple type; a recursive datatype gives it one. *)
type 'a fix = Fix of ('a fix -> 'a)
 
(* Y: loops under call-by-value, before f is ever entered. *)
let y f = let g (Fix x as fx) = f (x fx) in g (Fix g)
 
(* Z: the self-application waits behind a lambda for an argument. *)
let z f = let g (Fix x as fx) = f (fun v -> x fx v) in g (Fix g)
 
(* Turing's combinator, strict version: Theta = A A with
   A = fun x f -> f (fun v -> x x f v). *)
let theta f =
  let a (Fix x as fx) = fun f -> f (fun v -> x fx f v) in
  a (Fix a) f
 
let fact_step self n = if n = 0 then 1 else n * self (n - 1)

Running it.

z fact_step 10      ->  3628800
theta fact_step 10  ->  3628800
y fact_step 10      ->  exception Stack_overflow

§ 04

Typing

In the simply typed λ-calculus every term normalizes, so no term loops, and no fixed-point combinator can be typed. The obstruction is $x x$ : $x$ would need a type $τ$ equal to $τ \to σ$ , which no finite simple type is. System F, with polymorphism, still normalizes and still has none^[8].

Two things restore them. Recursive types allow $τ = τ \to σ$ directly, either through a datatype, as in the fix type above, or by switching on equi-recursive types, which OCaml does with -rectypes:

The same Z without the wrapper type, and the type of self-application.

(* With -rectypes, self-application type-checks directly. *)
let z f = (fun x -> f (fun v -> x x v)) (fun x -> f (fun v -> x x v))
let omega_type_of x = x x

What ocamlc -rectypes -i infers.

val z : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b
val omega_type_of : ('a -> 'b as 'a) -> 'b

The type of omega_type_of is the cyclic type 'a -> 'b as 'a: a function that can be applied to itself. The other way is to add recursion as a primitive, which is what every typed functional language does: let rec in ML and OCaml, and in Haskell a library function fix f = let x = f x in x that relies on lazy, recursive let.

§ 05

Semantics

In domain theory, a program denotes a continuous function on a partially ordered set of approximations, with a least element $⊥$ for "no information yet". Kleene's fixed-point theorem gives every continuous $f$ a least fixed point, the limit of its iterates from $⊥$ ^[7]:

fix f = n \geq 0 ⨆ f^{n} (⊥) = ⊥ ⊔ f (⊥) ⊔ f (f (⊥)) ⊔ \dots

For factorial, $F^{n} (⊥)$ is the function that is correct on $0, \dots, n - 1$ and undefined elsewhere, and the limit is correct everywhere. A recursive definition means this least fixed point, and $Y$ computes it.

§ 06

Open recursion

Writing a recursive function as a step function that takes its recursive call as a parameter has uses beyond encoding recursion. A different fixed-point operator can insert behaviour at every recursive call without changing the step function:

One Fibonacci step function run by a plain, a memoizing and a tracing fixed point.

(* Open recursion: the recursive call goes through a parameter, so a
   different fixed-point operator can insert behaviour at every call. *)
let fib_step self n =
  if n < 2 then n
  else
    let a = self (n - 1) in
    let b = self (n - 2) in
    a + b
 
let calls = ref 0
 
(* The plain fixed point, counting calls. *)
let rec fix f n = incr calls; f (fix f) n
 
(* A fixed point that memoizes every call. *)
let memo_fix f =
  let table = Hashtbl.create 64 in
  let rec self n =
    match Hashtbl.find_opt table n with
    | Some v -> v
    | None -> incr calls; let v = f self n in Hashtbl.add table n v; v
  in
  self
 
(* A fixed point that traces calls to a given depth. *)
let trace_fix f =
  let depth = ref 0 in
  let rec self n =
    if !depth < 3 then Printf.printf "%sfib %d\n" (String.make (2 * !depth) ' ') n;
    incr depth;
    let v = f self n in
    decr depth; v
  in
  self

Running it.

fix fib_step 25       ->  75025  (242785 calls)
memo_fix fib_step 25  ->  75025  (26 calls)
trace_fix fib_step 4, first three levels:
fib 4
  fib 3
    fib 2
    fib 1
  fib 2
    fib 1
    fib 0

The same fib_step makes 242,785 calls under the plain fixed point and 26 under the memoizing one, which is dynamic programming obtained without editing the function. Object-oriented languages use the same idea for inheritance: a method calls other methods through self, and a subclass can override them.

§ 07

Logic

Read as logic, a fixed point of implication is a contradiction. If a proposition $A$ could be defined as $A \Rightarrow B$ for arbitrary $B$ , then assuming $A$ gives $A \Rightarrow B$ and so $B$ ; hence $A \Rightarrow B$ holds, which is $A$ , and $B$ follows unconditionally. This is Curry's paradox^[5], and it is the reason logics based on the untyped λ-calculus turned out inconsistent^[6]. Type systems that correspond to consistent logics exclude general fixed points, and proof assistants that allow recursion check that it terminates.

§ 08

History

Kleene and Rosser showed in 1935 that Church's original logic based on the λ-calculus was inconsistent^[6], and Curry gave a simpler paradox of the same kind in 1942^[5]. Turing published $Θ$ in 1937^[2], and $Y$ is usually attributed to Curry, who used it throughout combinatory logic^[1]. Plotkin's 1975 study of call-by-value made the need for the η-expanded form precise^[4]. The startup accelerator Y Combinator, founded in 2005, is named after the combinator.