Beta normal form

In the lambda calculus, a term is in beta normal form if no beta reduction is possible. A term is in beta-eta normal form if neither a beta reduction nor an eta reduction is possible. A term is in head normal form if there is no beta-redex in head position. In the lambda calculus, a term is in beta normal form if no beta reduction is possible. A term is in beta-eta normal form if neither a beta reduction nor an eta reduction is possible. A term is in head normal form if there is no beta-redex in head position. In the lambda calculus, a beta redex is a term of the form: A redex r {displaystyle r} is in head position in a term t {displaystyle t} , if t {displaystyle t} has the following shape: A beta reduction is an application of the following rewrite rule to a beta redex contained in a term: where A [ x := M ] {displaystyle A} is the result of substituting the term M {displaystyle M} for the variable x {displaystyle x} in the term A {displaystyle A} . A head beta reduction is a beta reduction applied in head position, that is, of the following form: Any other reduction is an internal beta reduction. A normal form is a term that does not contain any beta redex, i.e. that cannot be further reduced. 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, head normal forms are the terms of the following shape: A head normal form is not always a normal form, because the applied arguments M j {displaystyle M_{j}} need not be normal. However, the converse is true: any normal form is also a head normal form. In fact, the normal forms are exactly the head normal forms in which the subterms M j {displaystyle M_{j}} are themselves normal forms. This gives an inductive syntactic description of normal forms.