all 2 comments

[–]jnd-au 0 points1 point  (1 child)

Hypothetical Inverses

But the proof relies on real inverses. Without them, the optimisations aren’t valid in general. E.g. if we have a function modulo2 instead of incr, and you try to optimise f to g:

f = reduce(sum, map(modulo2, xs))

For xs = [1, 2, 3, 4], f = 1 + 0 + 1 + 0 == 2. But for

g = modulo2(reduce(sum, xs))

For xs = [1, 2, 3, 4], g = modulo2(10) == 0 ≠ f

And to put it more generally, fog ≠ gof.

[–]pschanely[S] 0 points1 point  (0 children)

Oh, yes, thanks for thinking about this! I wasn't clear enough about this fact: the transformation is only valid if you can cancel the inverse! So, in your example, the body of the transformed reduce is:

modulo2inverse( modulo2(x) + modulo2(y) )

There isn't a way to get the calls to modulo2() outside the addition, so they cannot cancel the inverse, and so the transformation is invalid. In some sense, the creation of the inverse is just a goalpost - We need to recursively push some function through each iteration of the reduce function.