2008 August 7th Thursday (八月　七日　木曜日)

ISZERO = λ n. n (λ x. FALSE) TRUE
TRUE = λ u. λ v. u
FALSE = λ u. λ v. v
0 = λ f. λ x. x
1 = λ f. λ x. f x
2 = λ f. λ x. f (f x)
3 = λ f. λ x. f (f (f x))
FACT = λ n. n (λ u. MULT n (FACT (PRED n))) 1
FACT = Y (λ g. λ n. n (λ u. MULT n (g (PRED n))) 1)
Y = λ f. ((λ x. f (x x)) (λ x. f (x x)))
ISZERO 0
0 (λ x. FALSE) TRUE
=>TRUE
1 (λ x. FALSE) TRUE
=>(λ x. FALSE) TRUE
Here, the "TRUE" and "FALSE" must be considered as Church object, that is to say, they is used to
compute. Let's take a look at the first "FACT". The "n (λ u. MULT n (FACT (PRED n))) 1" will be
expanded by the Church Number "n". If the "n" is "0", okey, the "(λ u. MULT n (FACT (PRED n)))"
replaced the parameter "f" and "1" replaced the parameter "x" (Note: 1 = λ f. λ x. f x ). So, the
"1" is returned directly. In the second "FACT", the technique is similiar, the "(g (PRED n))" make
a recursion to loop multiply next Church number. If the "n (λ u. MULT n (g (PRED n))) 1" expression
find the "n" is "0", the "1" is returned directly; otherwise, the "1" is applied into the
"(λ u. MULT n (g (PRED n)))" lamba expression, the "1" passed into is ignored, the result of "MULT n (g (PRED n))"
is returned.