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.