💭

停止性問題と不完全性定理

2023/08/10に公開
5

はじめに

はじめまして。記事を開いていただきありがとうございます。

巷では「停止性問題は不完全性定理と深いつながりがある」みたいな主張をよく耳にしますが、その具体的な繋がりまで説明されていることは多くありません。

そこで、この記事では停止性問題が具体的にどう不完全性定理に繋がるのか解説しようと思います。

結論を言ってしまうと、「決定不能なRE集合さえあればそこから直ちに第一不完全性定理が導ける」というだけの話であり、ちょうど手頃な具体例に停止性問題があっただけで別に停止性問題である必然性はありません。

なので、私は停止性問題と不完全性定理には本質的なつながりはないと考えております。

もう少し各用語についても説明します。
停止性問題とは、一般にプログラム及びそのプログラムへの入力を受け取ったときにその実行が停止するのか有限時間で判断できるのかという問題です。

結論を言ってしまうと、できません
停止性問題は決定不能な問題と呼ばれるコンピュータには有限時間で計算できない問題になっております。

また、第一不完全性定理とは、ある条件を満たす一階述語論理は必ず証明も反証もできない論理式を持つという論理学における基本的な定理です。

不完全性定理周辺の話題はメタ数学の極みといった感じで、何かが成り立つと言ったときそれはどの体系において成り立つのか、その条件はどの体系における条件なのか、などを常に気にする必要があります。

すなわち、常に自分の位置を把握しながら全てを相対的に捉える必要があり、これにはとても鍛錬が必要だと感じています。
(かくいう私も不完全性定理を理解できているとはとても言えません)

しかし、この記事ではそこまでの難しい話はしないのでそういったメタ数学的な混乱はないかと思われるので安心してください。

それでは以下で詳しく説明していきます。
よろしくお願いします。

この記事について

  • 前提知識: 論理学の基本的な記号の意味程度

停止性問題について

停止性問題とは、一般にプログラム及びそのプログラムへの入力を受け取ったときにその実行が停止するのか有限時間で判断できるのかという問題です。

これからこの停止性問題をもう少し形式化していきます。

チューリングマシンとは

「プログラム」を数学的に扱うために、「プログラム」と同等な概念としてチューリングマシン(以下TMと呼ぶ)を導入します。
ただし、厳密な定義はここでは与えません。

TMとは直感的には無限に長いテープを持つ機械のことで、有限長の文字列をテープから受け取って、それを一文字ずつ読み込みながらテープを書き換えて行って最終的に有限ステップで一つの文字列を出力します。

TMはとても原始的な機械ですが、本質的な計算能力は現代の(高性能な)コンピュータと代わりません。
自然数を適当に文字列だと思うことで、1つのTMは1つの自然数上の部分関数を与えます。

そこで、次のような定義を与えます。


定義1:(計算可能関数)

自然数上の部分関数fがあるTMによって与えられるとき、f計算可能であるという


つまり、コンピュータによって有限時間で計算できる関数のことを計算可能であると言います。

万能チューリングマシン

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です。

\{e\}(x)という表記により、万能TMがコードe\in\mathbb{N}のTMを模倣しており、それに入力x\in\mathbb{N}を入れていることを表現します。

停止性問題の定義

問題とはyesかnoを返すようなもののことであり、yesのものをすべて集めた集合と同一視することができます。
すなわち、「ある自然数は素数であるか?」という問題は、素数全体の集合そのものと見なせます。

停止性問題とは、プログラムとその入力を受け取って、その計算は有限時間で停止するか?という問題でした。

すなわち、万能TMを用いて言い直せば、TMのコードe\in\mathbb{N}とそのマシンへの入力x\in\mathbb{N}を受け取って、それが有限時間で停止するか?という問題に言い換えることができます。

また、有限時間で停止するか、というのはすなわち部分関数\{e\}: \mathbb{N}\rightharpoonup\mathbb{N}の定義域\operatorname{dom}(\{e\})xが入っているか?と言いかえることができます。

