
10 Feb
2009
10 Feb
'09
6:57 a.m.
On Mon, Feb 9, 2009 at 10:50 PM, Iavor Diatchki
I 0 * _ = I 0 I x * I y = I (x * y)
Note that (*) is now non-commutative (w.r.t. _|_). Of course, that's what we need here, but it means that the "obviously correct" transformation of
foo x = if x == 0 then 0 else foo (x - 1) * foo (x + 1)
into foo' x = if x == 0 then 0 else foo' (x + 1) * foo' (x - 1) is *not* in fact correct. --Max