week1: shorthand tweaks
[lambda.git] / 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)