バグのないプログラムと不完全なこの世界: Architect Note

最近、オライリーの「アンダースタンディングコンピュテーション」を読みました。コンピューターサイエンスの素養がない人にも分かりやすく計算について教えるという内容で、細々と写経しながら読み進めていました。

hirak/memo-understanding-computation ・ GitHub

この本、8章と9章がとにかく面白くて、特にライスの定理は初めて知ったので、自分なりに理解をまとめておこうと思います。

※形式的な証明は私もちゃんと理解していないので、直感的な解説になります。

不可能なプログラムは存在する

我々プログラマーは日々コードを書いているわけですが、プログラムで解けない問題は存在するか考えたことはあるでしょうか？ライスの定理は不可能なプログラムがあることを示した定理です。

ライスの定理 - Wikipedia

計算機科学における計算可能関数の理論に関する定理で、定められた性質Fを満たすかどうかを任意の部分計算可能関数について判定する方法は(Fが自明な場合を除いて)存在しない、というもの。

…うん、ちょっと何言ってるかよく分かんないので、誤解を恐れずにあえて具体的な話に言い換えると、こんな感じでしょうか。

任意のプログラムの文字列を引数に取り、そのプログラムが「Hello, world!」を出力するかどうかを、実行せずに静的解析だけで判定するプログラム、は絶対に書くことができない。

同じように、「このプログラムは無限ループに陥るかどうか」「このプログラムは仕様通り動いているかどうか」などのプログラムの性質を、プログラムで検証して確実に決定することは不可能である。

ここで言う「絶対に書くことができない」は、現代のコンピュータの性能のせいとか、作るのが困難だ、という話ではなくて、どんなにコンピュータの性能が上がったとしても、腕のいい天才プログラマを沢山集めたとしても、どう頑張っても到達することはない、という強烈な否定です。

バグがないことを証明できない？！

私は日々ユニットテストを書いたり、型アノテーションを書いてみたり、四苦八苦しながらプログラミングしています。だから、「バグを完全に見つけてくれる静的解析ツール」があればいいのになーと思っていました。本当に思っています。というかプログラマなら誰でもそういった夢のツールが欲しいと思っているんじゃないでしょうか。

ライスの定理は完璧な静的解析ツールが作れないことを示しています。ちょっと受け入れがたい内容ではないでしょうか？

HelloWorld検証プログラムを作ろうと努力してみる

定理とか知ったことじゃないし、HelloWorld検証プログラムぐらいオレならすぐ作れるぜ！という方のために、少し努力してみましょう。

ここで、「実行せずにプログラムの性質を検証する」という条件に注意してください。HelloWorldだと実行してしまえば出力が1通りなので、evalすれば簡単に検証できます。ライスの定理はプログラムの性質全般に言える話で、「二つのint値を取りその合計値を返すadd関数」みたいに、組み合わせが無数に存在する場合も考えなくてはいけません。

ここではあくまでイメージのためにHelloWorldを選択しているだけですので、ちょっと奇妙ですが実行しないことにこだわって作っていきます。

さて、RubyでHelloWorldと言えばこんな感じでしょうか。

puts "Hello, world!"

ということは、一番素朴なHelloWorld検証プログラムはこうなると思います。

def prints_hello_world?(program)
  program == 'puts "Hello, world!"'
end

…いやいやちょっと待ってください。これではスペースやコメント文の具合で、いくらでもゆらぎが生じてしまいます。putsと"の間に半角スペースが一個でも多ければ、falseになってしまいますね。

というか、分割して書いたりもできるし、

puts "Hello, "
puts "world!"

文字列としては含まれるけど実行されない、というパターンもあるし、

if false
  puts "Hello, world!"
end

わざと難読化して書くこともできるでしょう。

全てを網羅して、結果としてHello worldを出力するかどうかを判別できなければ、prints_hello_world?の実装とは言えないのです。少なくとも、パースして分析することは必須なようです。

def prints_hello_world?(program)
  # programをパースする
  # programを分析する
  # programが"hello world"をプリントするならtrueを返す。そうでなければfalseを返す
end

しかしいくらパースできても、Hello worldの書き方は無限にあるわけです。

…だんだんと、難しいということが見えてきたのではないでしょうか？

prints_hello_world?で数学の難問が解けてしまう

ちょっと飛ばして、では仮にprints_hello_world?関数ができたとしましょう。どんなコードなのかわかりませんが、とにかく出来上がったとします。

しかしこの時、奇妙なことが起こります。これはアンダースタンディングコンピュテーションの中にあった例ですが、ゴールドバッハ予想を証明できる、というものです。

ゴールドバッハ予想とは「すべての2よりも大きな偶数は、2つの素数の和として表すことができる」という命題で、この記事執筆時点(2015年8月)ではまだ誰も証明できていません。コンピュータを使って4から400京までのすべての偶数で成り立つことは確かめられているので、たぶん正しそうですが、偶数は無限にあるので証明には至りません。

これをもじって、「もし、2つの素数の和として表すことができない2よりも大きな偶数が見つかったら、Hello worldを出力する」というプログラムを書くことができます。

require 'prime'

def primes_less_than(n)
  Prime.each(n - 1).entries
end

def sum_of_two_primes?(n)
  primes = primes_less_than(n)
  primes.any? {|a| primes.any? {|b| a + b == n}}
