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.