[Haskell-cafe] Termination of substitution

[Neil Mitchell]

Hi

Thanks for the interesting comments. Its looks like learning some of
the basics about System Fw is probably the way forward.

>  However GHC goes beyond Fw by adding
>         data types
>         letrec
>  This blows strong normalisation out of the water.  (Assuming you have reasonable rules for case and letrec.)  But perhaps if you restrict data types a bit, and place draconian restrictions on letrec (e.g. never inline one) you could retain strong normalisation. It depends how much you want your rules to do.

I have restricted letrec appropriately. I haven't looked at the data
type problem, but given that GHC manages to ignore it, I think its
probably fair for me to ignore it for the time being.

Thanks very much for the helpful comments,

Neil