[Haskell-cafe] Equational Reasoning goes wrong
paul at cogito.org.uk
Sun Jul 22 14:26:25 EDT 2007
Neil Mitchell wrote:
> 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?
I think this is a case of "fast and loose" reasoning. Proving that your
program doesn't contain any bottoms can be non-trivial, and as you have
pointed out equational reasoning can introduce bottoms where none
existed before. If you ignore the possibility of bottom values you can
still prove useful things about your program, its just that the absence
of bottoms isn't one of them.
For more on this, see http://lambda-the-ultimate.org/node/879 which
points to a paper on the subject. It talks about partial vs total
functions (i.e. functions like "+" and ":" are total because any defined
arguments give a defined result, but "head" is partial because it only
has a defined result for a subset of the possible arguments and bottom
the rest of the time). The gist of the paper is that if you pretend a
partial function is total you can get away with it, except that you can
get bottoms sometimes.
More information about the Haskell-Cafe