0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

Haskellでラムダ計算:ゼロ判定

Last updated at Posted at 2024-11-19

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

型の違いで結果が違うのでしょうか。

0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?