[Haskell-cafe] Equational Reasoning goes wrong

[Neil Mitchell]

Hi

Haskell is known for its power at equational reasoning - being able to
treat a program like a set of theorems. For example:

break g = span (not . g)

Which means we can replace:

f = span (not . g)

with:

f = break g

by doing the opposite of inlining, and we still have a valid program.

However, if we use the rule that "anywhere we encounter span (not . g)
we can replace it with break g" then we can redefine break as:

break g = break g

Clearly this went wrong! Is the folding back rule true in general,
only in specific cases, or only modulo termination?

Thanks

Neil