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でラムダ計算:predecessor先行値取得関数

Last updated at Posted at 2024-11-23

今回は自然数$n$の前の自然数$(n-1)$を取得するpredecessor関数を実装してみます。

$n$の先行する値を取得する関数を定義するために、対$(n,n-1)$を定義して、結果として二番目の要素を取り出すことを考えます。
ラムダ計算で対$(a,b)$を下記の関数で定義します。

$$(\lambda z.zab)$$

一番目の要素は$\textbf{T}$を適用することによって取得$$(\lambda z.zab)\textbf{T}\rightarrow\textbf{T}ab\rightarrow a$$二番目の要素は$\textbf{F}$を適用することによって取得できます。
$$(\lambda z.zab)\textbf{F}\rightarrow\textbf{F}ab\rightarrow a$$対を関数でこんな風に定義するなんてミステリアスですね。

Haskellでの対の計算

対関数$(\lambda z.zab)$をHaskellで定義する時に$a,b$を束縛変数にしないとエラーが起きてしまうので、困っていました。ChatGPTに訊いたところ、あっと言う間に答えを教えてくれました。論理的な理解までしているなんてびっくり。

pair a b = \z -> z a b
true x y = x    -- $\lambda xy.x$
false x y = y   -- $\lambda xy.y$
main = do
    print $ pair 1 2 true
    print $ pair 1 2 false
ghci> main
1
2

Φ関数

補助的な関数として、対$p=(n,n-1)$から対$(n+1,n)$を作り出す関数を考えます。
$$\Phi\equiv(\lambda p z.z(\textbf{S}(p\textbf{T}))(p\textbf{T}))$$部分式$p\textbf{T}$は対$p$の第一要素となります。対$\textbf{B}$を基準対として以下のように定義します。

$$\textbf{B}\equiv\lambda z.z\textbf{00}、つまり対(\textbf{0},\textbf{0})$$

Φ(B)

$\Phi(\textbf{B})$を計算してみましょう。
$\Phi(\textbf{B})\rightarrow
(\lambda p z.z(\textbf{S}(p\textbf{T}))(p\textbf{T}))(\textbf{B})$
上記の式で$p$を$\textbf{B}$で置き換えます。
$p\textbf{T}=
\textbf{BT}\rightarrow
(\lambda z.z\textbf{00})\textbf{T}\rightarrow
\textbf{T00}\rightarrow\textbf{0}$となるので、
$\Phi(\textbf{B})\rightarrow
(\lambda z.z(\textbf{S0})\textbf{0})\rightarrow
(\lambda z.z\textbf{10})\rightarrow
\lambda z.z\textbf{10}$

つまり、
$$\Phi(\textbf{B})\rightarrow\lambda z.z\textbf{10}、つまり(\textbf{1},\textbf{0})$$

となります。

Φ(Φ(B))

$\Phi(\textbf{B})\rightarrow\lambda z.z\textbf{10}$を利用して、
$\Phi(\Phi(\textbf{B}))\rightarrow
\Phi(\lambda z.z\textbf{10})\rightarrow
(\lambda p z.z(\textbf{S}(p\textbf{T}))(p\textbf{T}))(\lambda z.z\textbf{10})$

ここで$p\leftarrow(\lambda z.z\textbf{10})$と置き換えると$p\textbf{T}\rightarrow
(\lambda z.z\textbf{10})\textbf{T}
\rightarrow\textbf{T10}\rightarrow\textbf{1}$なので、

$\Phi(\Phi(\textbf{B}))\rightarrow
(\lambda z.z(\textbf{S}\textbf{1})(\textbf{1}))\rightarrow
\lambda z.z\textbf{21}$、つまり対$(\textbf{2},\textbf{1})$となります。

Φ(Φ(Φ(B)))

$\Phi(\Phi(\Phi(\textbf{B})))\rightarrow
\Phi(\lambda z.z\textbf{21})\rightarrow
(\lambda p z.z(\textbf{S}(p\textbf{T}))(p\textbf{T}))(\lambda z.z\textbf{21})$

上記の式で$p\leftarrow\lambda z.z\textbf{21}$と置き換えるので、
$p\textbf{T}\rightarrow(\lambda z.z\textbf{21})\textbf{T}\rightarrow
\textbf{T21}\rightarrow
\textbf{2}$となり、式は
$\Phi(\Phi(\Phi(\textbf{B})))\rightarrow
\lambda z.z(\textbf{S}(\textbf{2}))(\textbf{2})\rightarrow
\lambda z.z(\textbf{3})(\textbf{2})\rightarrow
\lambda z.z\textbf{3}\textbf{2}$、つまり対$(\textbf{3},\textbf{2})$

先行値取得関数P

対$(0,0)=(\lambda z.z\textbf{00})$に関数$\Phi$を$n$回適用して第二要素を取り出したものが、$n$の先行数となります。

$$\textbf{P}\equiv(\lambda n.(n\Phi(\lambda z.z\textbf{00}))\textbf{F})
\equiv(\lambda n.(n\Phi(\textbf{B}))\textbf{F})$$

P1の計算

$\textbf{P1}$はどうなるでしょうか。
$\textbf{P1}\rightarrow
(\lambda n.(n\Phi(\textbf{B}))\textbf{F})\textbf{1}
\equiv(\textbf{1}\Phi(\textbf{B}))\textbf{F}\rightarrow
((\lambda sz.s(z))\Phi(\textbf{B}))\textbf{F}\rightarrow
\Phi(\textbf{B})\textbf{F}$
$\rightarrow(\lambda z.z\textbf{10})\textbf{F}\rightarrow
\textbf{0}$
$$\textbf{P1}\rightarrow\textbf{0}$$

P2の計算

$\textbf{P2}\rightarrow
(\lambda n.(n\Phi(\textbf{B}))\textbf{F})\textbf{2}
\equiv(\textbf{2}\Phi(\textbf{B}))\textbf{F}\rightarrow
((\lambda sz.s(s(z)))\Phi(\textbf{B}))\textbf{F}\rightarrow
(\Phi(\Phi(\textbf{B})))\textbf{F}$
$\rightarrow(\lambda z.z\textbf{21})\textbf{F}\rightarrow
\textbf{1}$
$$\textbf{P2}\rightarrow\textbf{1}$$

P3の計算

$\textbf{P3}\equiv(\lambda n.(n\Phi(\textbf{B}))\textbf{F})\textbf{3}\rightarrow
(\textbf{3}\Phi(\textbf{B}))\textbf{F}\rightarrow
((\lambda s z.s(s(s(z))))\Phi(\textbf{B}))\textbf{F}$
$\rightarrow(\Phi(\Phi(\Phi(\textbf{B})))\textbf{F}\rightarrow
(\lambda z.z\textbf{3}\textbf{2})\textbf{F}\rightarrow
\textbf{2}$
$$\textbf{P3}\rightarrow\textbf{2}$$
かなり長い道のりでしたね(^^;)

Haskellで$\Phi,\textbf{P}, \textbf{B}$など書いてみたのですが、どうもうまく行きません。うまく行きましたら、追記していきます。

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?