Equational Reasoning goes wrong

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
11 messages Options
Reply | Threaded
Open this post in threaded view
|

Equational Reasoning goes wrong

Neil Mitchell
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
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

Heinrich Apfelmus
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
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

Paul Johnson-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

Conor McBride
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
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

Hugh Perkins
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 g


For 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
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

Hudak, Paul
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
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

Claus Reinke
In reply to this post by Neil Mitchell
> Haskell is known for its power at equational reasoning - being able
> to treat a program like a set of theorems.

when you're trying to do equational reasoning, you better make
sure that you're reasoning with equations. as others have pointed
out some of the more interesting relations between programs are
inequations, where one side is defined in all cases in which the
other is, and both sides are equal whenever both are defined.

the interesting bit here is that the equation you're trying to use is
also part of the program in which you're going to use it (unlike flat
sets of theorems), and if you apply the equation to parts of itself,
you might change it. by sawing off the branch of logic you're
working from, you might then find yourself suspended in mid air.

at the point of definition for an equation 'lhs = rhs', we have an
inequation: lhs is not yet defined, rhs presumably is, and then we
declare them to be equivalent, so that lhs is defined whenever
rhs is, and both have equal values whenever both are defined.

in other words, as long as/whereever our new definition holds,
we can use it as an equation, whereas we only have an
inequation if we start fiddling with the definition itself.

if we replace lhs with rhs in the definition (making the left hand
side "more defined"), we get something valid (semantically,
though not necessarily syntactically) but useless - a tautology
that only "defines" what already was.

if we replace rhs with lhs in the definition (making the right hand
side "less defined"), we get another valid but useless equation -
a tautology that does not add any information to help make a
useful new definition. [this is the variant that loops, making no
progress towards producing information]
 
if our definition is recursive, and we replace an occurrence
of lhs in rhs with an instance of rhs, we have not changed
the information content of the definition.

a very useful group of transformations in non-strict languages
(when you want to make your code less strict, eg in cyclic
programming) are the eta-expansions:

    f --> \x.(f x)              -- f is a function
    p --> (fst p,snd p)     -- p is a pair
    l --> (head l:tail l)     -- l is a list
    ..

all of which add information by "borrowing from the future" -
if f,p,l turn out to be defined, the above are equations,
otherwise they are inequations, the rhs being more defined
than the lhs (because the future payback never happens).

in particular:

    Prelude> let x = x
    Prelude> :t x
    x :: t

    Prelude> let r = (\y->x y,(fst x,snd x),(head x:tail x))
    Prelude> :t r
    r :: (t -> t1, (a, b), [a1])

    Prelude> let f (a,(_,_),(_:_)) = a `seq` ()
    Prelude> :t f
    f :: (t, (t1, t2), [t3]) -> ()

    Prelude> f r
    ()

while

    Prelude> f (x,x,x)
    Interrupted.

well, at least that is my naive way of looking at these things;-)

claus


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

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

Re: Equational Reasoning goes wrong

Janis Voigtlaender
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.227716

Ciao, 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
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

Jon Fairbairn
In reply to this post by Neil Mitchell
"Neil Mitchell" <[hidden email]> writes:

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

To add another viewpoint on what goes wrong: I think you're
being seduced by syntax. When you say that you can replace
"span (not . g)" with "break g", you require that the break
you defined above be in scope. You wouldn't consider

> bother = \break -> break . span (not . g)

to be a suitable candidate for replacement without doing an
alpha conversion first. Now because the definitions in a
haskell programme are all mutually recursive, there's really
a big Y (fix) round the whole lot. Simplifying it a bit, you
could say that unsugaring the definition

> break g = span (not . g)

gives you

> break g := fix (\break -> span (not . g))

(where ":=" denotes non-recursive definition). Now it's
clear that you can't apply your equation in there, because
the break you want to use isn't in scope.

--
Jón Fairbairn                                 [hidden email]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equational Reasoning goes wrong

J.N. Oliveira
In reply to this post by Janis Voigtlaender
Janis Voigtlaender wrote:

> (....)
> http://portal.acm.org/citation.cfm?doid=227699.227716

This paper cites works by L. Kott, but not his PhD thesis "Des
substitutions dans les systemes d'equations algebriques sur le magma"
(Univ. Paris VII, 1979) which is (as far as I can remember) among the
earliest efforts to characterize fixpoint stability with respect to
substitution.

J. Oliveira
www.di.uminho.pt/~jno
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe