[Haskell-cafe] Equational Reasoning goes wrong

[Hugh Perkins]

On 7/22/07, Neil Mitchell <ndmitchell at gmail.com> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070723/fdbde2ee/attachment.htm