[Haskell-cafe] Equational Reasoning goes wrong

[Conor McBride]

Hi Neil

You'll be pleased to know that lots of people have been banging their  
heads
off this one.

On 22 Jul 2007, at 15:53, Neil Mitchell wrote:

[..]

> break g = span (not . g)

[..]

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

The latter two. That is,

   (a) folding is decreasing in the definition order: if you still get a
         proper value afterwards, it's what you had before, but you  
might
         introduce looping;
   (b) various people have studied restrictions to the folding rule  
which
         purport to guarantee that definition is preserved, on the nose
         (but they haven't always quite got it right).

You're probably aware that the granddaddy of all this stuff, introducing
the "unfolding" and "folding" rules is:

   A Transformation System for Developing Recursive Programs
     Rod Burstall and John Darlington
     JACM 24(1), 44--67, 1977.

They introduce the unfolding/folding terminology and state the rules in
the naive form. They don't do the metatheory with any rigour but they do
credit an "informal argument" to Gordon Plotkin showing

   "we retain correctness, but we might lose termination unless we  
impose
   some extra restriction".

This whole style of program transformation really caught on in the Logic
Programming community, and it's there that you'll find people trying to
sort out the tangle. (Just use citeseer on Burstall and Darlington and
you'll find plenty of stuff.) Tamaki and Sato adapted the techniques
in 1982, transferring the problem also. They had a go at fixing it in
1983. Gardner and Shepherdson (1991) "Unfold/Fold Transformations of
Logic Programs" certainly give a suitably restricted fold rule, but I'm
sure it wasn't the last word, and that others (eg Manna and Waldinger,
Pettorossi and Proietti) aren't exactly silent on the subject.

I don't know how many of these things live online, but I know that
B&D77, T&S83 and G&S91 live in my filing cabinet...

Hope this helps

Conor