Beta reduction
In the lambda calculus, a beta redex is a term of the form: : (\mathbf{\lambda} x . A) M. A redex r is in head position in a term t, if t has the following shape (note that application has higher priority than abstraction, and that the formula below is meant to be a lambda-abstraction, not an application): : \lambda x_1 \ldots \lambda x_n . \underbrace{(\lambda x . A) M_1}_{\text{the redex }r} M_2 \ldots M_m , where n \geq 0 and m \geq 1. A beta reduction is an application of the following rewrite rule to a beta redex contained in a term: : (\mathbf{\lambda} x . A) M \longrightarrow A[x := M] where A[x := M] is the result of substituting the term M for the variable x in the term A. A head beta reduction is a beta reduction applied in head position, that is, of the following form: : \lambda x_1 \ldots \lambda x_n . (\lambda x . A) M_1 M_2 \ldots M_m \longrightarrow \lambda x_1 \ldots \lambda x_n . A[x := M_1] M_2 \ldots M_m , where n \geq 0 and m \geq 1. Any other reduction is an internal beta reduction. == Normal forms ==
Normal forms
A normal form is a term that does not contain any beta redex, i.e. that cannot be further reduced. Some authors may also include η reductions, hence the distinguishing terms beta normal form and beta-eta normal form. A head normal form is a term that does not contain a beta redex in head position, i.e. that cannot be further reduced by a head reduction. When considering the simple lambda calculus (viz. without the addition of constant or function symbols, meant to be reduced by additional delta rule head normal forms are the terms of the following shape: : \lambda x_1 \ldots \lambda x_n . x M_1 M_2 \ldots M_m , where x is a variable, n \geq 0 and m \geq 0. A head normal form is not always a normal form, ==See also==