Church–Rosser theorem

The Church–Rosser theorem states that β-reduction in the λ-calculus is confluent: whenever a term $M$ reduces in some number of steps to $N_{1}$ and also to $N_{2}$ , there is a term $P$ to which both $N_{1}$ and $N_{2}$ reduce^[1]^[2]. A term may contain several redexes, and the theorem says that the choice of which to reduce first never leads to results that cannot be reconciled. Two consequences make it fundamental. A term has at most one normal form, so a terminating computation has one result whatever the evaluation order. And two terms are equal in the λ-calculus exactly when they reduce to a common term, which shows that the calculus is consistent: distinct normal forms, such as $λ x . λ y . x$ and $λ x . λ y . y$ , are never equal. Alonzo Church and J. Barkley Rosser proved the theorem in 1936^[1]. The name is now used for the same property of any rewriting system.

§ 01

Statement

Write $M \to N$ when $N$ results from $M$ by contracting one β-redex, $↠$ for the reflexive and transitive closure of $\to$ , and $=$ for β-conversion, the equivalence relation it generates. The theorem is

M ↠ N_{1} \land M ↠ N_{2} ⟹ \exists P . N_{1} ↠ P \land N_{2} ↠ P

Two terms that reduce to a common term are called joinable. Confluence is equivalent to the Church–Rosser property proper, which is the form Church and Rosser stated: two convertible terms are joinable,

M = N ⟹ \exists P . M ↠ P \land N ↠ P

The Church–Rosser property implies confluence directly, and confluence implies it by induction on the chain of forward and backward reduction steps that make up a conversion^[2]^[11].

Left: the complete reduction graph of (λx. x x) ((λy. y) z), with bound variables renamed for readability. The two paths from the top rejoin at z z, but they take different numbers of steps. Right: an abstract system in which every one-step fork can be joined, but b reduces to the two normal forms a and d.

§ 02

Consequences

If $M$ had two normal forms $N_{1}$ and $N_{2}$ , confluence would give a common reduct $P$ of both, and since normal forms do not reduce, $N_{1} = P = N_{2}$ up to renaming of bound variables. So normal forms are unique, and a normal form can be regarded as the value of a term. Terms without a normal form, such as $(λ x . x x) (λ x . x x)$ , have no value, but no term has two.

If $λ x . λ y . x = λ x . λ y . y$ , the Church–Rosser property would give a common reduct of two distinct normal forms, which is impossible. Hence β-conversion does not equate all terms: the λ-calculus is consistent as an equational theory. Before 1936 this was not known, and the inconsistency of Church's earlier system of logic, of which the λ-calculus was a part, had been shown by Kleene and Rosser in 1935^[2].

Confluence says that a normal form, if there is one, can be reached from every reduct of a term\; it does not say that every strategy reaches it. The term $(λ x . y) Ω$ has the normal form $y$ , but a strategy that keeps reducing $Ω$ never gets there. That leftmost-outermost reduction always finds the normal form is a separate result, the standardization theorem^[2].

§ 03

Why one step is not enough

A tempting proof would show that single steps can be completed to a square: if $M \to N_{1}$ and $M \to N_{2}$ , then $N_{1} \to P$ and $N_{2} \to P$ for some $P$ . Tiling such squares would prove the theorem. But β-reduction does not have this diamond property. Contracting a redex can duplicate another redex, and the copies must then be reduced one at a time.

λ-terms with de Bruijn indices, and the list of all one-step reducts of a term.

(* λ-terms with de Bruijn indices, one-step β-reduction and printing. *)
type t = V of int | L of t | A of t * t
 
let rec shift d c = function
  | V i -> if i >= c then V (i + d) else V i
  | L b -> L (shift d (c + 1) b)
  | A (f, a) -> A (shift d c f, shift d c a)
 
(* subst b a: replace index 0 in b by a, as in (λ. b) a. *)
let subst b a =
  let rec go k = function
    | V i -> if i = k then shift k 0 a else if i > k then V (i - 1) else V i
    | L t -> L (go (k + 1) t)
    | A (f, x) -> A (go k f, go k x)
  in
  go 0 b
 
(* All terms reachable in exactly one β-step. *)
let rec reducts = function
  | V _ -> []
  | L b -> List.map (fun b' -> L b') (reducts b)
  | A (f, a) ->
    (match f with L b -> [ subst b a ] | _ -> [])
    @ List.map (fun f' -> A (f', a)) (reducts f)
    @ List.map (fun a' -> A (f, a')) (reducts a)
 
