Beta normal form

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".

Beta reduction

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

: ((mathbf{lambda} x . A(x)) t)

where A(x) is a term (possibly) involving variable x.

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

: ((mathbf{lambda} x . A(x)) t) ightarrow A(t)

where A(t) is the result of substituting the term t for the variable x in the term A(x).

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 ightarrow lambda x_0 ldots lambda x_{i-1} . A(M_1) M_2 ldots M_n , where i geq 0, n geq 1 .

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

Reduction strategies

In general, there can be several different beta reductions possible for a given term. Normal-order reduction is the evaluation strategy in which one continually applies the rule for "beta reduction in head position" until no more such reductions are possible. At that point, the resulting term is in "head normal form".

In contrast, in applicative order reduction, one applies the internal reductions first, and then only applies the head reduction when no more internal reductions are possible.

Normal-order reduction is complete, in the sense that if a term has a head normal form, then normal order reduction will eventually reach it. In contrast, applicative order reduction may not terminate, even when the term has a normal form. For example, using applicative order reduction, the following sequence of reductions is possible:

: (mathbf{lambda} x . z) ((lambda w. w w w) (lambda w. w w w)) : ightarrow (lambda x . z) ((lambda w. w w w) (lambda w. w w w) (lambda w. w w w)): ightarrow (lambda x . z) ((lambda w. w w w) (lambda w. w w w) (lambda w. w w w) (lambda w. w w w)): ightarrow (lambda x . z) ((lambda w. w w w) (lambda w. w w w) (lambda w. w w w) (lambda w. w w w) (lambda w. w w w)):ldots

But using normal-order reduction, the same starting point reduces quickly to normal form:

: (mathbf{lambda} x . z) ((lambda w. w w w) (lambda w. w w w)) : ightarrow z

ee also

* Lambda calculus
* Normal form


Wikimedia Foundation. 2010.

Нужно сделать НИР?

Look at other dictionaries:

  • Normal form — may refer to: Normal form (abstract rewriting) Normal form (databases) Normal form (game theory) Normal form (mathematics) In formal language theory: Beta normal form Chomsky normal form Greibach normal form Kuroda normal form Normal form… …   Wikipedia

  • Beta — may refer to: *Beta (β), the second letter of the Greek alphabetIn finance: * Beta coefficient in Capital Asset Pricing ModelIn mathematics: * Beta function in mathematics * Beta distribution in statistics * False negative rate in statistics *… …   Wikipedia

  • Canonical form — Generally, in mathematics, a canonical form (often called normal form or standard form) of an object is a standard way of presenting that object. Canonical form can also mean a differential form that is defined in a natural (canonical) way; see… …   Wikipedia

  • Normal-gamma distribution — Normal gamma parameters: location (real) (real) (real) (real) support …   Wikipedia

  • Normal-inverse Gaussian distribution — Normal inverse Gaussian (NIG) parameters: μ location (real) α tail heavyness (real) β asymmetry parameter (real) δ scale parameter (real) support …   Wikipedia

  • BETA ISRAEL — BETA ISRAEL, ethno religious group in Ethiopia which claims to be of Jewish origin and which is attached to a form   of the Jewish religion based on the Bible, certain books of the Apocrypha, and other post biblical Scripture; living in the… …   Encyclopedia of Judaism

  • Normal distribution — This article is about the univariate normal distribution. For normally distributed vectors, see Multivariate normal distribution. Probability density function The red line is the standard normal distribution Cumulative distribution function …   Wikipedia

  • Beta-alanine — Chembox new Reference= [ Merck Index , 11th Edition, 196.] ImageFile = Beta alanine structure.svg ImageSize = 150px IUPACName = 3 Aminopropanoic acid OtherNames = β Alanine 3 Aminopropionic acid Section1 = Chembox Identifiers CASNo = 107 95 9… …   Wikipedia

  • Normal order — For other uses, see Normal order (disambiguation). In quantum field theory a product of quantum fields, or equivalently their creation and annihilation operators, is usually said to be normal ordered (also called Wick order) when all creation… …   Wikipedia

  • Normal variance-mean mixture — In probability theory and statistics, a normal variance mean mixture with mixing probability density g is the continuous probability distribution of a random variable Y of the form where α and β are real numbers and σ > 0 and random variables… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”