日記 (2026 年 2 月 12 日)
前回は、 計算可能性に関するトピックとして、 列挙定理と停止性問題の計算不可能性を扱った。
今回は、 別のトピックとして、 Kleene の正規形定理を扱う。
Kleene の正規形定理とは、 どんな計算可能関数でも 「原始再帰関係に 1 回の最小化を施した後に原始再帰関数で最終結果を抽出する」 という形で表せることを主張する定理である。
定義によれば、 計算可能関数とは、 初期関数から始めて合成と原始再帰と最小化を自由に組み合わせて得られるような関数のことだが、 実はその組み合わせ方として 「原始再帰関係→最小化→原始再帰関数」 という形だけで十分だということである。
実は、 この定理の証明の本質的な部分は命題 12.8 ですでに行っている。
そこで、 これを示した第 12 回の内容を思い出すことにしよう。
この回ではまず、 プログラムの Gödel 数 φ と初期メモリの Gödel 数 ρ およびステップ数 n を渡すと、 そのプログラムを n ステップ実行した直後の状況を返す関数 configat を構成した。
すると、 同じ φ と ρ を渡したときに、 プログラムが (もし正常終了するなら) 正常終了するステップ数を返す関数 n∞ は、
n∞(φ,ρ):=μn.configat(φ,ρ,n)@1=len(φ)
と定義できるのだった。
ここで、 このプログラムが部分関数 f:k→ を計算するとすれば、 これは、 関数への引数をレジスタマシンの初期メモリに変換する関数 tomem を使って、
f(x)=configat(φ,tomem(x),n∞(φ,tomem(x)))@0@∗k
と書けるのだった。
この観察をまとめると、 関係 Haltat⊆k+2 を
Haltat(φ,x,n):⟺configat(φ,tomem(x),n)@1=len(e)
で定め、 関数 ext:k+2→ を
ext(φ,x,n):=configat(φ,tomem(x),n)@0@∗k
で定めれば、
f(x)=ext(φ,x,μn.Haltat(φ,x,n))
と書けるということになる。
つまり、 f の値を 「Haltat に最小化を施して ext を適用した結果」 として書けたことになる。
さらに、 ここまでの構成を追えば、 ここに現れている Haltat と ext がともに原始再帰的であることも分かる。
これによって、 計算可能関数を 「原始再帰関係に 1 回の最小化を施した後に原始再帰関数で最終結果を抽出する」 という形で表すという最初に述べた目標は一応達成されたことになる。
ただし、 Kleene の正規形定理はより強く、 外側にある ext を φ にも x にも依存せず最小化の結果だけに依存する形にしても、 上記のように書けることを主張する。
幸いこれは、 Haltat の定義を次のように少し変えて、 最小化をとる変数に (ステップ数だけでなく) メモリの情報を加えておくことで証明できる。
命題 14.1.
次を満たす原始再帰関係 Haltat(k)⊆k+2 が存在する。
任意のプログラム と自然数列 x∈k に対し、 初期のメモリが (x0,⋯,xk−1,0,⋯) である状態から を実行することを考える。
この途中で異常終了しないならば、 自然数 ν に対して以下は同値である。
- Haltat(k)(⌈⌉,x,ν) が成り立つ。
- ある自然数 n が存在して、 n ステップ実行直後のメモリを n と書くことにすると、 n は正常終了している状態であり、 さらに ν@0=n および ν@1=⌈n⌉ も成り立つ。
証明.
これは、
Haltat(φ,x,ν) :⟺ configat(⌈⌉,tomem(x),ν@0)=⟨ν@1,len(φ)⟩
とすれば良い。
実際、 この右辺には原始再帰的な関数や操作しか含まれていないので、 この Haltat は原始再帰的である。
さらに、 命題 12.7 で述べられている configat の性質により、 以下の 2 条件が同値であることが分かる。
- 上記の Haltat について、 Haltat(⌈⌉,x,ν) が成り立つ。
- n:=ν@0 とおいて、 n ステップ実行直後の状況を (n,pn) とすれば、 ⌈n⌉=ν@1 かつ pn=len(⌈⌉) が成り立つ。
この後者の条件にある pn=len(⌈⌉) であるとは、 n ステップ時点で正常終了の状態であるということである。
したがって、 この条件は、 命題の主張の 2 番目の条件と同値である。
これを用いると、 以下の Kleene の正規形定理が証明できる。
定理 14.2 [Kleene の正規形定理 (—’s normal form theorem)].
次を満たす原始再帰関係 Haltat(k)⊆k+2 と原始再帰関数 ext(k):→ が存在する。
任意の計算可能関数 f:k→ に対し、 ある自然数 e∈ が存在して、 任意の自然数列 x∈k に対し、
f(x)=ext(k)(μt.Haltat(k)(e,x,t))
が成り立つ。
証明.
f を計算するプログラムを として、 e:=⌈⌉ と定める。
まず、 命題 14.1 の通りに Haltat をとり、 自然数列 x∈k に対して、
ν∞(e,x):=μt.Haltat(e,x,t)
とおく。
すると命題 14.1 により、 初期のメモリが (x,0,⋯) である状態から を実行したときに、 それが正常終了する最小のステップ数が ν∞(e,x)@0 として得られ、 そのときのメモリの Gödel 数が ν∞(e,x)@1 になる。
したがって、 計算の定義により f(x)=ν∞(e,x)@1@∗k である。
そこで、 関数 ext:→ を
ext(ν):=ν@1@∗k
で定めれば、 これは原始再帰的であり、 さらに
f(x) = ν∞(e,x)@1@∗k = ext(μt.Haltat(e,x,t))
が成り立つ。
Haltat も ext も f には依存していないため、 これらは定理の主張を満たす。
次回からは、 新たに計算可枚挙性という概念を導入し、 その性質を見ていくことにする。
参考文献
- H. B. Enderton (2011) 『Computability Theory』 Academic Press