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