24 May
2010
24 May
'10
8:28 a.m.
Alexander Solla
On May 23, 2010, at 1:35 AM, Jon Fairbairn wrote:
It seems to me relevant here, because one of the uses to which one might put the symmetry rule is to replace an expression “e1 == e2” with “e2 == e1”, which can turn a programme that terminates into a programme that does not.
I don't see how that can be (but if you have a counter example, please show us).
Oops! I was thinking of the symmetry rule in general. What I said applies to “a && b” and not to “a == b”, but my point was that surely you can’t be sure of that until after you’ve finished a proof that does consider ⊥? -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2009-01-31)