(逆になぜTMが与える自然数上の関数が"部分"関数だったかというと、入力次第では有限ステップで停止しない可能性があったからと言えます)

さっきの問題の定義とも照らし合わせて、停止性問題K\subseteq\mathbb{N^2}を次のように定義します。


定義2:(停止性問題)

次のK停止性問題という
K = \{(e, x)\in\mathbb{N^2}\ |\ x\in\operatorname{dom}(\{e\})\}


停止性問題の計算不可能性

停止性問題Kは決定不能であることを所謂対角線論法により証明します。
集合X\subseteq\mathbb{N}決定可能(または単に計算可能)であるとは、次の特性関数\chi_X:\mathbb{N}\rightarrow\mathbb{N}が計算可能であることを言います。

\chi_X(x) = \left\{ \begin{array}{ll} 1 & if\ x\in{X} \\ 0 & otherwise \end{array} \right.

定理3:(停止性問題は決定不能)

停止性問題Kは決定不能である

Proof: (Sketch)

Kが決定可能であるとすると、次の全域関数g(e, x): \mathbb{N^2}\rightarrow \mathbb{N}も計算可能である。

\begin{equation*} g(e, x) = \left\{ \begin{array}{ll} \{e\}(x) & if\ (e, x)\in{K} \\ 0 & otherwise \end{array} \right. \end{equation*}

gはTM eに入力xを入れたとき停止するならそれを計算し、停止しないなら0を返す関数。つまりg実行前に停止性を判断する能力を持つ。)

すると、f(x) = g(x, x) + 1も計算可能であるため、このfのコードをaとすると、次のように万能TMでfを模倣することができる。

f(x) = \{a\}(x)

f(x)とはg(x, x)+1のことであり、g全域関数であったため、f(a)は定義されており、f(a) = g(a, a)+1のことである。
また、f(a)=\{a\}(a)なので、gの定義よりf(a) = g(a, a)である。

ゆえに、g(a, a) + 1 = g(a, a)となり矛盾が生じ、Kが決定不能であることが示された。
\square


これは万能関数の全域拡張gが存在すると仮定した点がすべての誤りの原因です。
全域拡張が存在するということは、事前に停止性を判断できてしまうということになってしまいます。

(ざっくり言うと)このように不用意な自己適用により本来不動点を持たないはずの関数から不動点を得る論法を対角線論法といいます。

ここまでの話は高橋[1]が個人的に一番わかりやすいです。
TMとか言う謎概念を出さずにNプログラムというとても素晴らしくわかりやすい概念を用いてわかりやすく説明されています。

半決定可能集合

停止性問題は決定不能ですが、実は半決定可能ではあります。
半決定可能な問題とは直感的に言うと、yesであるなら有限時間で停止するが、noである場合は有限時間で停止しない場合があるような問題のことです。

ここでは、同値な概念であるRE集合の定義方法を用いて半決定可能集合を定義します。


定義4:(半決定可能)

X\subseteq\mathbb{N}半決定可能 \Leftrightarrow_{def} ある計算可能関数fが存在し、X = \operatorname{dom}(f)


停止性問題KK=dom(\{-\}(-))と書くことができるため、\{-\}(-)が(定義より)計算可能であることから直ちに半決定可能であることが従います。

半決定可能集合は実は補集合も半決定可能であったら決定可能であることまで言えます。
イメージとしては、元の集合と補集合の両方で判定を同時に走らせておけば、yesだったら元の集合が停止して答えを出すし、noなら補集合が停止して答えを出してくれるので結果としてyesでもnoでも有限時間で決定することが可能となりためです。


定理5:

X\subseteq\mathbb{N}及び\mathbb{N}-Xが共に半決定可能 \Leftrightarrow Xは決定可能

Proof: (Sketch)

上で書いたことをそのまま形式化するだけ。

半決定可能集合は原始的述語の存在量化で表せるので、X\mathbb{N}-Xを表す述語を\exists{y}. p(x, y)\exists{y}. q(x, y)とすれば、あとはp\lor{q}の最小化\mu_y(p\lor{q})(これは未定義を引き起こさない!)をpに突っ込むだけ。

Xからyesが帰って来れば\mu_y(p\lor{q})からはp(x, y)を真にするようなyが帰ってくるし、\mathbb{N}-Xからnoが返ってくるなら\mu_y(p\lor{q})からはq(x, y)を真にするようなyが返ってくる。
すなわち、X=\{x\ |\ p(x, \mu_y(p(x, y)\lor{q(x, y)}))\}となるため、Xは確かに決定可能。逆は明らか。
\square


第一不完全性定理について

これより不完全性定理の説明に入ります。

不完全性定理には第一不完全性定理とその証明をPA上で形式化して得られる第二不完全性定理がありますが、ここでは簡単な第一不完全性定理について話します。

第一不完全性定理とは、ある条件を満たす一階述語論理は必ず証明も反証もできない論理式を持つという論理学における基本的な定理でした。

ある条件とは、ここでは詳しくは説明しませんが「ある程度の自然数を扱える」「何が公理か計算可能である」「(\omega-)無矛盾である」の3つです。

ある程度の自然数と扱えるとは、ロビンソン算術程度を含めばよいです。
何なら\Sigma_1完全性が成り立つと読み替えてもらっても大丈夫です。

\omega-無矛盾性は第一不完全性定理の証明において本質的ですが、ロッサー述語と呼ばれる人工的な可証性述語を用意することで無矛盾性にまで仮定を弱めることもできます。

何が公理か計算可能であること(再帰的公理化可能であるといいます)は、可証性述語を\Sigma_1述語たらしめるために必要な条件です。
\Sigma_1述語であるがために、\Sigma_1完全性より「T\vdash\phi\Rightarrow \ T\vdash \texttt{Pr}_T(\overline{\lceil\phi\rceil})」が言えて嬉しいわけです。
(実は再帰的公理化可能性はRE公理化可能にしても原始再帰的公理化可能にしても変わりません)

\omega-無矛盾性より逆も言えて、また対角補題を用いることでゲーデル文により第一不完全性定理は証明されます。

第二不完全性定理の証明のためにはこのような流れの証明方法が好ましいのですが、第一不完全性定理の証明だけならもう少し簡単に証明ができます。

以下、算術の言語上の\Sigma_1完全かつ\Sigma_1健全かつ再帰的公理化可能な理論について第一不完全性定理、すなわち証明も反証も不可能な論理式が存在することを証明していきます。

まず集合の弱表現可能性を定義します。
\overline{x}x\in\mathbb{N}の数項を表します。


定義6:(弱表現可能)

X\subseteq\mathbb{N}T弱表現可能 \Leftrightarrow_{def} \exists\phi, \forall{x}\in\mathbb{N}.「x\in{X} \Leftrightarrow T\vdash\phi(\overline{x})


すると、次の補題が成り立ちます。


補題7:

\Sigma_1健全かつ\Sigma_1完全な理論Tにおいて、集合X\subseteq\mathbb{N}は半決定可能ならば弱表現可能である

Proof: (Sketch)

半決定可能集合の\Sigma_1定義可能性を認めれば、\Sigma_1健全性および\Sigma_1完全性より直ちに従う。
\square


\Sigma_1健全性の仮定は実は無矛盾性にまで弱められるらしいのですが、その分証明は複雑になるらしいです。


補題8:

再帰的公理化可能な理論Tにおいて、集合X\subseteq\mathbb{N}は弱表現可能ならば半決定可能である

Proof: (Sketch)

X = \{x\ |\ T\vdash{\phi(\overline{x})}\}が半決定可能であること、すなわち各自然数x\in\mathbb{N}について、\phi(\overline{x})が証明可能であるかを半決定的に判定できることを示せばよい。
これはとても大変。
\square


以上より以下の補題が得られます。


補題9:

\Sigma_1健全かつ\Sigma_1完全で再帰的公理化可能な理論Tにおいて、半決定可能性と弱表現可能性は同値である


この補題により第一不完全性定理が直ちに従います。


定理10:(ゲーデルの第一不完全性定理)

\Sigma_1健全かつ\Sigma_1完全で再帰的公理化可能な理論Tにおいて、証明も反証もできない論理式が存在する。

Proof:

停止性問題Kは半決定可能かつ決定不能な問題である。
今、Kを弱表現する論理式を\phiとすると

\forall{n}\in\mathbb{N}. 「x\in{K}\Leftrightarrow T\vdash\phi(\overline{x})」

Kは決定不能ゆえKの補集合\mathbb{N}-Kは半決定可能ではないため、\mathbb{N}-Kを弱表現する論理式は存在しない。よって、\lnot\phi\mathbb{N}-Kを弱表現しない。

すなわち、次が言える。

\exists{d}\in\mathbb{N}. 「d\in\mathbb{N}-K \not\Leftrightarrow T\vdash{\lnot\phi(\overline{d})}」

つまり、「d\in\mathbb{N}-KかつT\not\vdash{\lnot\phi(\overline{d})}」か「d\in{K}かつT\vdash{\lnot\phi(\overline{d})}」である。

後者だとすると、d\in{K}よりT\vdash{\phi(\overline{d})}が言えて、\Sigma_1健全性(より導かれる無矛盾性)に反する。
すなわち前者であることが確定するが、d\not\in{K}よりT\not\vdash{\phi(\overline{d})}が言えるため、Tは不完全である。
\square


証明において本質的に使われている停止性問題の性質は、決定不能な半決定可能集合であることのみです。

偶然手頃な位置に停止性問題が転がっていただけで、停止性問題である必然性はありません。

おわりに

毎回低姿勢問題って変換されるのやめてほしい

参考文献

[1]: 高橋正子(1991) 『計算論 計算可能性とラムダ計算』近代科学社
[2]: 田中一之(2022) 『計算理論と数理論理学』共立出版
[3]: 田中一之・鹿島亮・角田法也・菊地誠(1997) 『数学基礎論講義 不完全性定理とその発展』日本評論社
[4]: 菊池誠(2014) 『不完全性定理』共立出版

参考文献の案内

[1]はラムダ計算の日本語書籍のバイブルですが、ラムダ計算なら構文論は岩波の『計算モデルの基礎理論』(井田)、意味論は『プログラム意味論』(横内)の方がわかりやすいです。
Nプログラムという素晴らしい概念を用いて万能関数や停止性問題の話がわかりやすく解説されています。

証明は主に[2]を参考にしました。とても難しい本だと思います。
論理学の本でありながらTMにもとても詳しいです。

[3]は個人的に不完全性定理を学ぶのに最も適していると感じる日本語書籍です。
厳密かつ簡潔でわかりやすいです。しかし、表現可能性のあたりは分かりにくいと感じました。

[4]は日本人として生まれてきたことに感謝させられる不完全性定理の最強の本です。
初学者が躓きやすいポイントが死ぬほど丁寧に解説されており、また本人の思想もとても熱く語られている点も見どころです。
(こういう言い方は怒られるかもしれませんが)数学の哲学に興味がある方も必見です。

Discussion

ざいどりっつざいどりっつ

停止性問題が反決定可能なことがよくわからなかった。万能チューリングマシンが与える関数が↓なn∈Nを集めたものがdom(f)になってくれるんですかね。私の知識不足からΣ1のくだりは分からなかった。反決定可能かつ決定可能な例を他に思い浮かべられなかった。その他、万能チューリングマシンにTMのコードでないようなものを入力としたとき、どのような挙動をするのでしょうか。

mineelmineel

コメントありがとうございます!フィードバックをいただけてとても嬉しいです!
正直全体的にこの記事は説明が雑になってしまっているのは自覚しており、いただいた疑問点については真っ当な疑問だと思いますので答えられる範囲で解答させていただきます。
(私自身まだまだ学習中の身であるため、普通に間違えている部分もあるかもしれません。あくまでこれらの説明や記事の説明は現時点の私の理解であることはご理解いただけると嬉しいです!)

停止性問題が反決定可能なことがよくわからなかった。万能チューリングマシンが与える関数が↓なn∈Nを集めたものがdom(f)になってくれるんですかね。

まさに仰るとおりです。
関数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に不当な引数を入力した場合と同じように万能TMが停止しないだけとなります。)

反決定可能かつ決定可能な例を他に思い浮かべられなかった。

最も代表的な例が停止性問題Kですが、他に分かりやすい例でいうと一階述語論理の証明可能性判定問題や、型無しラムダ計算の\beta同値性問題(=プログラムの等価性判定問題)等があります。

前者は証明を適当に並べてちっちゃい順から考えていけば、考えている論理式が証明可能であればどっかで停止して証明可能性が分かるし、証明可能でなければ一生止まらず確かに半決定可能となります。
後者に関しては、(型無しラムダ式が合流性が保証されているため)各\beta変換で得られる可算無限個のラムダ式のペアについて合流しているペアが見つかるまで探し続けて、見つからなかったら一生止まらず確かに半決定可能となります。

ラムダ計算の用語について詳しくなかったら後者の説明は無視してください🙇‍♂
これは「プログラムの等価性判定は有限時間でできない」というイメージで、例えばあるレガシーなコードをモダンな言語へ厳密にリプレイスすることは理論上不可能であるということが(都合よく解釈すれば)言えることとなります!

このように「あれば止まるし、なければ一生探し続けるようなアルゴリズム」が半決定可能だが決定可能でないアルゴリズムのイメージとなります。

私の知識不足からΣ1のくだりは分からなかった。

ここに関しては本当に私の説明不足がすべてです。
(T上)\Sigma_1式とは(有界でない)量化が存在量化のみの式(とT上で同値な式)をさします。
具体例として、\forall x. x=x等は\Sigma_1式でなくて\exists x. x=x\Sigma_1式となります。\forallがあっても、\forall x < t. x + 0 = 0xの探索範囲が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)とすれば規定されます。

mineelmineel

ご返信ありがとうございます!

万能チューリングマシンについて、私から返信を参考に構成しようと思います。

まだ目的があまり見えなく、万能チューリングマシンの具体的な表示を得たいということでしょうか?
それなら様々な本に詳細は載っており、異なる計算モデルでもよければ特に『計算論 計算可能性とラムダ計算』(高橋正子)の1章はとても解説が分かりやすいためぜひおすすめしたいです!

正直目的意識のすり合わせが上手くできていない可能性がありますが、ひとまず自分なりに解釈しながら答えさせていただきます!
私の解釈が間違っていた場合はまた返信でご指摘いただけるととても嬉しいです。

自然数を入れて万能TMへのコードを返す計算可能関数の存在は自明ではないと私は考えます。

まずこのような関数F:\mathbb{N}\rightharpoonup\mathbb{N}を定義する目的は、与えられた自然数に対応するTMが存在せず万能TMが「困る」ことを防ぐために「k番目のTMのコードを返す関数」としてFを定義しているという認識で大丈夫でしょうか。

しかし、どちらにせよ万能TMが模倣するTM \{x\}:\mathbb{N}\rightharpoonup\mathbb{N}も部分関数であり、定義域外の入力を与えた場合には万能TMは「困る」(=無限ループする)ことになるため、上述の目的の下ではあまりFを定義する意義がないのではないかと感じました。

その上でもう少し仰られていることについて詳しく見ていきたいと思います。

これよりそのような計算可能関数を構成します。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にぶちこめばいいです。

適当なエンコード方法を定めれば、\operatorname{program?}:\mathbb{N}\to\{0, 1\}は確かに再帰的述語として得ることができます。

また、Fの定義はもしかすると以下のような定義を意図していますでしょうか?

F(k) = \left\{ \begin{array}{ll} \mu_n(\operatorname{program?}(n)) & \text{if }k=0 \\ \mu_n(F(k-1)<n\land\operatorname{program?}(n)) & \text{otherwise} \end{array} \right.

これなら確かにk番目のTMのコードを得る全域関数になっており、再帰定理よりこのような定義の妥当性も保証されます。
全域性については、\operatorname{program?}(n)を真にするnkより大きい自然数の中に必ず見つかる(見つからなかったらTMの数がk個未満、つまり有限個ということになり矛盾)ため保証されます。

このFを噛ますことで確かに与えられた自然数に対応するTMがないという事態は防ぐことができると思います。

加えて、私が想像していた万能チューリングマシンの挙動は、万能TMによって与えられる部分関数をfとして、F(x,y)=μn(program?(x)*(f(x,y)-n)+¬program?(x)=0)とすれば規定されます。

「チューリングマシンの挙動」をどういう意味で使っているかがあまりよくわかりませんでした。
私自身は、各引数と(無限ループも含む)出力の対応リスト、すなわち、TMが与える部分関数のことを「チューリングマシンの挙動」の意味として考えていたため、万能TMの挙動というのは万能TMによって与えられる部分関数それ自体を指しておりました。

F(x, y)=\mu_n(\operatorname{program?}(x)*(f(x, y)-n)+\lnot\operatorname{program?}(x)=0)とは、もしかすると自然数x\in\mathbb{N}に対応するTMがあればその計算結果を、なければ0を返すという、対応するTMが存在しない自然数が入力されたときの出力を無限ループではなく0に変更した万能TMを意図していますでしょうか?

だとすると、次のような定義がより正確な定義になるかもしれないです。
適当に恒等関数\operatorname{id}(x)=xに対応するTMのコードをc\in\mathbb{N}としておいて(全域関数だったら何でもよい)、与えられた自然数が対応するTMが存在しなかったら恒等関数に対応するTMのコードを返す関数を\operatorname{check}(x)=\operatorname{program?}(x)*x+(1-\operatorname{program?}(x))*cとすれば、次のように定義できます。

F(x, y)=\operatorname{program?}(x)*f(\operatorname{check}(x), y)

ちなみに、さらに変更して万能チューリングマシンを完全に全域関数まで拡張すると計算不可能になることが対角線論法により言えたりして意外と単純な拡張に見えても慎重にやる必要があったりします。

どこまで質問にお答えできているかは分かりませんが、認識のズレやまだ気になる点があれば私の分かる範囲でお答えします!

ざいどりっつざいどりっつ

私が万能チューリングマシンを構成すると語ったことがいけませんでした。私はプログラム以外を読んだときに万能TMの動作がよくわからない、それが問題でした。私のつくった関数、computeとでも呼びましょう。computeは¬program?(x)のとき、0*(f(x,n)-y)+1=0を満たす最小のyを返しますが、そのようなyは見つかりません。これ以外に関してはあなたの解答で納得しました。とくに私との認識のズレはないと思います。
 追記するとすれば、計算可能関数f,gが等価な条件にf↓⇔g↓があるので、私はコードが与えられなかったときの動作を考えたかったのだと思う。 あと正直にいうと万能TMを具体的に構成はしたくないですね、私の直感がこう言う、「おそらく人間のお気持ちを再帰的な言葉に置き換えて、同値性示して、帰納法回してを繰り返すのだろう(小並感)」。