In the lambda calculus

Lambda calculus

In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped 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


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:

• , where .
  
  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
  Evaluation strategy
  In computer science, an evaluation strategy is a set of rules for evaluating expressions in a programming language. Emphasis is typically placed on functions or operators: an evaluation strategy defines when and in what order the arguments to a function are evaluated, when they are substituted...
  
   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:
  
  
  But using normal-order reduction, the same starting point reduces quickly to normal form:
  
  
  Sinot's director string
  Director string
  In mathematics, in the area of lambda calculus and computation, directors or director strings are a mechanism for keeping track of the free variables in a term...
  
  s is one method by which the computational complexity of beta reduction can be optimized.
  The source of this article is wikipedia, the free encyclopedia.  The text of this article is licensed under the GFDL.