Church figured out how to encode integers and arithmetic operations using lambda terms. Here are the basics: 0 = \f\x.fx 1 = \f\x.f(fx) 2 = \f\x.f(f(fx)) 3 = \f\x.f(f(f(fx))) ... Adding two integers involves applying a special function + such that (+ 1) 2 = 3. Here is a term that works for +: + = \m\n\f\x.m(f((n f) x)) So (+ 0) 0 = (((\m\n\f\x.m(f((n f) x))) ;+ \f\x.fx) ;0 \f\x.fx) ;0 ~~>_beta targeting m for beta conversion ((\n\f\x.[\f\x.fx](f((n f) x))) \f\x.fx) \f\x.[\f\x.fx](f(([\f\x.fx] f) x)) \f\x.[\f\x.fx](f(fx)) \f\x.\x.[f(fx)]x \f\x.f(fx)