Haskellでラムダ計算の続きです。
A Tutorial Introduction to the Lambda Calculus
数がゼロの時に真、それ以外の時に僞を出力する関数$\textbf{Z}$を定義します。
$$\textbf{Z}\equiv \lambda x.x\textbf{F}\neg\textbf{F}$$
ところで、変数$a$に関数$f$をゼロ回適用したものは$a$となります。
$$\textbf{0}f a\equiv(\lambda s z.z)f a\rightarrow a$$
一方、どんな変数$a$に$\textbf{F}$に適用しても、同値関数$\textbf{I}$になってしまいます。
$$\textbf{F}a\equiv(\lambda x y.y)a\rightarrow \lambda y.y\equiv\textbf{I}$$
$\textbf{0}$に$\textbf{F}$に適用すると、$\textbf{0}\textbf{F}\neg\rightarrow\neg$を考慮して、
$$\textbf{Z0}\equiv(\lambda x.x\textbf{F}\neg\textbf{F})\textbf{0}
\rightarrow\textbf{0}\textbf{F}\neg\textbf{F}
\rightarrow\neg\textbf{F}
\rightarrow\textbf{T}$$
となります。自然数$\textbf{N}$を$\textbf{Z}$に適用すると、
$$\textbf{ZN}\equiv(\lambda x.x\textbf{F}\neg\textbf{F})\textbf{N}
\rightarrow\textbf{N}\textbf{F}\neg\textbf{F}
\rightarrow\textbf{IF}
\rightarrow\textbf{F}$$
となります。なぜなら、
$\textbf{NF}\neg
\rightarrow(\lambda fx.f^nx)\textbf{F}\neg
\rightarrow\textbf{F}^n\neg$
$\rightarrow\textbf{F}(\textbf{F}(\ldots(\textbf{F}(\textbf{F}\neg))))$
$\rightarrow\textbf{F}(\textbf{F}(\ldots(\textbf{F}(\textbf{I}))))
\rightarrow\textbf{I}$
なので。
Haskellでの実装
logicalToBin x = x True Falseは真か偽かを判定する関数。Haskellで定義済みのTrue（真）とFalse（偽）を返す。
-- Haskell iszero.hs
true x y = x
false x y = y
logicalToBin x = x True False -- Check whether true or false
not' x = x false true
zero s z = z
one s z = s(z)
two s z = s(s(z))
three s z = s(s(s(z)))
iszero x = x false not' false
add1 n = (n + 1)
main = do
print "(iszero zero) ->"
print $ logicalToBin (iszero zero)
print "(iszero one) ->"
print $ logicalToBin (iszero one)
--print "(iszero two) ->"
--print $ logicalToBin (iszero two)
*Main> main
"(iszero zero) ->"
True
"(iszero one) ->"
False
なぜかlogicalToBin (iszero two)の場合はエラーが出てしまった。
*Main> :t one
one :: (t1 -> t2) -> t1 -> t2
*Main> :t two
two :: (t -> t) -> t -> t
型の違いで結果が違うのでしょうか。