I've been reading "The Emperor's New Mind" by Roger Penrose. He briefly introduces lambda calculus (pp. 86-92) and gives this formula for addition:
$A = \lambda fgxy.[((fx)(gx))y]$
This was my attempt at using it:
$$ A = \lambda fgxy.[((fx)(gx))y] \\ 1 = \lambda an.an \\ 2 = \lambda bm.b(bm) \\ A12 = \lambda xy.( ( ((\lambda an.an)x) ((\lambda bm.b(bm))x) ) y) \\ = \lambda xy.[ ( ((\lambda an.an)x) (\lambda m.x(xm)) ) y] \\ = \lambda xy.[ ( (\lambda n.xn) (\lambda m.x(xm)) ) y] \\ = \lambda xy.[ ( x((\lambda m.x(xm))) ) y] \\ = \lambda xy.[ ( x(\lambda m.x(xm)) ) y] \\ $$
Is it legal to transform the last step into $= \lambda xy.[x(x(x(y)))]$? I guess it might be (by some informal reasoning), but this seems to go beyond the scope of what Penrose gave an introduction of. Alternative definitions (for example here, slides 27 and 28) don't seem to be problematic.
Thanks!
$A=\lambda fgxy.[((fx)(gx))y]$ must be a typo in the book. (It's in my copy too).
The definition that actually works is $A=\lambda fgxy.[(fx)((gx)y)]$.
Usually this would be written as just $\lambda fgxy.fx(gxy)$, but it seems like Penrose doesn't bother to explain the usual rules for omitting parentheses (basically that $MNK$ means $(MN)K$), and instead writes everything fully parenthesized.