β-reduction

β-reduction is the rule of computation of the λ-calculus: an application of a function to an argument, $(λ x . e) a$ , is replaced by the body $e$ with $a$ substituted for $x$ . Substitution has to rename bound variables where necessary so that no free variable of the argument is captured. A term that contains no application of this form is in normal form. By the Church–Rosser theorem, the order in which reductions are performed cannot lead to two different normal forms^[1], and normal-order reduction, which always reduces the leftmost outermost application first, reaches the normal form whenever there is one^[3]. The evaluation strategies of programming languages, call-by-value, call-by-name and call-by-need, are restrictions of β-reduction^[4].

§ 01

Definition

A β-redex is a term of the form $(λ x . e) a$ , and its contractum is $e [a / x]$ , the body with the argument substituted for the parameter:

(λ x . e) a \to_{β} e [a / x]

The one-step reduction relation $\to_{β}$ contracts one redex anywhere in a term, including under a λ and inside an argument. Its reflexive transitive closure $↠_{β}$ is multi-step reduction, and the equivalence it generates, $=_{β}$ , is β-conversion. A term with no redex is in β-normal form. The λ-calculus has two further rules. α-conversion renames a bound variable, $λ x . e = λ y . e [y / x]$ when $y$ is not free in $e$ , and terms are normally considered up to it. η-reduction removes a redundant abstraction, $λ x . f x \to_{η} f$ when $x$ is not free in $f$ ^[2].

Capture-avoiding substitution

Substitution replaces the free occurrences of a variable. It is defined by recursion on the term^[2]:

x [a / x] (λ x . e) [a / x] (λ y . e) [a / x] (λ y . e) [a / x] = a y [a / x] = y (y \neq = x) (e_{1} e_{2}) [a / x] = e_{1} [a / x] e_{2} [a / x] = λ x . e = λ y . e [a / x] if y \in / FV (a) = λ z . e [z / y] [a / x] if y \in FV (a), with z fresh

The last case renames the bound variable before substituting under it. Without it, a free variable of the argument that happens to share its name with a binder in the body would become bound, and the meaning of the term would change:

Named λ-terms with a parser and printer, used by the programs below.

(* Named lambda terms, a small parser, and printing. *)
type t = Var of string | Lam of string * t | App of t * t
 
let rec free = function
  | Var x -> [ x ]
  | Lam (x, b) -> List.filter (( <> ) x) (free b)
  | App (a, b) -> free a @ free b
 
(* Parser for terms like  \x y. x (y z). *)
let parse s =
  let n = String.length s and i = ref 0 in
  let rec ws () = if !i < n && s.[!i] = ' ' then (incr i; ws ()) in
  let ident () =
    ws ();
    let j = !i in
    while !i < n && (match s.[!i] with 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '\'' | '_' -> true | _ -> false) do incr i done;
    String.sub s j (!i - j)
  in
  let rec term () =
    ws ();
    if !i < n && s.[!i] = '\\' then (
      incr i;
      let rec params acc = ws (); if s.[!i] = '.' then (incr i; List.rev acc) else params (ident () :: acc) in
      let xs = params [] in
      List.fold_right (fun x b -> Lam (x, b)) xs (term ()))
    else
      let rec apps f = ws (); if !i < n && s.[!i] <> ')' then apps (App (f, atom ())) else f in
      apps (atom ())
  and atom () =
    ws ();
    if s.[!i] = '(' then (incr i; let t = term () in ws (); incr i; t)
    else if s.[!i] = '\\' then term ()
    else Var (ident ())
  in
  term ()
 
let rec show = function
  | Var x -> x
  | Lam (x, b) -> "\\" ^ x ^ ". " ^ show b
  | App (a, b) ->
      (match a with Lam _ -> "(" ^ show a ^ ")" | _ -> show a) ^ " " ^ (match b with Var x -> x | _ -> "(" ^ show b ^ ")")
 
let rec size = function Var _ -> 1 | Lam (_, b) -> 1 + size b | App (a, b) -> 1 + size a + size b

Naive substitution and capture-avoiding substitution.

(* Naive substitution: replaces free x in t by s, ignoring capture. *)
let rec subst_naive x s = function
  | Var y -> if y = x then s else Var y
  | Lam (y, b) -> if y = x then Lam (y, b) else Lam (y, subst_naive x s b)
  | App (a, b) -> App (subst_naive x s a, subst_naive x s b)
 
(* Capture-avoiding substitution: rename a binder that would capture a
   free variable of s. *)
let rec fresh y avoid = if List.mem y avoid then fresh (y ^ "'") avoid else y
 
