# [Haskell-cafe] Equational Reasoning goes wrong

Jonathan Cast jcast at ou.edu
Sun Jul 22 23:02:10 EDT 2007

```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
```