Normalization property (lambda-calculus)
Encyclopedia
In mathematical logic
and theoretical computer science
, a rewrite system has the strong normalization property (in short: the normalization property) if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form
. A rewrite system may also have the weak normalization property, meaning that for every term, there exists at least one particular sequence of rewrites that eventually yields a normal form.
does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term
. It has the following rewrite rule: For any term 
,
But consider what happens when we apply
to itself:
Therefore the term
is not strongly normalizing.
including the
simply typed lambda calculus
, Jean-Yves Girard
's System F
, and Thierry Coquand
's calculus of constructions
are strongly normalizing.
A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program terminates
. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be Turing complete
. That means that there are computable functions that cannot be defined in the simply typed lambda calculus (and similarly there are computable functions that cannot be computed in the calculus of constructions or System F). As an example, it is impossible to define a self-interpreter
in any of the calculi cited above.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
and theoretical computer science
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
, a rewrite system has the strong normalization property (in short: the normalization property) if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form
Normal form (term rewriting)
In abstract rewriting, a normal form is an element of the system which cannot be rewritten any further. Stated formally, for some reduction relation ⋅ → ⋅ over X a term t in X is a normal form if there does not exist a term t′ in X such that t → t′.Consider...
. A rewrite system may also have the weak normalization property, meaning that for every term, there exists at least one particular sequence of rewrites that eventually yields a normal form.
Untyped lambda calculus
The pure untyped lambda calculusLambda 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...
does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term
. It has the following rewrite rule: For any term ,
But consider what happens when we apply
to itself:
 |
 |
 |
|
 |
|
 |
Therefore the term
is not strongly normalizing.Typed lambda calculus
Various systems of typed lambda calculusTyped lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
including the
simply typed lambda calculus
Typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
, Jean-Yves Girard
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
's System F
System F
System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
, and Thierry Coquand
Thierry Coquand
Thierry Coquand is a professor in computer science at the University of Gothenburg, Sweden. He is known for his work in constructive mathematics, especially the calculus of constructions. He received his Ph.D. under the supervision of Gérard Huet.- External links :*...
's calculus of constructions
Calculus of constructions
The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...
are strongly normalizing.
A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program terminates
Termination analysis
In computer science, a termination analysis is program analysis which attempts to determine whether the evaluation of a given program will definitely terminate. Because the halting problem is undecidable, termination analysis cannot work correctly in all cases. The aim is to find the answer...
. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be Turing complete
Turing completeness
In computability theory, a system of data-manipulation rules is said to be Turing complete or computationally universal if and only if it can be used to simulate any single-taped Turing machine and thus in principle any computer. A classic example is the lambda calculus...
. That means that there are computable functions that cannot be defined in the simply typed lambda calculus (and similarly there are computable functions that cannot be computed in the calculus of constructions or System F). As an example, it is impossible to define a self-interpreter
Self-interpreter
A self-interpreter, or metainterpreter, is a programming language interpreter written in the language it interprets. An example would be a BASIC interpreter written in BASIC...
in any of the calculi cited above.
See also
- Typed lambda calculusTyped lambda calculusA typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
- RewritingRewritingIn mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems...
- Total functional programmingTotal functional programmingTotal functional programming is a programming paradigm that restricts the range of programs to those that are provably terminating....
- Barendregt–Geuvers–Klop conjecture