There's a neat thread about strong normalization happening on The Types Forum.
If you've ever wondered Why is it useful to have {type systems,reductions,operations,...} that always terminate? this may Illuminate you.
Here are some snippets to give you a feel for the discussion:
I think it is clearer to split Gérard's original question in two:
- Is strong normalization useful for programming languages ?
- Is the proof of strong normalization via type systems applicable for programming languages?
-- François-Régis Sinot
Termination is good:
If a program is a solution to a problem then knowing that it terminates
for any input is an important aspect of it being a solution. Often the
best way to see that it is terminating is expressing it in a language
where all programs terminate. The programming language Epigram is an
example of an experimental language which is intended to be terminating
(even though not all conditions are enforced in the current version), see
http://www.e-pig.org/ for more information.
-- Thorsten Altenkirch
Termination is good!
I think the moral sense of strong normalization is that a program
in a strictly-typed language can only diverge as a result of some
programming construct, which _explicitly_ permits looping, like
iteration, recursion etc. My favourite example here is that the
"big Omega" can be written in Algol 60, because procedure types
in this language are not fully specified.
-- Pawel Urzyczyn
Termination is good and with fixpoints is turing complete?
Another way to put this is that data structures should be definable in a
strongly-normalising language so that data access, etc. is guaranteed to
terminate. Then add fixpoints or loops to describe arbitrary computations.
-- Barry Jay
Terminating reductions allows exhaustive applications of optimizations:
In a compiler, if a set of reductions is strongly normalizing, then the compiler can apply them exhaustively to an intermediate-language term without fear of looping. (We rely on this in the MLj and SML.NET compilers' "simplify" compilation phases, which apply simple reductions and directed commuting conversions until a normal form is reached. Though it has to be said that it's not the classical SN results that are relevant here, but something more specific to our intermediate language and the simplifying reductions that we employ).
-- Andrew Kenney
Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list.
Recent comments
12 weeks 1 day ago
12 weeks 1 day ago
12 weeks 1 day ago
34 weeks 3 days ago
38 weeks 4 days ago
40 weeks 2 days ago
40 weeks 2 days ago
42 weeks 6 days ago
47 weeks 4 days ago
47 weeks 4 days ago