Beta normal form

In lambda calculus, a term is in '''beta normal form''' if no ''beta reduction'' is possible.<ref>{{cite encyclopedia| url=http://encyclopedia2.thefreedictionary.com/Beta+normal+form | title=Beta normal form | encyclopedia=Encyclopedia | publisher=TheFreeDictionary.com |accessdate=18 November 2013 }}</ref> 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 the head position''. The normal form of a term, if one exists, is unique (as a corollary of the Church–Rosser theorem).<ref>{{Cite book |last=Thompson |first=Simon |title=Type theory and functional programming |date=1991 |publisher=Addison-Wesley |isbn=0-201-41667-0 |location=Wokingham, England |pages=38 |oclc=23287456}}</ref> However, a term may have more than one head normal form.

==Beta reduction== In the lambda calculus, a '''beta redex''' is a term of the form:<ref name=":0">{{Cite book |last=Barendregt |first=Henk P. |url=https://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf |title=Introduction to Lambda Calculus |year=1984 |edition=Revised |pages=24}}</ref><ref>{{Cite book |last=Thompson |first=Simon |title=Type theory and functional programming |date=1991 |publisher=Addison-Wesley |isbn=0-201-41667-0 |location=Wokingham, England |pages=35 |oclc=23287456}}</ref>

:<math> (\mathbf{\lambda} x . A) M</math>.

A redex <math>r</math> is in '''head position''' in a term <math>t</math>, if <math>t</math> 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):

:<math> \lambda x_1 \ldots \lambda x_n . \underbrace{(\lambda x . A) M_1}_{\text{the redex }r} M_2 \ldots M_m </math>, where <math>n \geq 0</math> and <math>m \geq 1</math>.

A '''beta reduction''' is an application of the following rewrite rule to a beta redex contained in a term:

:<math> (\mathbf{\lambda} x . A) M \longrightarrow A[x := M] </math>

where <math>A[x := M]</math> is the result of substituting the term <math>M</math> for the variable <math>x</math> in the term <math>A</math>.

A ''head'' beta reduction is a beta reduction applied in head position, that is, of the following form:

:<math> \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 </math>, where <math>n \geq 0</math> and <math>m \geq 1</math>.

Any other reduction is an ''internal'' beta reduction.

== Normal forms ==

A '''normal form''' is a term that does not contain any beta redex,<ref name=":0" /><ref name=":1">{{Cite book |last=Thompson |first=Simon |title=Type theory and functional programming |date=1991 |publisher=Addison-Wesley |isbn=0-201-41667-0 |location=Wokingham, England |pages=36 |oclc=23287456}}</ref> ''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:

:<math> \lambda x_1 \ldots \lambda x_n . x M_1 M_2 \ldots M_m </math>, where <math>x</math> is a variable, <math>n \geq 0</math> and <math>m \geq 0</math>.

A head normal form is not always a normal form,<ref name=":1" /> because the applied arguments <math>M_j</math> need not be normal. However, the converse is true: any normal form is also a head normal form.<ref name=":1" /> In fact, the normal forms are exactly the head normal forms in which the subterms <math>M_j</math> are themselves normal forms. This gives an inductive syntactic description of normal forms.

There is also the notion of '''weak head normal form'''. A λ-term, M, is in weak head normal form in case it is a λ-abstraction, <math>M = \mathbf{\lambda} x . N</math> where <math>N</math> is any expression, even containing a redex, or it is in head normal form (in the pure lambda calculus, the only head normal forms that are not λ-abstractions are of the form <math>x M_1 M_2 \ldots M_m</math>, where <math>x</math> is any variable and <math>m \geq 0</math>).<ref>{{cite encyclopedia| url=http://encyclopedia2.thefreedictionary.com/Weak+Head+Normal+Form | title=Weak Head Normal Form | encyclopedia=Encyclopedia | publisher=TheFreeDictionary.com |accessdate=30 April 2021 }}</ref><ref name="Cockett2023"/> Weak head normal forms were introduced by Simon Peyton Jones to reflect the form to which functional languages actually evaluate.<ref name="Cockett2023">{{Cite web |title=Notes on evaluating λ-calculus terms and abstract machines |url=https://cspages.ucalgary.ca/~robin/class/521/lectures_lambda/abstract-machines.pdf |access-date=2024-05-14|date=2023-03-29|first1=J.R.B.|last1=Cockett}}</ref><ref>{{Cite book |last=Peyton Jones |first=Simon L. |title=The implementation of functional programming languages |date=1987 |publisher=Prentice/Hill International |isbn=978-0-13-453333-9 |location=Englewood Cliffs, NJ}}</ref>

==References== {{reflist}}

{{DEFAULTSORT:Beta Normal Form}} Category:Lambda calculus Category:Normal forms (logic) {{Normal forms in logic}}