(* Print with binder names chosen by depth; free variables come from ctx. *)
let names = [| "x"; "y"; "u"; "v"; "w"; "p"; "q"; "r"; "s" |]
let show ?(ctx = [ "z" ]) t =
  let rec go env = function
    | V i -> List.nth (env @ ctx) i
    | L b -> let x = names.(List.length env) in "λ" ^ x ^ ". " ^ go (x :: env) b
    | A (f, a) ->
      let sf = match f with L _ -> "(" ^ go env f ^ ")" | _ -> go env f in
      let sa = match a with A _ | L _ -> "(" ^ go env a ^ ")" | _ -> go env a in
      sf ^ " " ^ sa
  in
  go [] t

Computing the complete reduction graph of a term.

open Lam
 
(* The whole reduction graph of a term, breadth first. *)
let graph m =
  let ids = Hashtbl.create 16 and order = ref [] in
  let rec visit = function
    | [] -> ()
    | t :: rest when Hashtbl.mem ids t -> visit rest
    | t :: rest ->
      Hashtbl.add ids t (Hashtbl.length ids); order := t :: !order;
      visit (rest @ reducts t)
  in
  visit [ m ];
  List.rev_map (fun t -> (Hashtbl.find ids t, t, List.map (Hashtbl.find ids) (reducts t))) !order

Running it on (λx. x x) ((λx. x) z).

t0 = (λx. x x) ((λx. x) z)      -> t1, t2
t1 = (λx. x) z ((λx. x) z)      -> t3, t4
t2 = (λx. x x) z                -> t5
t3 = z ((λx. x) z)              -> t5
t4 = (λx. x) z z                -> t5
t5 = z z                        -> normal form

Reducing the outer redex first copies the inner redex $(λ x . x) z$ twice, and it then takes two steps to reach $z z$ , while the other path takes one. A term can also erase a redex, as $(λ x . y) R$ does. So the one-step forks $t_{1} \leftarrow t_{0} \to t_{2}$ have no one-step join, and the naive induction fails.

§ 04

Proof by parallel reduction

The proof now standard, due to Tait and Martin-Löf, replaces single steps by parallel reduction $⇛$ , which contracts any set of redexes present in a term at once, including none^[2]. It is defined by the rules

x ⇛ x \frac{M ⇛ M ^{'}}{λ x . M ⇛ λ x . M ^{'}} \frac{M ⇛ M ^{'} N ⇛ N ^{'}}{M N ⇛ M ^{'} N ^{'}}

\frac{M ⇛ M ^{'} N ⇛ N ^{'}}{( λ x . M ) N ⇛ M ^{'} [ x := N ^{'} ]}

Every single step is a parallel step, and every parallel step is a sequence of single steps, so $↠$ is also the reflexive and transitive closure of $⇛$ . Takahashi simplified the proof by defining the complete development $M^{*}$ , which contracts every redex of $M$ at once^[4]:

x^{*} (λ x . M)^{*} ((λ x . M) N)^{*} (M N)^{*} = x = λ x . M^{*} = M^{*} [x := N^{*}] = M^{*} N^{*} otherwise

The key lemma, proved by induction on the derivation of $M ⇛ N$ using a substitution lemma, is the triangle property: every parallel reduct of $M$ reduces to $M^{*}$ in one parallel step,

M ⇛ N ⟹ N ⇛ M^{*}

Therefore $⇛$ has the diamond property: two parallel steps from $M$ are joined by one parallel step from each to $M^{*}$ . The diamond property is preserved by taking the reflexive and transitive closure, by tiling the diamonds, so $↠$ has it too, and that is confluence^[4].

Checking the triangle property on random terms, and the failed one-step diamond from the example.

open Lam
 
(* Every term M' with M ⇛ M': contract any subset of the redexes of M,
   including redexes created inside the arguments, in parallel. *)
let rec parallel = function
  | V i -> [ V i ]
  | L b -> List.map (fun b' -> L b') (parallel b)
  | A (f, a) ->
    let fs = parallel f and as_ = parallel a in
    let apps = List.concat_map (fun f' -> List.map (fun a' -> A (f', a')) as_) fs in
    (match f with
     | L b ->
       apps @ List.concat_map (fun b' -> List.map (fun a' -> subst b' a') as_) (parallel b)
     | _ -> apps)
 
(* How many ways parallel can choose, without building the terms. *)
let rec choices = function
  | V _ -> 1
  | L b -> choices b
  | A (f, a) ->
    let n = choices f * choices a in
    (match f with L b -> n + choices b * choices a | _ -> n)
 
(* The complete development M*: contract every redex present in M. *)
let rec star = function
  | V i -> V i
  | L b -> L (star b)
  | A (L b, a) -> subst (star b) (star a)
  | A (f, a) -> A (star f, star a)
 
