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

今回は自然数$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$を束縛変数にしないとエラーが起きてしまうので、とりあえず$z,a,b$の束縛変数で定義してみました。

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

Φ関数とP関数

補助的な関数として、対$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}$$

対$(\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})
$$

P3を計算する

例えば、$3$の前の自然数は次のようになるので、reductionしていきながら求めてみましょう。
$\textbf{P3}\equiv(\lambda n.(n\Phi(\lambda z.z\textbf{00}))\textbf{F})\textbf{3}\rightarrow(\textbf{3}\Phi(\lambda z.z\textbf{00}))\textbf{F}$
$\rightarrow((\lambda s z.s(s(s(z))))\Phi(\lambda z.z\textbf{00}))\textbf{F}$
$\rightarrow(\Phi(\Phi(\Phi(\lambda z.z\textbf{00}))))\textbf{F}
\rightarrow(\Phi(\Phi(\Phi(\textbf{B})))\textbf{F}$

ここで$\Phi(\Phi(\Phi(\textbf{B}))$を順次計算していきます。

Φ(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})\textbf{B}\rightarrow
(\lambda z.z\textbf{10})\textbf{B}\rightarrow
(\lambda z.z\textbf{00})\textbf{10}$
$\rightarrow(\textbf{100})\textbf{0}
\rightarrow(\textbf{I})\textbf{0}
\rightarrow\textbf{0}$
なぜならば、$\textbf{100}\rightarrow(\lambda sz.s(z))\textbf{00}
\rightarrow\textbf{0}(\textbf{0})\rightarrow(\lambda sz.z)\textbf{0}\rightarrow\lambda z.z\rightarrow\textbf{I}$なので。
つまり、
$$\Phi(\textbf{B})\rightarrow\textbf{0}$$

となります。

Φ(Φ(B))

この値を利用して、
$\Phi(\Phi(\textbf{B}))\rightarrow
\Phi(\textbf{0})\rightarrow
(\lambda p z.z(\textbf{S}(p\textbf{T}))(p\textbf{T}))(\textbf{0})$
$\rightarrow(\lambda z.z(\textbf{S}(\textbf{0T}))(\textbf{0T}))$
ここで$\textbf{0T}\rightarrow
(\lambda sz.z)\textbf{T}\rightarrow
\lambda z.z\rightarrow\textbf{I}$なので、
$\Phi(\Phi(\textbf{B}))\rightarrow
(\lambda z.z(\textbf{S}\textbf{I})(\textbf{I}))$
ここで$\textbf{SI}\rightarrow
(\lambda nab.a(nab))\textbf{I}\rightarrow
\lambda ab.a(\textbf{I}ab)\rightarrow
\lambda ab.a(ab)=\lambda sz.s(s(z))=\textbf{2}$なので
$\Phi(\Phi(\textbf{B}))\rightarrow
(\lambda z.z(\textbf{2})(\textbf{I}))\rightarrow
\lambda z.z\textbf{2I}$

Φ(Φ(Φ(B)))

$\Phi(\Phi(\Phi(\textbf{B})))\rightarrow
\Phi(\lambda z.z\textbf{2I})\rightarrow
(\lambda p z.z(\textbf{S}(p\textbf{T}))(p\textbf{T}))(\lambda z.z\textbf{2I})$
上記の式で$p$を$\lambda z.z\textbf{2I}$を置き換えるので、
$p\textbf{T}\rightarrow(\lambda z.z\textbf{2I})\textbf{T}\rightarrow
\textbf{T2I}\rightarrow
\textbf{2}$となり、式は
$\Phi(\Phi(\Phi(\textbf{B})))\rightarrow\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{P3}\equiv\Phi(\Phi(\Phi(\textbf{B})))\textbf{F}=
(\lambda z.z\textbf{3}\textbf{2})\textbf{F}\rightarrow
\textbf{F32}\rightarrow\textbf{2}$
かなり長い道のりでしたね(^^;)

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