English version
それぞれの具体例は実際にやってみたいと思わないとあまり面白くないかもしれない.計算がどのように進むのかは確かめないと式の羅列でしかないからだ.
PRED を使って引き算を定義する.
SUB := λ m n. n PRED m
SUB 3 2 = (λ m n. n PRED m) (λ f x. f (f (f x))) (λ f x. f (f x))
= (λ n. n PRED (λ f x. f (f (f x)))) (λ f x. f (f x))
= (λ f x. f (f x)) PRED (λ f x. f (f (f x)))
= (λ x. PRED (PRED x)) (λ f x. f (f (f x)))
PRED が二番目の引数分(= 2)コピーされた.これがトリックである.引く数が10 ならば,PRED が 10 個コピーされる.
= PRED (PRED (λ f x. f (f (f x))))
つまり,これは,PRED (PRED 3) であるので,
= PRED 2
= 1
つまり 3 - 2 は 1 である.引き算も可能だった.