In the lambda calculus the *β-reduction* rule is a relation
between λ-terms.

If `x`

is a variable and `M`

and `N`

are λ-terms then
`M[x/N]`

is the lambda term where all
free occurrences of `x`

in `M`

have been replaced by `N`

.
The β-reduction is a relation between λ-terms of the form`(λx.M N)`

and the λ-term `M[x/N]`

.
We write: `(λx.M N)`

→_{β}`M[x/N]`

.

If we have `M`

→_{β}`N`

, then `M`

is called the
*β-redex* and `N`

is called the *reductum* or *contractum*.

`λx.x y`

→_{β}`y`

`λx.x λy.y`

→_{β}`λy.y`

H. P. Barendregt. *The Lambda Calculus. Its Syntax and Semantics.* Elsiever, 1984.

W. Kluge. *Abstract Computing Machines. A Lambda Calculus Perspective.* Springer, 2005.

Copyright © 2014 Barry Watson. All rights reserved.