Haskellでラムダ計算の続きです。
数がゼロの時に真、それ以外の時に僞を出力する関数$\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での実装
Haskellで書くと以下のようになりますが、iszero zeroの挙動がおかしいようです。
true x y = x
false x y = y
not' x y = x false true
zero s z = z
three s z = s(s(s(z)))
iszero x = x false not' false
add1 n = (n + 1)
main = do
print $ iszero zero add1 1 0
つまり$\textbf{Z0}\rightarrow\textbf{T}$の型チェックがうまく行っていないようです。
ghci> :t iszero
iszero
:: ((p1 -> p2 -> p2)
-> (((p3 -> p4 -> p4) -> (p5 -> p6 -> p5) -> t1) -> p7 -> t1)
-> (p8 -> p9 -> p9)
-> t2)
-> t2
ghci> :t three
three :: (t -> t) -> t -> t
ghci> :t iszero three
<interactive>:1:8: error:
• Couldn't match type ‘p6’ with ‘p6 -> p6’
Expected: ((((p3 -> p4 -> p4)
-> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> (p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> ((p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> (p3 -> p4 -> p4)
-> (p6 -> p6 -> p6)
-> p6
-> p6
-> p6)
-> (((p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> (p3 -> p4 -> p4) -> p6 -> p6 -> p6)
-> ((p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> (p3 -> p4 -> p4)
-> (p6 -> p6 -> p6)
-> p6
-> p6
-> p6
Actual: ((((p3 -> p4 -> p4)
-> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> (p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> ((p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> (p3 -> p4 -> p4)
-> (p6 -> p6 -> p6)
-> p6
-> p6
-> p6)
-> (((p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> (p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> ((p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6)
-> (p3 -> p4 -> p4)
-> (p6 -> p6 -> p6)
-> p6
-> p6
-> p6
‘p6’ is a rigid type variable bound by
the inferred type of
it :: (p3 -> p4 -> p4) -> (p6 -> p6 -> p6) -> p6 -> p6 -> p6
at <interactive>:1:1
• In the first argument of ‘iszero’, namely ‘three’
In the expression: iszero three