In the lambda calculus the β-reduction rule is a relation between λ-terms.
x is a variable and
N are λ-terms then
M[x/N] is the lambda term where all
free occurrences of
have been replaced by
The β-reduction is a relation between λ-terms of the form
and the λ-term
If we have
M is called the
N is called the reductum or contractum.
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.