end

n = 4

while sum_of_two_primes?(n)
  n = n + 2
end

puts "Hello, world!"

ゴールドバッハ予想が正しければ、このプログラムは無限ループに入って、永遠にHello worldを出力することはないはずです。

今、print_hello_world?プログラムが手元にあるのでした。print_hello_world?でこのコードを検証し、trueが返ってくればゴールドバッハ予想は外れで、falseが返ってくればゴールドバッハ予想は正しいことになります。

なんということでしょう、print_hello_world?にはどうやら数学の難問を解くほどの能力が内包されているようです。

…そんな馬鹿な。print_hello_world?は決して書けない、というのが真実味を帯びてきました。

どうして不可能なのか

ライスの定理の証明は、プログラムの停止性問題に帰結して解くことができるそうです。Wikipediaには証明が載っていますが、これを見ても納得感にはつながりませんでした。

なので、個人的にどうやってライスの定理を納得したのかについて書きます。

全能のパラドクス

少し話題が変わりますが、全能のパラドクスという問題があります。思考実験的ではありますが、全知全能の神のような存在がいたとして、の話。

「全能者は自分で持ち上げられないほど重い岩を作り出せるか？」

もし、自分で持ち上げられない岩を作り上げることができたなら、その瞬間に「できないこと」が生まれてしまいます。では、そういう岩を作ることができないとすれば、確かに持ち上げられないという事態は起こりませんが、「自分が持ち上げられないほど重い岩を作ることができない」という、これまた「できないこと」が発生します。

どっちになっても「全能」ではなくなる…。パラドクス状態です。

全能のパラドクスを以って「つまり全能なんてあり得ないんだよ！」みたいな思索もできますが、ここで言いたいのはこの全能のパラドクスがライスの定理とよく似ているということです。

自己言及のパラドクス

全能のパラドクスと似ていますが、自己言及のパラドクスも有名です。

「この文は間違っている」

文章をSとしましょう。Sが正しければ、「この文は間違っている」のだから、Sは間違いということになります。ではSが間違いであれば、「この文は間違っていない」のだから、Sは正しいということになります。

どちらに転んでもヘンな状態です。パラドクス状態です。

この状況は、文章が自分自身を参照していることに端を発しています。同じように、「全能性」が全能者自身に対しても適用されると解釈していることから、全能のパラドクスが生まれています。

ライスの定理も同じです。 プログラムでプログラムの性質を証明する という部分に自己言及的な側面があることから生まれています。

それどころか、我々が日々使っているプログラミング言語は常に自己言及する能力を持っています。クワイン（実行すると自分自身のソースコードを出力するプログラム）は、チューリング完全な言語であれば必ず書けるということが知られています。

ライスの定理は、プログラムにできることに限界があることを示していますが、それは何らかの能力が足りないから生まれているものではありません。

何とも皮肉なことに、能力があり過ぎる（自己参照さえできる）がゆえに、できないことが生まれているのです。

不完全な世界の歩き方

ライスの定理は証明されたからこそ定理なのであって、もう覆ることはありません。私たちが日々書いたコードが仕様通りでバグがないプログラムかどうか、自動で判別するようなプログラムは存在しません。

コンピュータはチューリングマシンで理論上の万能性（自己を参照でき、無限をも扱える能力）を獲得するに至りました。むしろこれ以上の能力は望めないとまで言われています。が、そのせいで逆にできないことが存在する状況になってしまったのです。

コンピュータは楽園を追放されたのです。

…んで、冒頭の書籍なんですが。

ここまでが8章の話です。絶望のどんぞこです。でも9章…続きがあるんですよ。

プログラムの性質は証明できない。これは大いなる悟りです。しかし不完全なこの世界で生き抜く方法をもまた、我々は手にしています。というのも、ライスの定理は割と極端なことを言っていて、現実世界ではそこまで行き着かなくても十分だったりするからです。

例えば、完全でないprints_hello_world?なら書けるはずです。限られたプログラムなら確実にtrue/falseを返せるけど、ものによっては例外を吐いて「判定不能」と返ってくる検証プログラム。それこそHelloWorldの冒頭で示したような素朴な文字列比較だって、不完全なprints_hello_world?の一つです。

不完全でも役には立つでしょう。100%は無理でも、当てられる確率を上げることだったらできるでしょう。同じように完全ではないがソフトウェアのバグを見つける仕組みとして、抽象解釈や型システムの話が出てきます。

他にも、万能性を棄てて安全性を選んだプログラミング言語を作れば、そちらではバグがないことを証明しながらソフトウェアを作れるのかもしれません。

ライスの定理に立ち向かう方法は、いっぱいあるわけです。

そんな感じで希望が見えてきたところで、この本は終わります。（ひどいネタバレだ）

まとめ

プログラムはプログラムの性質を証明できない。
これは能力があり過ぎることから生まれる構造であり、皮肉で面白い
でも、できないことがあったってへっちゃらさ
アンダースタンディングコンピュテーション、めっちゃ面白かったのでオススメです。（読み終わるまでだいぶ時間かかったけど）

ところでこの話、最終的にはゲーデルの不完全性定理（完全な理論体系というのは作れない、みたいな話）に行き着くようです。数学は食わず嫌い気味だったのですが、だんだん興味がわいてきました。