Vコンビネータの導出

昨日はベッドの上で昼間わからなかった Vx = V の導出を考えていたらわかった
Ax = xとなるxはM(BAM)であることが割と簡単に証明できる。M(BAM) = (BAM)(BAM) = A(M(BAM))。Kx = xたるxはVであることは簡単に示せる。Kxy = x, Kxy = (Kx)y = xy. thus xy = x. で、あとはM = SIIとI = SKKまでは理解していたのでBをSから導出するだけ。

Sってとても便利で、いらない引数をくくりだすことができる。

1: xX = (I x)(KX x) = SI(KX)x
2: X(Yx) = (KX x)(Y x) = S(KX)Yx
3: XxY = (X x)(KY x) = SX(KY)x
4: Xx(Yx) = (X x)(Y x) = SXYx

Bxyz = x(yz)
= (Kx z)(y z)
= S(Kx)yz
= (KS x)(K x) yz
= S(KS)K xyz

よって

V = M(BKM)
= ( (S(KS)KK) (S(SKK)(SKK)) )( (S(KS)KK) (S(SKK)(SKK)) )
Vx = ( (S(KS)KK) (S(SKK)(SKK)) )( (S(KS)KK) (S(SKK)(SKK)) )x
= ( (KS)K (KK)(S(SKK)(SKK)) )...
= S (KK) (S(SKK)(SKK))  ( (S(KS)KK) (S(SKK)(SKK)) )x
= (KK)(...) ( (S(SKK)(SKK))  ( (S(KS)KK) (S(SKK)(SKK)) )) x
= K ( (S(SKK)(SKK))  ( (S(KS)KK) (S(SKK)(SKK)) )) x
= (S(SKK)(SKK))  ( (S(KS)KK) (S(SKK)(SKK)) ) # xが消えた！
= (SKK)( (S(KS)KK) (S(SKK)(SKK)) ) ((SKK)( (S(KS)KK) (S(SKK)(SKK)) ))
= K( (S(KS)KK) (S(SKK)(SKK)) ) (...) K( (S(KS)KK) (S(SKK)(SKK)) ) (...)
= ( (S(KS)KK) (S(SKK)(SKK)) )( (S(KS)KK) (S(SKK)(SKK)) ) # 元の形に戻った！

この感動を伝えきれていない自信がとてもある。