Beta Normal Form - Beta Reduction

In the lambda calculus, a beta redex is a term of the form

where is a term (possibly) involving variable .

A beta reduction is an application of the following rewrite rule to a beta redex

where is the result of substituting the term for the variable in the term .

A beta reduction is in head position if it is of the following form:

$\lambda x_0 \ldots \lambda x_{i-1} . (\lambda x_i . A(x_i)) M_1 M_2 \ldots M_n \rightarrow \lambda x_0 \ldots \lambda x_{i-1} . A(M_1) M_2 \ldots M_n$ , where .

Any reduction not in this form is an internal beta reduction.

Read more about this topic: Beta Normal Form

Famous quotes containing the word reduction:

“The reduction of nuclear arsenals and the removal of the threat of worldwide nuclear destruction is a measure, in my judgment, of the power and strength of a great nation.”
—Jimmy Carter (James Earl Carter, Jr.)