Rubyでわかる？チューリングマシンの停止性問題

論理と計算のしくみを読んでいてチューリングマシンの停止性問題(Halting problem)の証明がしっくり来なかったので、Rubyで書いてみました。こうして書いてみると、証明のアイデアとしては単純明快です。

ちなみに、Lisper のためのチューリングマシンの停止性問題にて書かれている話とほぼ同じ内容です。

証明

停止性問題ってのはものすごく簡単に言えば『「プログラム"machine"に引数"input"を渡した時、無限ループせずに停止するか」を判定するプログラムは書けない』ってことです。このプログラム"halts?"が書けた物として、矛盾を導きます。

halts?が書けたと仮定すると、これを元にして以下のようなプログラムを書くことができます*1。

def my_machine(input)
    if halts?(input, input) then
        while true
            # runs forever
        end
    end

    print "Halted.\n";
end

そして、halts?はこのプログラム"my_machine"の停止性も判断できるはずです。ここでhalts?(:my_machine, :my_machine) の戻り値だけに着目します。halts?がどんな実装をされていたとしても、この値は当然trueかfalseの2値のうちのいずれかです。

trueのときどうなるか、以下のようにテスト用のhalts?を書いて調べます。

def halts?(machine, input)
    if machine == :my_machine && input == :my_machine
        return true
    end

    abort "not implemented"
end

print "halts?: ", halts?(:my_machine, :my_machine), "\n"
my_machine(:my_machine)

結果は以下。

halts?: true
(ここで無限ループ)

halts?は:my_machineが:my_machineという引数について停止すると判定しているのに、:my_machineに実際に:my_machineを渡して動かすと停止しません。

次、falseの場合の実行結果は以下です。

halts?: false
Halted.

halts?は停止しないと判定しているのに、my_machineは停止してしまいました。

よってhalts?(:my_machine, :my_machine)の値がtrueでもfalseでも矛盾してしまうので、こんな関数は書けないってことがわかりました。

*1:ここでhalts?の第一引数にプログラムとしてinputを渡しているのがちょっと気になるかも。書籍内の証明ではチューリングマシンをコード化した自然数を使っているため、halts?の引数のmachineもinputも両方自然数となっているため、このような議論ができます。この辺はデータもプログラムもS式となるLispの例の方が考えやすいです。