[Haskell-cafe] Equational Reasoning goes wrong

[Paul Hudak]

Note that you can take any closed term e and do the following 
"equational reasoning":

e
==> let x = e in x
==> let x = x in x
==> _|_

Technically, though, this is not "wrong", in that it is still 
"consistent", where consistency is defined using the usual information 
ordering on domains.  Conventional equational reasoning is consistent, 
it's just that it may lose information.  And in that sense, it doesn't 
have to lose everything at once -- for example with data structures one 
could go from (e1,e2), say, to (_|_,e2), to (_|_,_|_), and finally to _|_.

As mentioned by a few others, constraining equational reasoning so that 
information is not lost has been studied before, but I'm not sure what 
the state-of-the-art is -- does anyone know?

    -Paul


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?
>
> Thanks
>
> Neil