ラムダ計算の計算可能性

ラムダ計算について ref 『C言語による計算の理論』.icon p.177-

自然数上の関数$ fを計算するラムダ項$ Mを定義する

$ f(n_1,n_2,\cdots,n_k)=mならば、$ (M \bar{n_1}\bar{n_2}\cdots\bar{n_k}\xrightarrow{\ast}_\beta\bar{m})

$ f(n_1,n_2,\cdots,n_k)\uparrowならば、$ (M \bar{n_1}\bar{n_2}\cdots\bar{n_k})はβ正規形を持たない

このとき$ Mは$ fを計算する、と言う

補足

$ n_1,\cdots,n_kは自然数

$ \bar{n_i}は、$ n_iのチャーチ数

$ n_iをラムダ項で表現したもの

$ f(..)\uparrowは値が未定義であることを示す

ラムダ項による計算可能性と、従来の計算可能性の同値性 ref 『C言語による計算の理論』.icon p.178

以下の2つは同値

①$ fを計算するラムダ項が存在する

②$ fは計算可能である

証明

①→②

②→①

以下のような問題は決定不可能である

$ M,Nが与えられた時に、$ M\xrightarrow{\ast}Nであるかどうかを答える

$ Mが与えられた時に、$ Mがβ正規形を持つかどうかを答える

証明

まず、以下を満たすような、決定不可能集合$ \alpha\subseteq\mathbb{N}と、計算可能部分関数$ fを用意する

$ f(x) = \left\{ \begin{array}{ll} 1 & (x\in\alpha) \\ 未定義 & (x\not\in\alpha) \\ \end{array} \right.

ここで、$ fを計算するラムダ項$ Fを用意すると、以下は全て同値になる

(1)$ n\in\alpha

(2)$ F(\bar{n})\xrightarrow{\ast}_\beta\bar{1}

(3)$ (F\bar{n})はβ正規形を持つ

もし、簡約可能性問題が決定可能ならば、与えられた$ nに対して(2)の成否が判定できることになる

これは$ \alphaが決定不可能であることに矛盾

もし、正規化可能性問題が決定可能ならば、与えられた$ nに対して、(3)の成否が判定できることになる

これは$ \alphaが決定不可能であることに矛盾