Beta Reduction

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.

Examples

• λx.x y →_β y
• λx.x λy.y →_β λy.y

References

H. P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. Elsiever, 1984.
W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.