Equational Reasoning goes wrong

11 messages
Open this post in threaded view
|

Equational Reasoning goes wrong

 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

 Neil Mitchell wrote: > 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? Well, from the equational point of view, the equation   break p = break p is trivially valid, so nothing is wrong with equational reasoning. Of course, the definitions   break p := span (not . p) and   break p := break p are clearly different, since the latter implies  break p = _|_ . It seems that "de-inlining" can make things less defined. But I think that this phenomenon is an artifact of working with named functions, similar to name capture. I guess it's not present for anonymous lambda terms. Regards, apfelmus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

 In reply to this post by Neil Mitchell 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? > I think this is a case of "fast and loose" reasoning.  Proving that your program doesn't  contain any bottoms can be non-trivial, and as you have pointed out equational reasoning can introduce bottoms where none existed before.  If you ignore the possibility of bottom values you can still prove useful things about your program, its just that the absence of bottoms isn't one of them. For more on this, see http://lambda-the-ultimate.org/node/879 which points to a paper on the subject.  It talks about partial vs total functions (i.e. functions like "+" and ":" are total because any defined arguments give a defined result, but "head" is partial because it only has a defined result for a subset of the possible arguments and bottom the rest of the time).  The gist of the paper is that if you pretend a partial function is total you can get away with it, except that you can get bottoms sometimes. Paul. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

 In reply to this post by Neil Mitchell 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

 In reply to this post by Neil Mitchell On 7/22/07, Neil Mitchell <[hidden email]> wrote: 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 gFor some reason this reminds me of the paradoxes of being able to go back in time.  What I mean is: - as long as we've defined break g = span (not . g), then we can go around replacing everywhere in our program "span(not.g)" with "break g"... unless we happen to replace the "span(not.g )" of the break definition itself... at which point the break definition no longer exists... and so the replaces we just made are invalid... including the replace of the break definition itself... etc... which, for the going back in time thing is like: - we go back in time, and change something so we no longer invent the time machine- ... which means we never invent the time machine- ... and never go back in time- ... and so we do invent the time machine _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

 In reply to this post by Neil Mitchell 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

Open this post in threaded view
|

Re: Equational Reasoning goes wrong

 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-corehttp://sourceforge.net/projects/fid-emacs_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

 In reply to this post by Neil Mitchell I am surprised that no one has mentioned David Sands' work yet in this thread. He has studied this issue extensively in the nineties (setting out from an analogous problem as the one given in Neil's original post). There are a number of papers that came out of this. The one probably most immediately interesting for the problem at hand is: "Total correctness by local improvement in the transformation of functional programs" http://portal.acm.org/citation.cfm?doid=227699.227716Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/mailto:[hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe