停止性問題と不完全性定理
はじめに
はじめまして。記事を開いていただきありがとうございます。
巷では「停止性問題は不完全性定理と深いつながりがある」みたいな主張をよく耳にしますが、その具体的な繋がりまで説明されていることは多くありません。
そこで、この記事では停止性問題が具体的にどう不完全性定理に繋がるのか解説しようと思います。
結論を言ってしまうと、「決定不能なRE集合さえあればそこから直ちに第一不完全性定理が導ける」というだけの話であり、ちょうど手頃な具体例に停止性問題があっただけで別に停止性問題である必然性はありません。
なので、私は停止性問題と不完全性定理には本質的なつながりはないと考えております。
もう少し各用語についても説明します。
停止性問題とは、一般にプログラム及びそのプログラムへの入力を受け取ったときにその実行が停止するのか有限時間で判断できるのかという問題です。
結論を言ってしまうと、できません。
停止性問題は決定不能な問題と呼ばれるコンピュータには有限時間で計算できない問題になっております。
また、第一不完全性定理とは、ある条件を満たす一階述語論理は必ず証明も反証もできない論理式を持つという論理学における基本的な定理です。
不完全性定理周辺の話題はメタ数学の極みといった感じで、何かが成り立つと言ったときそれはどの体系において成り立つのか、その条件はどの体系における条件なのか、などを常に気にする必要があります。
すなわち、常に自分の位置を把握しながら全てを相対的に捉える必要があり、これにはとても鍛錬が必要だと感じています。
(かくいう私も不完全性定理を理解できているとはとても言えません)
しかし、この記事ではそこまでの難しい話はしないのでそういったメタ数学的な混乱はないかと思われるので安心してください。
それでは以下で詳しく説明していきます。
よろしくお願いします。
この記事について
- 前提知識: 論理学の基本的な記号の意味程度
停止性問題について
停止性問題とは、一般にプログラム及びそのプログラムへの入力を受け取ったときにその実行が停止するのか有限時間で判断できるのかという問題です。
これからこの停止性問題をもう少し形式化していきます。
チューリングマシンとは
「プログラム」を数学的に扱うために、「プログラム」と同等な概念としてチューリングマシン(以下TMと呼ぶ)を導入します。
ただし、厳密な定義はここでは与えません。
TMとは直感的には無限に長いテープを持つ機械のことで、有限長の文字列をテープから受け取って、それを一文字ずつ読み込みながらテープを書き換えて行って最終的に有限ステップで一つの文字列を出力します。
TMはとても原始的な機械ですが、本質的な計算能力は現代の(高性能な)コンピュータと代わりません。
自然数を適当に文字列だと思うことで、1つのTMは1つの自然数上の部分関数を与えます。
そこで、次のような定義を与えます。
定義1:(計算可能関数)
自然数上の部分関数
つまり、コンピュータによって有限時間で計算できる関数のことを計算可能であると言います。
万能チューリングマシン
1つのTMは1つのプログラムを表します。+1するTMは+1しかできないし、+2するTMは+2しかできません。
万能TMは、「TM(のコード)」と「そのTMへの入力」と受け取り、そのTMを実際に動かした際の出力を出力とします。
5+1を計算したかったら、+1するTMと5を引数として与えてやれば5+1を計算できます。たしかに万能です。
「TMのコード」と言いましたが、実は各TMには(頑張れば)一意に自然数を割り当てることができ、逆に自然数を貰えば対応するTMを(あれば)完全に復元することもできます。
各TMに割り当てられる自然数のことをTMのコードと言います。
自然数による識別子のことです。
なので、万能TMは一見「TMを引数に取るなんてまるで他のTMと一線を画した上位のTMだ」って感じがしますが、実際はただ自然数を受け取って自然数を返すだけの他と何ら変わらないただのTMです。
停止性問題の定義
問題とはyesかnoを返すようなもののことであり、yesのものをすべて集めた集合と同一視することができます。
すなわち、「ある自然数は素数であるか?」という問題は、素数全体の集合そのものと見なせます。
停止性問題とは、プログラムとその入力を受け取って、その計算は有限時間で停止するか?という問題でした。
すなわち、万能TMを用いて言い直せば、TMのコード
また、有限時間で停止するか、というのはすなわち部分関数
(逆になぜTMが与える自然数上の関数が"部分"関数だったかというと、入力次第では有限ステップで停止しない可能性があったからと言えます)
さっきの問題の定義とも照らし合わせて、停止性問題
定義2:(停止性問題)
次の
停止性問題の計算不可能性
停止性問題
集合
定理3:(停止性問題は決定不能)
停止性問題
Proof: (Sketch)
(
すると、
また、
ゆえに、
これは万能関数の全域拡張
全域拡張が存在するということは、事前に停止性を判断できてしまうということになってしまいます。
(ざっくり言うと)このように不用意な自己適用により本来不動点を持たないはずの関数から不動点を得る論法を対角線論法といいます。
ここまでの話は高橋[1]が個人的に一番わかりやすいです。
TMとか言う謎概念を出さずにNプログラムというとても素晴らしくわかりやすい概念を用いてわかりやすく説明されています。
半決定可能集合
停止性問題は決定不能ですが、実は半決定可能ではあります。
半決定可能な問題とは直感的に言うと、yesであるなら有限時間で停止するが、noである場合は有限時間で停止しない場合があるような問題のことです。
ここでは、同値な概念であるRE集合の定義方法を用いて半決定可能集合を定義します。
定義4:(半決定可能)
停止性問題
半決定可能集合は実は補集合も半決定可能であったら決定可能であることまで言えます。
イメージとしては、元の集合と補集合の両方で判定を同時に走らせておけば、yesだったら元の集合が停止して答えを出すし、noなら補集合が停止して答えを出してくれるので結果としてyesでもnoでも有限時間で決定することが可能となりためです。
定理5:
Proof: (Sketch)
上で書いたことをそのまま形式化するだけ。
半決定可能集合は原始的述語の存在量化で表せるので、
すなわち、
第一不完全性定理について
これより不完全性定理の説明に入ります。
不完全性定理には第一不完全性定理とその証明をPA上で形式化して得られる第二不完全性定理がありますが、ここでは簡単な第一不完全性定理について話します。
第一不完全性定理とは、ある条件を満たす一階述語論理は必ず証明も反証もできない論理式を持つという論理学における基本的な定理でした。
ある条件とは、ここでは詳しくは説明しませんが「ある程度の自然数を扱える」「何が公理か計算可能である」「(
ある程度の自然数と扱えるとは、ロビンソン算術程度を含めばよいです。
何なら
何が公理か計算可能であること(再帰的公理化可能であるといいます)は、可証性述語を
(実は再帰的公理化可能性はRE公理化可能にしても原始再帰的公理化可能にしても変わりません)
第二不完全性定理の証明のためにはこのような流れの証明方法が好ましいのですが、第一不完全性定理の証明だけならもう少し簡単に証明ができます。
以下、算術の言語上の
まず集合の弱表現可能性を定義します。
定義6:(弱表現可能)
すると、次の補題が成り立ちます。
補題7:
Proof: (Sketch)
半決定可能集合の
補題8:
再帰的公理化可能な理論
Proof: (Sketch)
これはとても大変。
以上より以下の補題が得られます。
補題9:
この補題により第一不完全性定理が直ちに従います。
定理10:(ゲーデルの第一不完全性定理)
Proof:
停止性問題
今、
すなわち、次が言える。
つまり、「
後者だとすると、
すなわち前者であることが確定するが、
証明において本質的に使われている停止性問題の性質は、決定不能な半決定可能集合であることのみです。
偶然手頃な位置に停止性問題が転がっていただけで、停止性問題である必然性はありません。
おわりに
毎回低姿勢問題って変換されるのやめてほしい
参考文献
[1]: 高橋正子(1991) 『計算論 計算可能性とラムダ計算』近代科学社
[2]: 田中一之(2022) 『計算理論と数理論理学』共立出版
[3]: 田中一之・鹿島亮・角田法也・菊地誠(1997) 『数学基礎論講義 不完全性定理とその発展』日本評論社
[4]: 菊池誠(2014) 『不完全性定理』共立出版
参考文献の案内
[1]はラムダ計算の日本語書籍のバイブルですが、ラムダ計算なら構文論は岩波の『計算モデルの基礎理論』(井田)、意味論は『プログラム意味論』(横内)の方がわかりやすいです。
Nプログラムという素晴らしい概念を用いて万能関数や停止性問題の話がわかりやすく解説されています。
証明は主に[2]を参考にしました。とても難しい本だと思います。
論理学の本でありながらTMにもとても詳しいです。
[3]は個人的に不完全性定理を学ぶのに最も適していると感じる日本語書籍です。
厳密かつ簡潔でわかりやすいです。しかし、表現可能性のあたりは分かりにくいと感じました。
[4]は日本人として生まれてきたことに感謝させられる不完全性定理の最強の本です。
初学者が躓きやすいポイントが死ぬほど丁寧に解説されており、また本人の思想もとても熱く語られている点も見どころです。
(こういう言い方は怒られるかもしれませんが)数学の哲学に興味がある方も必見です。
Discussion
停止性問題が反決定可能なことがよくわからなかった。万能チューリングマシンが与える関数が↓なn∈Nを集めたものがdom(f)になってくれるんですかね。私の知識不足からΣ1のくだりは分からなかった。反決定可能かつ決定可能な例を他に思い浮かべられなかった。その他、万能チューリングマシンにTMのコードでないようなものを入力としたとき、どのような挙動をするのでしょうか。
コメントありがとうございます!フィードバックをいただけてとても嬉しいです!
正直全体的にこの記事は説明が雑になってしまっているのは自覚しており、いただいた疑問点については真っ当な疑問だと思いますので答えられる範囲で解答させていただきます。
(私自身まだまだ学習中の身であるため、普通に間違えている部分もあるかもしれません。あくまでこれらの説明や記事の説明は現時点の私の理解であることはご理解いただけると嬉しいです!)
まさに仰るとおりです。f(x, y)=\{x\}(y): \mathbb{N}\times\mathbb{N}\rightharpoonup\mathbb{N} (\rightharpoonup は部分関数を表す)が万能TMによって与えられるのでf は計算可能となります。K は\operatorname{dom}(f) と書け確かに半決定可能となります。
関数
そのため、停止性問題
このとき仰るとおりのことが成り立ち、万能TMが与えるTM(が与える関数)\{x\}:\mathbb{N}\rightharpoonup\mathbb{N} が停止しないような引数y\in\mathbb{N} (つまり、\{x\}(y)\uparrow となるy )に対しては(x, y)\not\in K となり、停止するような引数y\in\mathbb{N} に対しては(x, y)\in K となります。
正直これは私の書き方が悪かったと思います。
なんとなく各チューリングマシンをエンコードして自然数が得られるイメージが分かりやすいかと思い記事のような説明をしましたが、実際は(TMは可算無限個しかないため)すべてのTMを(適当な順序を付けて)並べたときの番号を各TMのコードだと考えていただきたいです。
すると、どんな自然数には必ず対応するTMが一意に存在するため、仰られたような疑問は解決されると思います。
(もちろんイメージされているような対応するTMが存在しない場合もあるエンコード方法で考えても問題なく、その場合でも万能TMがただのTMであることを思い出していただけば通常のTMに不当な引数を入力した場合と同じように万能TMが停止しないだけとなります。)
最も代表的な例が停止性問題K ですが、他に分かりやすい例でいうと一階述語論理の証明可能性判定問題や、型無しラムダ計算の\beta 同値性問題(=プログラムの等価性判定問題)等があります。
前者は証明を適当に並べてちっちゃい順から考えていけば、考えている論理式が証明可能であればどっかで停止して証明可能性が分かるし、証明可能でなければ一生止まらず確かに半決定可能となります。\beta 変換で得られる可算無限個のラムダ式のペアについて合流しているペアが見つかるまで探し続けて、見つからなかったら一生止まらず確かに半決定可能となります。
後者に関しては、(型無しラムダ式が合流性が保証されているため)各
ラムダ計算の用語について詳しくなかったら後者の説明は無視してください🙇♂
これは「プログラムの等価性判定は有限時間でできない」というイメージで、例えばあるレガシーなコードをモダンな言語へ厳密にリプレイスすることは理論上不可能であるということが(都合よく解釈すれば)言えることとなります!
このように「あれば止まるし、なければ一生探し続けるようなアルゴリズム」が半決定可能だが決定可能でないアルゴリズムのイメージとなります。
ここに関しては本当に私の説明不足がすべてです。T 上)\Sigma_1 式とは(有界でない)量化が存在量化のみの式(とT 上で同値な式)をさします。\forall x. x=x 等は\Sigma_1 式でなくて\exists x. x=x は\Sigma_1 式となります。\forall があっても、\forall x < t. x + 0 = 0 はx の探索範囲がt 未満と限られているため\Sigma_1 式となります。
(
具体例として、
そのうえで、\Sigma_1 式に関して完全(意味上で正しいものが証明できる)かつ健全(証明できるものは意味上で正しい)ような再帰的公理化可能な理論T を考えたとき、半決定可能性とT 上弱表現可能性が同値になり、記事の最後に載っているような証明が可能となります!
返信ありがとうございます。万能チューリングマシンについて、私から返信を参考に構成しようと思います。自然数を入れて万能TMへのコードを返す計算可能関数の存在は自明ではないと私は考えます。
これよりそのような計算可能関数を構成します。program?(n)という再帰的述語の存在を仮定します。これはnがTMのコードかどうかを判定するような述語です。P:={n∈N:program?(n)}と定義する。これより、計算可能なF:N->Pを定義する
F(0)=μn(program(n)),
F(k+1)=μn((F(k<n)^program?(n))
とすれば各自然数に対し、コードを返せます。これを利用して、万能TMにぶちこめばいいです。
加えて、私が想像していた万能チューリングマシンの挙動は、万能TMによって与えられる部分関数をfとして、F(x,y)=μn(program?(x)*(f(x,y)-n)+¬program?(x)=0)とすれば規定されます。
ご返信ありがとうございます!
まだ目的があまり見えなく、万能チューリングマシンの具体的な表示を得たいということでしょうか?
それなら様々な本に詳細は載っており、異なる計算モデルでもよければ特に『計算論 計算可能性とラムダ計算』(高橋正子)の1章はとても解説が分かりやすいためぜひおすすめしたいです!
正直目的意識のすり合わせが上手くできていない可能性がありますが、ひとまず自分なりに解釈しながら答えさせていただきます!
私の解釈が間違っていた場合はまた返信でご指摘いただけるととても嬉しいです。
まずこのような関数F:\mathbb{N}\rightharpoonup\mathbb{N} を定義する目的は、与えられた自然数に対応するTMが存在せず万能TMが「困る」ことを防ぐために「k 番目のTMのコードを返す関数」としてF を定義しているという認識で大丈夫でしょうか。
しかし、どちらにせよ万能TMが模倣するTM\{x\}:\mathbb{N}\rightharpoonup\mathbb{N} も部分関数であり、定義域外の入力を与えた場合には万能TMは「困る」(=無限ループする)ことになるため、上述の目的の下ではあまりF を定義する意義がないのではないかと感じました。
その上でもう少し仰られていることについて詳しく見ていきたいと思います。
適当なエンコード方法を定めれば、\operatorname{program?}:\mathbb{N}\to\{0, 1\} は確かに再帰的述語として得ることができます。
また、F の定義はもしかすると以下のような定義を意図していますでしょうか?
これなら確かにk 番目のTMのコードを得る全域関数になっており、再帰定理よりこのような定義の妥当性も保証されます。\operatorname{program?}(n) を真にするn がk より大きい自然数の中に必ず見つかる(見つからなかったらTMの数がk 個未満、つまり有限個ということになり矛盾)ため保証されます。
全域性については、
このF を噛ますことで確かに与えられた自然数に対応するTMがないという事態は防ぐことができると思います。
「チューリングマシンの挙動」をどういう意味で使っているかがあまりよくわかりませんでした。
私自身は、各引数と(無限ループも含む)出力の対応リスト、すなわち、TMが与える部分関数のことを「チューリングマシンの挙動」の意味として考えていたため、万能TMの挙動というのは万能TMによって与えられる部分関数それ自体を指しておりました。
だとすると、次のような定義がより正確な定義になるかもしれないです。\operatorname{id}(x)=x に対応するTMのコードをc\in\mathbb{N} としておいて(全域関数だったら何でもよい)、与えられた自然数が対応するTMが存在しなかったら恒等関数に対応するTMのコードを返す関数を\operatorname{check}(x)=\operatorname{program?}(x)*x+(1-\operatorname{program?}(x))*c とすれば、次のように定義できます。
適当に恒等関数
ちなみに、さらに変更して万能チューリングマシンを完全に全域関数まで拡張すると計算不可能になることが対角線論法により言えたりして意外と単純な拡張に見えても慎重にやる必要があったりします。
どこまで質問にお答えできているかは分かりませんが、認識のズレやまだ気になる点があれば私の分かる範囲でお答えします!
私が万能チューリングマシンを構成すると語ったことがいけませんでした。私はプログラム以外を読んだときに万能TMの動作がよくわからない、それが問題でした。私のつくった関数、computeとでも呼びましょう。computeは¬program?(x)のとき、0*(f(x,n)-y)+1=0を満たす最小のyを返しますが、そのようなyは見つかりません。これ以外に関してはあなたの解答で納得しました。とくに私との認識のズレはないと思います。
追記するとすれば、計算可能関数f,gが等価な条件にf↓⇔g↓があるので、私はコードが与えられなかったときの動作を考えたかったのだと思う。 あと正直にいうと万能TMを具体的に構成はしたくないですね、私の直感がこう言う、「おそらく人間のお気持ちを再帰的な言葉に置き換えて、同値性示して、帰納法回してを繰り返すのだろう(小並感)」。