かんやくしてみる

ここ見ながらとりあえずチャーチ数で2を表現してみる。

^f^x`$f`$f$x
^f``s`k$f``s`k$fi
``s``s`ks``s`kki``s``s`ks``s`kki`ki

なんかできた。そこでこれをちょっと書き直して、

s(s`ks(s`kki))(s(s`ks(s`kki))`ki)

とかした上で引数FとXを付けて本当にチャーチ数になっているのかどうか確かめてみる。

s(s`ks(s`kki))(s(s`ks(s`kki))`ki)FX
(s`ks(s`kki))F((s(s`ks(s`kki))`ki)F)X
s`ks(s`kki)F((s(s`ks(s`kki))`ki)F)X
`ksF((s`kki)F)((s(s`ks(s`kki))`ki)F)X
s(s`kkiF)((s(s`ks(s`kki))`ki)F)X
s`kkiFX(((s(s`ks(s`kki))`ki)F)X)
`kkF(iF)X(((s(s`ks(s`kki))`ki)F)X)
kFX(((s(s`ks(s`kki))`ki)F)X)
F(((s(s`ks(s`kki))`ki)F)X)
F(s(s`ks(s`kki))`kiFX)
F(s`ks(s`kki)F(`kiF)X)
F(`ksF(s`kkiF)(`kiF)X)
F(s(s`kkiF)(`kiF)X)
F(s`kkiFX(`kiFX))
F(`kkF(iF)X(`kiFX))
F(kFXX)
F(FX)

おぉ、なってる。だが長すぎやしないだろうか？