ここで関数の作用数をチャーチ数をに変換する関数を定義します。
$$\lambda n.n(\lambda z.z+1)0$$
真ん中のラムダ式は整数を$1$増加させるのオペレータです。
Haskellの式では、churchToInt n = n (+1) 0となります。
例えば、$\textbf{2}=\lambda sz.s(s(z))$なので、これにチャーチ数から自然数を求める関数を適用すると
$(\lambda n.n(\lambda z.z+1)0)\textbf{2}
\rightarrow(\lambda n.n(\lambda z.z+1)0)(\lambda sz.s(s(z)))$
$\rightarrow(\lambda z.z+1)((\lambda z.z+1)(0))
\rightarrow(\lambda z.z+1)(1)
\rightarrow 2$
つまり$2$となります。
Haskellで$\textbf{0},\textbf{1},\textbf{2},\textbf{3}$を検証します。
前の記事の算術編１で紹介したsuccessor関数$\textbf{S}$を用いた$\textbf{S0},\textbf{S1},\textbf{S2},\textbf{S3}$もHaskellでもう一度検証します。きちんと$1$増加した値になっていますね。
zero s z = z
one s z = s(z)
two s z = s(s(z))
three s z = s(s(s(z)))
-- チャーチ数を通常の整数に変換
churchToInt n = n (+1) 0
succ' n a b = a (n a b)
main = do
print $ "zero = " ++ show (churchToInt zero)
print $ "one = " ++ show (churchToInt one)
print $ "two = " ++ show (churchToInt two)
print $ "three = " ++ show (churchToInt three)
print $ "succ' zero = " ++ show (churchToInt (succ' zero))
print $ "succ' one = " ++ show (churchToInt (succ' one))
print $ "succ' two = " ++ show (churchToInt (succ' two))
print $ "succ' three =" ++ show (churchToInt (succ' three))
*Main> main
"zero = 0"
"one = 1"
"two = 2"
"three = 3"
"succ' zero = 1"
"succ' one = 2"
"succ' two = 3"
"succ' three =4"