[Haskell-cafe] Equational Reasoning goes wrong

[Jonathan Cast]

It seems to me that the best answer, rather than constraining equational 
reasoning, is to recognize what we're doing.

We start out with a specification for the program we're writing (this could be 
a Haskell script for a previous version of the program, or just a set of 
equations (or other properties) we hope it satisfies).  This specification is 
a predicate on (denotations of) Haskell functions, say S(f).

We then derive an implementation of the program.  This implementation is also 
a predicate, I(f).  By saying we have derived this implementation, we mean 
that S(f) => I(f).  By contrast, the program is correct (our reasoning was 
pointful) iff I(f) => S(f).

This can be guaranteed given the two conditions set forth by John Hughes 
in "The Design of a Pretty-Printing Library", consistency of the 
specification and termination of the implementation.  More precisely, we want 
the two conditions:

(1) There is at least one function f such that S(f).

(2) There is at most one function f such that I(f).

Given (2), we know that {f | I(f)} is either a singleton set or the null set.  
In either case, the powerset P({f | I(f)}) = {{}, {f | I(f)}}.  Now, S(f) => 
I(f), so {f | S(f)} subset {f | I(f)}; thus, {f | S(f)} is either {} or {f | 
I(f)}.  If there is at least one f such that S(f), then {f | S(f)} /= {}, so 
{f | S(f)} = {f | I(f)}, or equivalently S(f) = I(f), so I(f) => S(f).

So if our specification is consistent and our implementation is as total as 
possible (which is equivalent to (2)), the derivation/re-factoring/whatever 
we're doing succeeds.  Otherwise we've got either a bad specification or a 
bad implementation, anyway, so we'll need to investigate the issue in greater 
detail.

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs