pkmnq — 7/2/2022, 6:23:51 PM

Have you ever wanted to “add” addition to addition? Of course “not”, here’s how to “do it” in “lambda” calculus!

+ + +
(\m. \n. \f. \x. m f (n f x)) + +
(\f. \x. + f (+ f x))
(\f. \x. (\m. \n. \g. \y. m g (n g y)) f (+ f x))
(\f. \x. \g. \y. f g (+ f x g y))
(\f. \x. \g. \y. f g ((\m. \n. \h. \z. m h (n h z)) f x g y))
(\f. \x. \g. \y. f g (f g (x g y)))
(\m. \n. \f. \x. m f (m f (n f x)))

Wow, I thought it would be some random useless function, but this is actually the m+m+n function. That kind of makes sense.