This page demonstrates β-reduction in the untyped λ-calculus. Type a term in the "Term" textbox below and press "Reduce" to see how the term gets to a normal form by repeated reductions. The leftmost outermost redexes are always chosen by the system (normal-order reduction); if a term has a normal form, this strategy is known to terminate. For λ abstractions, as well as λx. M, this system permits OCaml or Haskell syntax (fun x -> M or \x -> M), or their mixtures (fun x. M or \x. M).