(* Random terms over the free variables 0 and 1, with plenty of redexes. *)
let rec random depth scope =
  if depth = 0 then V (Random.int (scope + 2))
  else match Random.int 5 with
    | 0 -> V (Random.int (scope + 2))
    | 1 -> L (random (depth - 1) (scope + 1))
    | 2 -> A (L (random (depth - 1) (scope + 1)), random (depth - 1) scope)
    | _ -> A (random (depth - 1) scope, random (depth - 1) scope)

Running it.

terms: 4980, pairs M ⇛ N: 29056, pairs where N ⇛ M* fails: 0
one-step reducts of (λx. x) z ((λx. x) z) and (λx. x x) z in common: 0
M* = z z, reached in one parallel step from both: true

The test enumerates every parallel reduct $N$ of each of about 5,000 random terms and confirms that $M^{*}$ is among the parallel reducts of $N$ . It is not a proof, but it would detect a mistake in the definitions: with the rule for $((λ x . M) N)^{*}$ changed to leave $M$ undeveloped, about 40% of the pairs fail.

§ 05

Local confluence and Newman's lemma

A weaker property is local confluence: every one-step fork $N_{1} \leftarrow M \to N_{2}$ can be joined, by any number of steps. It is much easier to check, since it concerns only single steps, but it does not imply confluence. In the system with $b \to a$ , $b \to c$ , $c \to b$ and $c \to d$ , every fork can be joined by going back and forth between $b$ and $c$ , yet $b$ reduces to the two normal forms $a$ and $d$ .

Checking both properties on that system.

(* Abstract rewriting systems on a finite set of objects. *)
let objects = [ "a"; "b"; "c"; "d" ]
let step = [ ("b", "a"); ("b", "c"); ("c", "b"); ("c", "d") ]
 
let succ x = List.filter_map (fun (u, v) -> if u = x then Some v else None) step
let rec reach seen = function
  | [] -> seen
  | x :: rest when List.mem x seen -> reach seen rest
  | x :: rest -> reach (x :: seen) (succ x @ rest)
let reachable x = reach [] [ x ]
let joinable x y = List.exists (fun z -> List.mem z (reachable y)) (reachable x)
 
let pairs f = List.for_all (fun x -> List.for_all (fun y ->
    List.for_all (fun z -> joinable y z) (f x)) (f x)) objects
let locally_confluent = pairs succ
let confluent = pairs reachable
let normal_forms = List.filter (fun x -> succ x = []) objects

Running it.

locally confluent: true
confluent: false
normal forms reachable from b: a, d

Newman proved in 1942 that the counterexample depends on the infinite loop: a terminating system that is locally confluent is confluent^[3]. Huet gave the short proof by well-founded induction that is now standard^[5]. Newman's lemma does not apply to the untyped λ-calculus, which does not terminate, but it gives a quick proof of confluence for strongly normalizing calculi such as the simply typed λ-calculus.

§ 06

Rewriting systems

Confluence is the central property of term rewriting systems, where it guarantees that rewriting computes a unique result, and a confluent and terminating system decides its equational theory by comparing normal forms^[11]. In a terminating system, local confluence can be decided by computing critical pairs, the terms at which two rules overlap, and checking that each pair is joinable\; this is the basis of Knuth and Bendix's completion procedure^[6]^[5]. Orthogonal systems, whose left-hand sides are linear and do not overlap, are confluent whether or not they terminate, a result that generalizes the Church–Rosser theorem and was proved by Rosen and by Klop^[7]^[8]. Combinatory logic is orthogonal, and therefore confluent.

Two confluent relations that commute have a confluent union, the Hindley–Rosen lemma^[12]^[7]\; it gives confluence of βη-reduction from confluence of β and of η. Confluence is fragile under extension. Klop showed that adding surjective pairing to the untyped λ-calculus as rewrite rules makes it non-confluent, even though the resulting equational theory is consistent^[8].

§ 07

History

Church and Rosser proved the theorem in their 1936 paper “Some properties of conversion”^[1]. Their proof was long and intricate, and simpler proofs have been sought ever since. Newman's abstract treatment of 1942 separated the combinatorial content from the calculus^[3], Hindley's thesis of 1964 studied the property for combinatory logic and unions of relations^[12], and the parallel-reduction proof of Tait and Martin-Löf, presented in Barendregt's monograph^[2], became the standard textbook argument. Takahashi's complete developments of 1995 shortened it further^[4]. The theorem became a benchmark for mechanized mathematics: Shankar checked a proof with the Boyer–Moore theorem prover, published in 1988^[9], and Nipkow formalized several proofs in Isabelle/HOL^[10].