ものまね鳥。算数鳥。

ものまね鳥の本において、算数が出来る鳥(コンビネータ)として以下のものが紹介されてる

Vxyz = zxy  // λxyz.zxy
Ix = x      // λx.x
fxy = y     // KI , λxy.y
txy = x     // K , λxy.x

SUCC = Vf
ZERO = I 
ONE = VfI
TWO = Vf(VfI)
THREE Vf(Vf(VfI))

通常のチャーチ数

ZERO = λxy.y   // f, KI
ONE  = λxy.xy  // I
TWO  = λxy.x(xy) 
THREE = λxy.x(x(xy)) 

と違い、見た目は分かり難いけど、
一つ前に戻るPREDを定義するのがチャーチ数にくらべて、圧倒的に楽。

PRED = Tf // T = λxy.yx
// f = KI = λxy.y

PRED(1) -> PRED(VfI) -> Tf(VfI) -> VfIf -> ffI -> I
PRED(2) -> PRED(Vf(VfI)) -> Tf(Vf(VfI)) -> Vf(VfI)f -> ff(VfI) -> VfI

Software foundationでcoqで自然数を定義したときと同じような感覚でPREDが使える。同じラムダ式なのに、チャーチ数との違いはなんなのだろうか。(まー足し算かけ算がチャーチ数ほどシンプルに書けないんですけどね)

ものまね鳥の本は、このあと僅か数ページで、このコンビネータの自然数表現を利用して一部の隙もなく不完全性定理の証明に特攻して完遂するんですが、そのへんは本を読んで感動してもらうとして、

チャーチ数を前に作ったtoSKメソッドでバラしてみました。

0 = λf.λx.x
  = (lambda (f) (lambda (x) x))     =    f =                                   K I
1 = (lambda (f) (lambda (x) (f x))) =                      I = (S (S (K S) K) (K I))
2 = (lambda (f) (lambda (x) (f (f x)))) =  (S (S (K S) K) I)
3 = (lambda (f) (lambda (x) (f (f (f x))))) =   (S (S (K S) K) (S (S (K S) K) I))
4 = (lambda (f) (lambda (x) (f (f (f (f x))))) = (S (S (K S) K) (S (S (K S) K) (S (S (K S) K) I)))

そういえば、
S (K S) K って Bだ。BlueBirdだ。ルリツグミだ。(ものまね鳥の本的に)
B は Bxyz = x(yz) 、λxyz.x(yz)
これも作った、toSKとbeta-reductionで確かめられる。
(toSK '(x y z) '(x (y z))) ;; => (S (K S) K)
(beta-reduction '(S (K S) K x y z)) ;; => (x (y z))
便利ー

すなわち、チャーチ数とは、

SUCC = S B
ZERO = f
ONE = S B f = I
TWO = S B (S B f) = S B I
THREE = S B (S B (S B f)) = S B (S B I)

なんですね。
知らんかったわー。