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