[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
More information about the Haskell-Cafe
mailing list