let rec subst x s = function
  | Var y -> if y = x then s else Var y
  | App (a, b) -> App (subst x s a, subst x s b)
  | Lam (y, b) when y = x -> Lam (y, b)
  | Lam (y, b) when List.mem y (free s) && List.mem x (free b) ->
      let y' = fresh y (free s @ free b) in
      Lam (y', subst x s (subst y (Var y') b))
  | Lam (y, b) -> Lam (y, subst x s b)
 
(* One beta-step at the root, if the term is a redex. *)
let contract subst = function App (Lam (x, b), a) -> Some (subst x a b) | _ -> None

Contracting three redexes with each.

(\x. \y. x) y
  naive:           \y. y
  capture-avoiding: \y'. y
(\x. \y. x y) (\z. y)
  naive:           \y. (\z. y) y
  capture-avoiding: \y'. (\z. y) y'
(\f. \x. f (f x)) x
  naive:           \x. x (x x)
  capture-avoiding: \x'. x (x x')

In the first example, $(λ x . λ y . x) y$ should be a constant function returning the free $y$ , and naive substitution produces the identity function instead. Implementations avoid the problem by generating fresh names, or by eliminating names altogether with de Bruijn indices, in which a variable is the number of binders between it and its own binder, so that no renaming is ever needed^[10].

§ 02

Confluence

A term can contain several redexes, and reducing different ones leads to different terms. The Church–Rosser theorem says that the choice does not matter in the end^[1]:

M ↠_{β} N_{1} and M ↠_{β} N_{2} ⟹ \exists P . N_{1} ↠_{β} P and N_{2} ↠_{β} P

Two consequences follow. A term has at most one normal form, up to α-conversion, so the normal form can be regarded as the value of the term. And two terms are β-convertible exactly when they reduce to a common term, so the λ-calculus is consistent: distinct normal forms such as $λ x . λ y . x$ and $λ x . λ y . y$ are not equal. The standard modern proof uses parallel reduction, which contracts any set of redexes present in a term simultaneously and has the diamond property^[11].

§ 03

Normal forms and strategies

Not every term has a normal form. $Ω = (λ w . w w) (λ w . w w)$ reduces only to itself. Some terms have a normal form that one order of reduction finds and another misses: $(λ x . z) Ω$ reduces to $z$ in one step if the outer redex is contracted, and forever if $Ω$ is reduced first. A reduction strategy chooses which redex to contract:

Normal order contracts the leftmost outermost redex, so a function is applied before its argument is reduced. Applicative order contracts the leftmost innermost redex, so arguments are reduced to normal form before they are passed.

Normal-order and applicative-order reduction, with a step limit, and a trace.

let rec fresh y avoid = if List.mem y avoid then fresh (y ^ "'") avoid else y
let rec subst x s = function
  | Var y -> if y = x then s else Var y
  | App (a, b) -> App (subst x s a, subst x s b)
  | Lam (y, b) when y = x -> Lam (y, b)
  | Lam (y, b) when List.mem y (free s) && List.mem x (free b) ->
      let y' = fresh y (free s @ free b) in Lam (y', subst x s (subst y (Var y') b))
  | Lam (y, b) -> Lam (y, subst x s b)
 
(* Normal order: contract the leftmost, outermost redex. *)
let rec normal = function
  | App (Lam (x, b), a) -> Some (subst x a b)
  | App (a, b) -> (match normal a with Some a' -> Some (App (a', b)) | None -> Option.map (fun b' -> App (a, b')) (normal b))
  | Lam (x, b) -> Option.map (fun b' -> Lam (x, b')) (normal b)
  | Var _ -> None
 
(* Applicative order: contract the leftmost, innermost redex, so an
   argument is normalized before it is passed. *)
let rec applicative = function
  | App (a, b) -> (
      match applicative a with
      | Some a' -> Some (App (a', b))
      | None -> (
          match applicative b with
          | Some b' -> Some (App (a, b'))
          | None -> (match a with Lam (x, body) -> Some (subst x b body) | _ -> None)))
  | Lam (x, b) -> Option.map (fun b' -> Lam (x, b')) (applicative b)
  | Var _ -> None
 
let reduce ?(limit = 1000) step t =
  let rec go n t = if n = limit then None else match step t with Some t' -> go (n + 1) t' | None -> Some (t, n) in
  go 0 t
 
let trace step t =
  let rec go t = print_endline ("  " ^ show t); match step t with Some t' -> go t' | None -> () in
  go t

Running it.

K z Omega, the argument is discarded:  (\x. z) ((\w. w w) (\w. w w))
  normal       z                      1 steps
  applicative  no normal form after 1000 steps
