[Haskell-cafe] Termination of substitution

[Simon Peyton-Jones]

As Stefan says, System Fw is strongly normalising.  This is a remarkable result because (as you observe) it's very non-obvious how to prove it.

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.

GHC's simplifier deals with the letrec problem by cutting each recursive loop -- see the paper "Secrets of the GHC inliner".  GHC doesn't solve the data type problem at all -- you can make the Simplifier loop if you try.

Simon


| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On Behalf Of Neil Mitchell
| Sent: 12 March 2008 21:05
| To: Haskell Cafe
| Subject: [Haskell-cafe] Termination of substitution
|
| Hi
|
| I'm trying to show that a system of rules for manipulating Haskell
| expressions is terminating. The rules can be applied in any order, to
| any subexpression - and there is a problem if there is any possible
| infinite sequence.
|
| The rule that is giving me particular problems is:
|
| (\v -> x) y   =>   x[v/y]
|
| (I realise this rule may duplicate the computation of y, but that is
| not relevant for this purpose.)
|
| In particular, given the expression
|
| (\x -> x x) (\x -> x x)
|
| we can keep applying this rule infinitely.
|
| However, I don't believe this expression is type safe in Haskell. Are
| any such expressions that would cause this to non-terminate not type
| safe? What are the necessary conditions for this to be safe? Does GHC
| perform lambda reduction, probably by introducing a let binding? Does
| the combination of reducing lambdas and creating let bindings give
| similar problems, particularly if bindings are inlined?
|
| I'm wondering if this rule is genuinely unsafe in Haskell. If it is,
| why isn't it an issue in real simplifiers. If it isn't, what makes it
| safe.
|
| Thanks for any help,
|
| Neil
| _______________________________________________
| Haskell-Cafe mailing list
| Haskell-Cafe at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe