English version
引き算をしたいのだが，これまでに作った Church数では負の数がない．これはfの数で数を示していたためだ．簡単のためにここでは負の数を考えないことにするが，より詳しいことは Wikipedia を参照して欲しい．
まず，準備として PRED (predecessor) を考える．これは一つ前の数の意味である．しかしここでは 0 の前は考えないものとする．
PRED := λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)
PRED 2 := (λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)) (λ f x. f (f x))
= (λ f x. (λ f x. f (f x)) (λ g h. h (g f)) (λ u. x) (λ u. u))
= (λ f x. (λ x. (λ g h. h (g f)) ((λ g h. h (g f)) x)) (λ u. x) (λ u. u))
= (λ f x. (λ x. (λ g h. h (g f)) (λ h. h (x f))) (λ u. x) (λ u. u))
= (λ f x. (λ g h. h (g f)) (λ h. h ( (λ u. x) f)) (λ u. u))
= (λ f x. (λ h. h ((λ h. h ( (λ u. x) f)) f)) (λ u. u))
ここで一つ f が消える．
= (λ f x. (λ h. h ((λ h. h x) f)) (λ u. u))
= (λ f x. (λ h. h ((f x))) (λ u. u))
= (λ f x. ((λ u. u) ((f x))) )
= (λ f x. (f x))
= (λ f x. f x)
= 1
ちなみに 0 を入れてみるとどうなるだろうか．
PRED 0 := (λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)) (λ f x. x)
= (λ f x. (λ f x. x) (λ g h. h (g f)) (λ u. x) (λ u. u))
= (λ f x. (λ x. x) (λ u. x) (λ u. u))
= (λ f x. (λ u. x) (λ u. u))
= (λ f x. x)
0 になってしまった．これは良い性質とも言える．PRED は入力が 0 の時は 0 を返し，それ以外は一つ前の数を返す函数である．
ここで面白いと思うのはチャーチ数そのものがプログラムの一部を成している所である．もちろんここでのチャーチ数は函数であるから自然と言えば自然である．
λ n . n (λ g h. h (g f)) は 0 を入れると，
(λ n . n (λ g h. h (g f))) (λ f x . x)
= (λ f x . x) (λ g h. h (g f))
= (λ x . x)
0 が出力される．PRED では他の項があるので，これ以上は詮索しないが，0 が出力されると，最初の項が無視されることに注意しよう．これはチャーチ数の 0 では f が bind されていないからである．