[Haskell-cafe] Equational Reasoning goes wrong

[Paul Johnson]

Neil Mitchell wrote:
> 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?
>
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.

Paul.