display | more...

A programming language is said to have the Strong Normalization property, or is strongly normalizing if for every well-formed term, every possible sequence of reductions eventually results in a normal form. That is, there are no infinite reduction sequences (ie infinite loops).

This means that for every program in the language we can trivially decide whether or not it halts: it always does. Therefore a strongly normalizing language is not Turing complete.

A nice consequence is that if your language also has the Church-Rosser property, that means you have a simple (though not necesserily efficient) decision procedure for equality of arbitrary programs: simply reduce each one to normal form and then compare.

Although strongly normalizing languages are thus unsuitable as general purpose programming languages because of a lack of Turing-completeness, the nice decidability of equality comes in useful in other applications. For example, an expressive type system may well include a strongly normalizing programming language as a way of doing some (type) computation at compile time.

Showing that all terms strongly normalize is often a tricky affair. Indeed even for the case of the simply-typed lambda calculus without a fixpoint operator , a simple proof based on an inudction on type derivation fails to go through in the case of application. Instead, one has to rely on an argument based on logical relations (sometimes called Tait's method).

Most interestingly, System F (the polymorphic lambda calculus), without either a fixpoint operator or recursive types is also strongly normalizing. (The difficulty of the proof is due to the impredicative nature of type abstraction in this language, as a result naively defining a logical relation may fail to be well-founded. Girard's method based of candidates extends Tait's method to work in this case).

An example of a language that is not strongly normalizing is the untyped lambda calculus, where the Y combinator may be used to write recursive functions. In fact, the simple expression ((lambda (x) (x x)) (lambda (x) (x x))) can be seen as a counter-example to strong normalization in this language.

Log in or register to write something here or to contact authors.