停止性問題とソフトウェア
http://d.hatena.ne.jp/m-hiyama/20090311/1236729482から連想したwikipedia:停止性問題の話。
前から疑問だったのだけども
「プログラムAとデータxが与えられたとき、A(x)が有限時間で停止するかどうかを決定せよ」
の「データx」は不要な情報ではないのかな。Aとxを結びつけたものをA'と呼べば、
全てのプログラムA'に対し、 -A'()が有限時間で停止する ⇒ H(A')は有限時間でYESを出力して停止する。 -A'()は有限時間では停止しない ⇒ H(A')は有限時間でNOを出力して停止する。 Hの定義より、Hは入力(A')によらず必ず停止する事に注意されたい。
となる。いや、結びつけて云々という説明を省くためなのかもしれないが。
もう一つ疑問なのだけれども
不完全性定理の公理系に相当するものは何か？と考えるとチューリングマシンでは遷移関数しか該当するものがない。では、遷移関数が恒等関数だったとしたらどうか。あらゆるA'()は有限時間では停止しない！
もちろん「停止性問題に欠陥がある！」という話ではなく「遷移関数の性質について言及していないwikipedia:停止性問題の記述はおかしいよね。」という話だ。wikipedia:ゲーデルの不完全性定理と比較するなら「自然数論を含む帰納的に記述可能な公理系」に相当する遷移関数でなければならない。
実践的な話
wikipedia:ゲーデルの不完全性定理に引き写して考えると、A'は
- 有限時間で停止する
- 有限時間では停止しない
- 有限時間で停止するかどうか原理的に証明不能
の三つに分けられそうだが、それはそれとして。この話に載るバグ検証系は基本的に∀A∈{特定の種類のソフトウェア},∀xに対して
- 有限時間で停止する
- 有限時間では停止しない
- 有限時間で停止するかどうか判らなかった
の三つのうち、どれに相当するか判定するものだと思う。分野によっては「原理的に証明不能」と「判らなかった」の差がないものもあるし、明らかに差があるものもある。
実用上は、∃A,∀xに対して
- 有限時間で停止する
- 有限時間では停止しない
のどちらかに相当すると判定できた∃Aのみを利用する、という考えでも構わないと思う。その結果をレーティングとして
- 有限時間での停止を保証
- 有限時間での停止または無限ループを保証
- 無保証
と付けることができたらちょっと面白いかもしれない。
