[TYPES] normalization and programming languages

[Barry Jay]

Pawel Urzyczyn wrote:

>------------------
>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. 
>P. Urzyczyn
>
>
>  
>
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