numbers.mdwn

   1
   2 Church figured out how to encode integers and arithmetic operations
   3 using lambda terms.  Here are the basics:
   4
   5 0 = \f\x.fx
   6 1 = \f\x.f(fx)
   7 2 = \f\x.f(f(fx))
   8 3 = \f\x.f(f(f(fx)))
   9 ...
  10
  11 Adding two integers involves applying a special function + such that
  12 (+ 1) 2 = 3.  Here is a term that works for +:
  13
  14 + = \m\n\f\x.m(f((n f) x))
  15
  16 So (+ 0) 0 =
  17 (((\m\n\f\x.m(f((n f) x))) ;+
  18   \f\x.fx)                 ;0
  19   \f\x.fx)                 ;0
  20
  21 ~~>_beta targeting m for beta conversion
  22
  23 ((\n\f\x.[\f\x.fx](f((n f) x)))
  24  \f\x.fx)
  25
  26 \f\x.[\f\x.fx](f(([\f\x.fx] f) x))
  27
  28 \f\x.[\f\x.fx](f(fx))
  29
  30 \f\x.\x.[f(fx)]x
  31
  32 \f\x.f(fx)