[Haskell-cafe] Equational Reasoning goes wrong
ndmitchell at gmail.com
Sun Jul 22 10:53:51 EDT 2007
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)
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?
More information about the Haskell-Cafe