[Haskell-cafe] Termination of substitution

[Neil Mitchell]

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