Haskellでラムダ計算：predecessor先行値取得関数

今回は自然数$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}$など書いてみたのですが、どうもうまく行きません。うまく行きましたら、追記していきます。