an argument used three times:  (\x. x x x) ((\y. y) a)
  normal       a a a                  4 steps
  applicative  a a a                  2 steps
an argument never used:  (\x. z) ((\y. y y y) ((\w. w) a))
  normal       z                      1 steps
  applicative  z                      3 steps
normal-order reduction of (\x y. y x) a (\z. z z):
  (\x. \y. y x) a (\z. z z)
  (\y. y a) (\z. z z)
  (\z. z z) a
  a a

Normal order finds the normal form of $(λ x . z) Ω$ and applicative order loops. The standardization theorem guarantees that this is general: if a term has a normal form, normal-order reduction reaches it^[3]^[2]. Normal order is not always efficient, though. When the argument is used three times it is copied unreduced and then reduced three times, in four steps against two; when it is not used, normal order saves the work of reducing it. No strategy that reduces terms is optimal for every term. Lévy characterized optimal reduction, which shares the reduction of copied redexes^[12], and Lamping gave an algorithm for it based on graph reduction^[8].

Evaluation in programming languages

Programming languages evaluate programs, not arbitrary terms: they stop at a value and never reduce under a λ. Call-by-value, used by ML, OCaml and most languages, contracts a redex only when its argument is a value, which resembles applicative order without reduction under λ. Call-by-name contracts the outermost redex, like normal order. Plotkin gave the two their precise definitions and relationship, along with the CPS transforms that simulate each in the other^[4]. Call-by-need, the basis of lazy languages such as Haskell, is call-by-name with sharing: an argument is evaluated at most once, the first time it is needed, and its value is shared by every copy, an idea Wadsworth introduced as graph reduction^[7].

§ 04

Cost

A β-step can copy its argument any number of times, so the size of a term can grow exponentially in the number of steps. Church numerals show it: the term $n 2$ has size linear in $n$ , and its normal form, the numeral for $2^{n}$ , has size exponential in $n$ :

Reducing n̄ 2̄ to normal form.

let rec fresh y avoid = if List.mem y avoid then fresh (y ^ "'") avoid else y
let rec subst x s = function
  | Var y -> if y = x then s else Var y
  | App (a, b) -> App (subst x s a, subst x s b)
  | Lam (y, b) when y = x -> Lam (y, b)
  | Lam (y, b) when List.mem y (free s) && List.mem x (free b) ->
      let y' = fresh y (free s @ free b) in Lam (y', subst x s (subst y (Var y') b))
  | Lam (y, b) -> Lam (y, subst x s b)
 
let rec normal = function
  | App (Lam (x, b), a) -> Some (subst x a b)
  | App (a, b) -> (match normal a with Some a' -> Some (App (a', b)) | None -> Option.map (fun b' -> App (a, b')) (normal b))
  | Lam (x, b) -> Option.map (fun b' -> Lam (x, b')) (normal b)
  | Var _ -> None
 
let rec nf n t = match normal t with Some t' -> nf (n + 1) t' | None -> (t, n)
 
(* The Church numeral n, as a string: \f x. f (f (... x)). *)
let church n = "(\\f x. " ^ String.concat "" (List.init n (fun _ -> "f (")) ^ "x" ^ String.make n ')' ^ ")"

Running it.

n     term size    normal form    steps
1            13              7        2
2            15             11        6
4            19             35       30
6            23            131      126
8            27            515      510
10           31           2051     2046

Counting β-steps is therefore not obviously a reasonable measure of time. Accattoli and Dal Lago showed that it is, for normal-order reduction: the number of leftmost-outermost steps to normal form is polynomially related to the time a Turing machine needs to compute it, provided the normal form is represented with sharing^[9].

§ 05

Typed λ-calculi

In the simply typed λ-calculus every reduction sequence terminates, a property called strong normalization; Tait proved it with the method of reducibility candidates, and Girard extended the method to System F^[5]^[6]. Under the Curry–Howard correspondence, a β-redex is a proof that introduces a connective and immediately eliminates it, and β-reduction is the removal of such detours, the normalization of proofs^[6]. Subject reduction, the property that reduction preserves types, is the formal core of the statement that well-typed programs do not go wrong^[13].

§ 06

History

Church introduced the λ-calculus in the early 1930s, with the conversion rules that were later named α, β and η. Church and Rosser proved confluence in 1936^[1], and Curry and Feys proved the standardization theorem, from which the normalizing property of normal order follows^[3]. Wadsworth's 1971 thesis introduced graph reduction and call-by-need^[7], de Bruijn his nameless notation in 1972^[10], and Plotkin in 1975 related the calculus to the call-by-name and call-by-value evaluation of programming languages^[4]. Barendregt's monograph of 1981, revised in 1984, is the standard reference^[2].