[TYPES] normalization and programming languages

Barry Jay cbj at it.uts.edu.au
Wed Nov 16 16:09:52 EST 2005

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

More information about the Types-list mailing list