13.5 停止確率

13.4 節は機械を一つ取り替え，値を持つプログラムの全体が語頭のない集合になるようにした．その代償として係数 $2$ が入ったが，得たものは大きい．重み $2 - | 𝑠 |$ の総和が $1$ を超えなくなったので，プログラムの全体に確率としての読み方が付いたからである．本節はまず，13.2 節が $𝐾 U$ について示した計算不可能性が $𝐾 V$ でも成り立つことを見て，そこから $V$ の停止の判定不可能性を出す．そのうえで，値を持つプログラム全体の重みを一つの実数にまとめ，その実数もまた計算できないことを示す．

停止問題という語を先に断っておく．プログラムを走らせる前に，それが値を返すかどうかを言い当てる問題のことである．13.2 節はこれに触れなかった．以下で判定できないと述べるのも，13.4 節で固定した $V$ の停止についてだけである．同じ論法は定義 13.1.4 の $U$ についても通るが，本書は $V$ についてだけ書く．

記述長も停止も決められない

定理 13.5.1. 自然数 $𝑥$ に $𝐾 V (𝑥)$ を対応させる関数は計算可能でない．

この主張は命題 13.4.6 からも出る． $𝐾 V (𝑥) = 2 𝐾 U (𝑥) + 1$ だから，一方が計算可能なら他方も計算可能で，定理 13.2.3 を $𝑦 : = 0$ に当てれば矛盾するからである．以下でそうせずに Berry の探索をもう一度書くのは，矛盾を出す段が $V$ の側の不変性，すなわち定理 13.4.7 だけに乗ることを見せるためである．以下の証明も， $𝐾 V (𝑥) \geq 𝑘$ を満たす $𝑥$ があることを言う一段では命題 13.4.6 を経由するが，そこから先に $U$ は現れない．

証明. $𝑥 \mapsto 𝐾 V (𝑥)$ が計算可能だとする．

$𝑘 \in ℕ$ に対し， $𝐾 V (𝑥) \geq 𝑘$ を満たす $𝑥$ のうち最小のものを $𝑔 (𝑘)$ と書く．そのような $𝑥$ があることを見る．系 13.2.2 を $𝑦 : = 0$ に当てると $𝐾 U (𝑥) \geq 𝑘$ を満たす $𝑥$ があり，命題 13.4.6 より $𝐾 V (𝑥) = 2 𝐾 U (𝑥) + 1 \geq 𝑘$ である．よって $𝑔 (𝑘)$ は定まる． $𝑔 (𝑘)$ は， $𝑥 = 0, 1, 2, \dots$ の順に $𝐾 V (𝑥)$ を計算して値が $𝑘$ 以上になる最初の $𝑥$ を返す探索で求まり，この探索は必ず停止する．そこで $M (𝑧, 𝑦) : = 𝑔 (𝑧)$ （第 $2$ 引数は使わない）と定めると，Church–Turing のテーゼより $M$ は計算可能であり，とくに定義 13.1.3 の意味で機械である．

定理 13.4.7 をこの $M$ に当てて定数 $𝑏 \in ℕ$ をとる． $𝑘 \in ℕ$ とし， $𝑠$ を $𝑘$ の二進表示のビット列とすると， $𝑠$ が表す自然数は $𝑘$ だから $M (𝑠, 0) = 𝑔 (𝑘)$ であり， $𝐾 V (𝑔 (𝑘)) \leq 2 | 𝑘 | + 𝑏$ である．いっぽう $𝑔 (𝑘)$ の定め方から $𝑘 \leq 𝐾 V (𝑔 (𝑘))$ である．二つを合わせると，すべての $𝑘 \in ℕ$ について

𝑘 \leq 2 | 𝑘 | + 𝑏

が成り立つ．

これは $𝑘$ を大きくとると破れる． $𝑘 : = 2 𝑏 + 4$ とおくと， $2 𝑏 + 4$ の二進表示は $1$ の後ろに $0$ を $𝑏 + 4$ 個並べたものだから $| 𝑘 | = 𝑏 + 5$ であり，上の不等式は $2 𝑏 + 4 \leq 3 𝑏 + 10$ になる．ところが $𝑏$ についての帰納法より $2 𝑏 \geq 𝑏 + 1$ だから

2 𝑏 + 4 = 16 \cdot 2 𝑏 \geq 16 𝑏 + 16 > 3 𝑏 + 10

である．矛盾した． $◼$

形式化: prefixComplexity_not_computable (ソース)

証明の筋は定理 13.2.3 とまったく同じ Berry の探索で，違いは定理 13.1.7 の代わりに定理 13.4.7 を当てるところだけである．そこで係数 $2$ が入るので，破れる場所を探す不等式が $𝑘 \leq | 𝑘 | + 𝑏$ ではなく $𝑘 \leq 2 | 𝑘 | + 𝑏$ になる．右辺は $𝑘$ の二進表示の桁数の $2$ 倍だから， $𝑘$ が倍になるたびに $2$ しか増えない．係数がいくつであっても，桁数に比例する量が $𝑘$ そのものに追いつくことはないので，同じ矛盾が出る．

次に見るのはビット列を引数にとる対応についての主張である．13.1 節が計算可能と呼んだのは自然数を引数にとる関数だったので，ビット列を自然数に読み替える約束を先に一つ決めておく．

定義 13.5.2（ビット列を引数にとる対応の計算可能性）. ビット列 $𝑠$ に，その先頭へ $1$ を置いた列が表す自然数を対応させる読み替えを考える．ビット列に自然数を対応させる対応が 計算可能 であるとは，自然数を引数にとる計算可能な関数があって，どのビット列 $𝑠$ についても， $𝑠$ の読み替え先を引数にしたその関数の値が，もとの対応が $𝑠$ に与える値に等しいことをいう．

読み替えは単射で，像は $1$ 以上の自然数の全体である．先頭が $1$ のビット列は，定義 13.1.2 より，それが表す自然数の二進表示そのものだからである． $0$ は像に入らないので，定義 13.5.2 は自然数を引数にとる関数の $0$ での値に何も要求していない．次の系 13.5.3 の主張と定理 13.5.8 の証明は，どちらもこの約束のうえにある．

系 13.5.3. ビット列 $𝑠$ に， $V (𝑠)$ が値を持つとき $1$ を，持たないとき $0$ を返す対応は，定義 13.5.2 の意味で計算可能でない．

証明. その対応が計算可能だとする． $𝑥 \in ℕ$ を与えて次の探索を行う．ビット列を長さの短い順に，長さの等しいものは先頭から見て $0$ が先に来る順に一本ずつ並べ，各 $𝑠$ について，仮定した対応で $V (𝑠)$ が値を持つかどうかを調べる．持たなければ次へ進む．持つならば $V$ を $𝑠$ に走らせて値を求め，それが $𝑥$ に等しければ $| 𝑠 |$ を返し，等しくなければ次へ進む．

命題 13.4.5 より $V (𝑠) = 𝑥$ を満たす $𝑠$ があるから，この探索は必ず停止する．並べ方が長さの短い順だから，返る値は $V (𝑠) = 𝑥$ を満たす $𝑠$ の長さの最小，すなわち $𝐾 V (𝑥)$ である．値を持つと分かったプログラムだけを走らせているので，途中で止まらなくなることもない．よって $𝑥 \mapsto 𝐾 V (𝑥)$ は計算の手続きで書き下せて，Church–Turing のテーゼより計算可能である．これは定理 13.5.1 に反する． $◼$

形式化: prefixUniversalEval_dom_not_computablePred (ソース)

形式化上の注記. 本文は系 13.5.3 を定理 13.5.1 の対偶として出したが，形式化は二つを独立に示す．定理 13.5.1 に紐付けた宣言は，本文と同じ Berry の探索による．系 13.5.3 に紐付けた宣言のほうは，そちらを取り込んだうえで使わずに，Mathlib のもつ部分計算可能関数の番号づけについての停止問題に帰着させて示されている．保証しているのは主張の正しさであって，紙の証明手順の一致ではない．

紐付けた宣言がビット列に使う読み替えも，定義 13.5.2 が固定したものではなく，Mathlib がもつビット列の標準の符号化である．二つは互いに計算可能に移り合うので，計算可能かどうかという主張としては同じものになるが，その移り合いを述べる宣言は無い．

系 13.5.3 が停止問題と呼ばれるものの， $V$ についての形である． $V$ に渡すプログラムについては，走らせる前に止まるかどうかを言い当てる手続きが無い．証明が使ったのは一手だけで，止まるかどうかが前もって分かるなら，短いプログラムから順に全部試して最短のものを見つけられる，というものである．逆に言えば， $𝐾 V$ を求める手続きが無い理由は，短いプログラムを試し尽くせないところにある．走らせてみて止まらないとき，それが「まだ止まっていない」のか「永久に止まらない」のかが区別できない．

停止確率

定義 13.5.4（停止確率）.

Ω : = \sum 𝑠 : V (𝑠) が値を持つ 2 - | 𝑠 |

と定め（ $𝑠$ は $V$ が値を持つビット列の全体をわたる．可算個の和は 13.4 節で置いた約束のとおり，有限部分和の上限として読む）， $V$ の 停止確率 と呼ぶ．

形式化: chaitinOmega (ソース)

第3章 3.1 節と 3.4 節は，確率空間の点の集合を $Ω$ と書いている．本章の $Ω$ はそれとは別のもので， $V$ について定まる一つの実数である．どちらも引数をとらないので，章をまたいで読むときは気をつけたい．この記号は Chaitin が導入したもので，記号そのものがこの量の名前として通っているため，本書では書き換えずに使う．

命題 13.5.5. $0 < Ω \leq 1$ である．

証明. 上から抑える． $V$ が値を持つビット列の全体は，命題 13.4.4 より空列を含まない語頭のない集合である．よって補題 13.4.2 より $Ω \leq 1$ である．

下から抑える．命題 13.4.5 を $𝑥 : = 0$ に当てると $V (𝑠) = 0$ を満たすビット列 $𝑠$ がある．定義 13.5.4 の和はこの $𝑠$ の項を含み，項はどれも非負だから， $Ω \geq 2 - | 𝑠 | > 0$ である． $◼$

形式化: 下からの評価 chaitinOmega_pos，上からの評価 chaitinOmega_le_one (ソース)

$Ω$ の読み方は定義 13.4.8 の $𝑃 V$ と同じである．でたらめに投げたビット列を $V$ に読ませるとき， $𝑃 V (𝑥)$ が「値が $𝑥$ になる重み」だったのに対し， $Ω$ は「何であれ値が返る重み」である．命題 13.5.5 はこれが $0$ と $1$ のあいだにあることを言っているので，確率と呼んでよい．両端はもっと狭められる．例 13.5.9 が $1 / 4 \leq Ω \leq 1 / 2$ を与える．

計算可能な実数

$Ω$ が計算できるかどうかを問うには，実数について計算可能であるとは何かを決めなければならない．13.1 節で計算可能と呼んだのは自然数を引数にとる関数のことだったから，そのままでは実数に当てられないからである．決め方は素朴で，どんな精度を指定されてもその精度まで近い値を返す手続きがあることをいう．

定義 13.5.6（計算可能な実数）. $𝑟$ を $0$ 以上の実数とする． $𝑟$ が 計算可能 であるとは，自然数を値にとる計算可能な数列 $𝑎 0, 𝑎 1, \dots$ があって，すべての $𝑛 \in ℕ$ について

𝑎 𝑛 2 - 𝑛 \leq 𝑟 + 2 - 𝑛 かつ 𝑟 \leq 𝑎 𝑛 2 - 𝑛 + 2 - 𝑛

が成り立つことをいう．

形式化: IsComputableENNReal (ソース)

二つの不等式を合わせると， $𝑎 𝑛 2 - 𝑛$ と $𝑟$ の差が $2 - 𝑛$ 以下だと言っている．すなわち $𝑎 𝑛$ は $𝑟$ を $2 - 𝑛$ の刻みで測った目盛りの読みであり， $𝑛$ を大きくすれば刻みはいくらでも細かくなる．この形をとった理由は二つある．一つは，近づける列を自然数の列にできることである．刻みの幅 $2 - 𝑛$ は $𝑛$ で決まってしまうので，動くのは目盛りの読みだけであり，有理数の列を持ち出さずに済む．有理数の列で定めるなら，先に有理数の上での計算可能性を定めなければならない．もう一つは，差を引き算で書かずに，どちらの向きも足し算の形にしてあることである．有理数の計算可能な列で定める流儀もあり，そちらの列からは丸めを一段はさんでこの形の列が得られるが，本書はそれを示さない．その一段は形式化もされていない．

道具をもう一つ借りる．予算つきの実行（Kleene の標準形定理）と呼ぶ．計算の手続きで書き下せる部分関数と自然数 $𝑡$ に対し，その部分関数を与えられた引数に手数の予算 $𝑡$ で走らせた結果が定まり，結果は値を持たないか一つの自然数を返すかのどちらかである．借りるのは次の三つである．

予算 $𝑡$ と引数から結果を求める対応は計算可能である．
$𝑡 \leq 𝑡'$ のとき，予算 $𝑡$ で値 $𝑣$ が返るなら予算 $𝑡'$ でも $𝑣$ が返る．
その部分関数がその引数で値 $𝑣$ を持つことと，ある予算 $𝑡$ で結果が $𝑣$ になることとは同値である．

当てる先は定義 13.4.3 の $V$ で，使うのは補題 13.5.7 の $Ω 𝑡$ の定め方とその証明，および定理 13.5.8 の証明である．本書はこれを証明しない．計算モデルを一つ選ばなければ「手数」そのものが定まらず，そこは 13.1 節で借りた枠組みの外にあるからである．

形式化上の注記. 本書が証明しないのは計算モデルの選び方に関わるからであって，形式化が及んでいないからではない．いま挙げた三つは，当てる先である $V$ について，どれも仮定なしに機械検証されている．第 $1$ の性質が prefixEvaln_primrec，第 $2$ が prefixEvaln_mono，第 $3$ が prefixEvaln_complete (InformationTheory/Shannon/Kolmogorov/OmegaNoncomputable.lean) である．形式化は Mathlib がもつ計算モデルを一つ選んでいるので，そこでは「手数」が定まる．第 $1$ の宣言が述べているのは，本文が借りた計算可能性より強い，原始再帰的であることである．

補題 13.5.7（下からの近似）. $𝑡 \in ℕ$ に対し

Ω 𝑡 : = \sum 2 - | 𝑠 |

と定める（和は，長さが $𝑡$ 以下で， $V$ が予算 $𝑡$ で値を返すビット列 $𝑠$ の全体をわたる）．このとき次の三つが成り立つ．第 $1$ に， $2 𝑡 Ω 𝑡$ は自然数であり， $𝑡 \mapsto 2 𝑡 Ω 𝑡$ は計算可能な数列である．第 $2$ に， $Ω 𝑡$ は $𝑡$ について単調非減少である．第 $3$ に， $Ω 𝑡$ の $𝑡$ にわたる上限は $Ω$ に等しい．

証明.

和がわたる集合は，長さ $𝑡$ 以下のビット列の全体という有限集合の部分集合だから有限である．その元 $𝑠$ は $| 𝑠 | \leq 𝑡$ を満たすので $2 𝑡 2 - | 𝑠 | = 2 𝑡 - | 𝑠 |$ は自然数であり， $2 𝑡 Ω 𝑡$ はそれらの有限個の和だから自然数である．計算可能であることを見る．長さ $𝑡$ 以下のビット列を並べる手続きは有限回の繰り返しで書け，各々について予算 $𝑡$ で値が返るかどうかは予算つきの実行の第 $1$ の性質より計算可能に決まり，返るものについて $2 𝑡 - | 𝑠 |$ を足す手続きも有限回で終わる．よって全体は必ず停止する手続きで書き下せて，Church–Turing のテーゼより計算可能である．
$𝑡 \leq 𝑡'$ とする．長さが $𝑡$ 以下なら長さは $𝑡'$ 以下であり，予算つきの実行の第 $2$ の性質より，予算 $𝑡$ で値が返るなら予算 $𝑡'$ でも返る．よって $Ω 𝑡'$ の和がわたる集合は $Ω 𝑡$ のそれを含み，項が非負だから $Ω 𝑡 \leq Ω 𝑡'$ である．
まず $Ω 𝑡 \leq Ω$ を見る．予算つきの実行の第 $3$ の性質より，予算 $𝑡$ で値が返るビット列では $V$ は値を持つ．よって $Ω 𝑡$ は定義 13.5.4 の和の有限部分和であり，和を有限部分和の上限として定めたことから $Ω 𝑡 \leq Ω$ である．逆向きを見る． $V$ が値を持つビット列からなる有限集合 $𝐹$ をとると，同じ性質より，各 $𝑠 \in 𝐹$ にある予算 $𝑡 𝑠$ があって値が返る． $𝐹$ は有限だから， $𝑡 𝑠$ と $| 𝑠 |$ を $𝑠 \in 𝐹$ の全体にわたって超える自然数 $𝑡 *$ がとれる．第 $2$ の主張と同じ理由で $𝐹$ の元はどれも予算 $𝑡 *$ で値が返り，長さも $𝑡 *$ 以下だから， $𝐹$ は $Ω 𝑡 *$ の和がわたる集合に含まれる．項が非負だから $\sum 𝑠 \in 𝐹 2 - | 𝑠 | \leq Ω 𝑡 *$ である． $Ω$ はこれら有限部分和の上限だから， $Ω$ は $Ω 𝑡$ の上限以下である．二つを合わせて，上限は $Ω$ に等しい．

$◻$

形式化: $Ω 𝑡$ にあたる omegaApprox，その分子 omegaApproxNum，分子に $2 - 𝑡$ を掛けたものが $Ω 𝑡$ に等しいこと omegaApprox_eq_num，分子の計算可能性 omegaApproxNum_computable，単調性 omegaApprox_mono，上限 iSup_omegaApprox (ソース)

$Ω 𝑡$ は $Ω$ を下から近づける．予算を増やせば止まるプログラムが見つかっていくので値は増えるいっぽうで，どこまでも増やせば $Ω$ に届く．ところが，いま $Ω 𝑡$ が $Ω$ にどれだけ近いかは，これだけでは分からない．まだ見つかっていない停止するプログラムがどれだけの重みを持つかを言う手立てが無いからである．次の定理が示すのは，その手立ては手続きとしては存在しないということである．

定理 13.5.8（停止確率は計算可能でない）. $Ω$ は定義 13.5.6 の意味で計算可能でない．

証明の要点は一つだけである． $Ω$ を上からも近づけられるなら，「あとどれだけの重みが残っているか」が分かり，残りが $2 - 𝑛$ を切った段から先では，長さ $𝑛$ のプログラムがもう止まらないと言い切れる．下からの近似 $Ω 𝑡$ は補題 13.5.7 のとおり手続きで求まるので，上からも近づけられると停止が判定できてしまう．

証明. 命題 13.5.5 より $Ω$ は $0$ 以上だから定義 13.5.6 を当てられる． $Ω$ が計算可能だとし，その定義の数列 $𝑎 0, 𝑎 1, \dots$ をとる．

各 $𝑛 \in ℕ$ について，条件

𝑎 𝑛 + 2 2 - (𝑛 + 2) \leq Ω 𝑡 + 2 - (𝑛 + 1)

を満たす $𝑡$ を探す．そのような $𝑡$ があることを見る．補題 13.5.7 の第 $3$ の主張より $Ω 𝑡$ の上限は $Ω$ であり， $2 - (𝑛 + 2)$ は正だから， $Ω - 2 - (𝑛 + 2) < Ω 𝑡$ を満たす $𝑡$ がある．定義 13.5.6 の第 $1$ の不等式を $𝑛 + 2$ に当てると $𝑎 𝑛 + 2 2 - (𝑛 + 2) \leq Ω + 2 - (𝑛 + 2)$ だから，この $𝑡$ について

𝑎 𝑛 + 2 2 - (𝑛 + 2) \leq Ω + 2 - (𝑛 + 2) < Ω 𝑡 + 2 - (𝑛 + 2) + 2 - (𝑛 + 2) = Ω 𝑡 + 2 - (𝑛 + 1)

である．

探索が手続きになることを見る．条件の両辺に $2 𝑡 + 𝑛 + 2$ を掛けると

𝑎 𝑛 + 2 2 𝑡 \leq (2 𝑡 Ω 𝑡) 2 𝑛 + 2 + 2 𝑡 + 1

となり，補題 13.5.7 の第 $1$ の主張よりこれは自然数どうしの比較である． $𝑎$ は計算可能な数列だから， $𝑛$ と $𝑡$ から両辺を求めて比べる手続きは有限回の計算で終わる．いま見たとおり条件を満たす $𝑡$ はあるので， $𝑛$ を与えて条件を満たす最小の $𝑡$ を返す探索は必ず停止し，Church–Turing のテーゼよりこの対応は計算可能である．その値を $𝑡 𝑛$ と書く．

$𝑡 𝑛$ での近さを見る．定義 13.5.6 の第 $2$ の不等式を $𝑛 + 2$ に当てると $Ω \leq 𝑎 𝑛 + 2 2 - (𝑛 + 2) + 2 - (𝑛 + 2)$ であり， $𝑡 𝑛$ が条件を満たすことと合わせて

Ω \leq Ω 𝑡 𝑛 + 2 - (𝑛 + 1) + 2 - (𝑛 + 2) < Ω 𝑡 𝑛 + 2 - 𝑛

である（右側は $2 - (𝑛 + 1) + 2 - (𝑛 + 2) = 3 \cdot 2 - (𝑛 + 2) < 4 \cdot 2 - (𝑛 + 2) = 2 - 𝑛$ による）．

停止を判定する．ビット列 $𝑠$ をとり， $𝑛 : = | 𝑠 |$ と置く． $V (𝑠)$ が値を持つことと， $V$ を $𝑠$ に予算 $𝑡 𝑛$ で走らせて値が返ることは同値である．一方の向きは予算つきの実行の第 $3$ の性質から出る．逆を示す． $V (𝑠)$ が値を持ち，予算 $𝑡 𝑛$ では値が返らないとすると， $𝑠$ は $Ω 𝑡 𝑛$ の和がわたる集合に属さない．いっぽうその集合の元も $𝑠$ も，どれも $V$ が値を持つビット列だから，その集合に $𝑠$ を足したものは定義 13.5.4 の和の有限部分和を与え，

Ω 𝑡 𝑛 + 2 - 𝑛 \leq Ω

である．これは直前に得た不等式に反する．

矛盾を出す．いま見たことから，ビット列 $𝑠$ に対して $V (𝑠)$ が値を持つかどうかは， $𝑡 | 𝑠 |$ を求めてから予算 $𝑡 | 𝑠 |$ で $V$ を走らせれば決まる． $𝑛 \mapsto 𝑡 𝑛$ は計算可能で，予算つきの実行の第 $1$ の性質より結果を求める対応も計算可能だから，この判定は必ず停止する手続きで書き下せて，Church–Turing のテーゼより計算可能である．これは系 13.5.3 に反する． $◼$

形式化: chaitinOmega_not_computable (ソース)

したがって，計算できないのは $Ω$ の値そのものというより，近似の誤差のほうである．

例 13.5.9（停止確率の両側からの見積もり）. $1 / 4 \leq Ω \leq 1 / 2$ である．

証明. 下から抑える．先頭のビットが $0$ であるビット列 $𝑑$ をとる．定義 13.1.4 より $U (𝑑, 0)$ は $𝑑$ の先頭の $0$ より後ろのビット列が表す自然数だから，そのような $𝑑$ ではつねに値を持つ． $𝑠 𝑑$ を $𝑑$ の自己限定形（定義 13.4.3）とすると， $𝑠 𝑑$ の先頭から最初の $0$ までの $1$ の個数は $| 𝑑 |$ ，その後ろは $𝑑$ だから，定義 13.4.3 より $V (𝑠 𝑑) = U (𝑑, 0)$ であり，とくに $V (𝑠 𝑑)$ は値を持つ．その長さは $| 𝑠 𝑑 | = 2 | 𝑑 | + 1$ である．また $𝑠 𝑑$ の最初の $0$ より後ろが $𝑑$ だから， $𝑑 \neq 𝑑'$ なら $𝑠 𝑑 \neq 𝑠 𝑑'$ である．

長さごとに数える． $𝑗 \geq 0$ とすると，先頭が $0$ で長さが $𝑗 + 1$ のビット列は，後ろの $𝑗$ ビットの選び方だけあるから $2 𝑗$ 本であり，そのそれぞれについて $| 𝑠 𝑑 | = 2 (𝑗 + 1) + 1 = 2 𝑗 + 3$ である．

$𝐽 \geq 0$ を任意にとる．いま数えたビット列のうち $| 𝑑 | \leq 𝐽 + 1$ にあたる $𝑠 𝑑$ は相異なる有限個で，どれも $V$ が値を持つから，それらの重みの和は定義 13.5.4 の和の有限部分和である．その値は

𝐽 \sum 𝑗 = 0 2 𝑗 2 - (2 𝑗 + 3) = 𝐽 \sum 𝑗 = 0 2 - 𝑗 - 3 = 14 (1 - 2 - (𝐽 + 1))

である．和を有限部分和の上限として定めたことから $Ω$ はこの値以上であり， $𝐽$ を大きくすると右辺は $1 / 4$ に近づくから， $Ω \geq 1 / 4$ である．

上から抑える．まず， $V$ が値を持つビット列の先頭のビットはつねに $1$ である．命題 13.4.4 よりそのようなビット列 $𝑠$ はあるビット列 $𝑑$ の自己限定形であり， $𝑑$ が空列だとすると $𝑠$ は $0$ の一文字で， $V (𝑠) = U (𝑑, 0)$ は定義 13.1.4 より値を持たないからである．よって $| 𝑑 | \geq 1$ であり， $𝑠$ は $1$ で始まって，その長さは $| 𝑠 | = 2 | 𝑑 | + 1 \geq 3$ である．

$V$ が値を持つビット列 $𝑠$ に，その先頭の $1$ を落とした列 $𝑠 -$ を対応させる． $𝑠$ は先頭に $1$ を戻せば $𝑠 -$ から決まるから，この対応は単射であり， $| 𝑠 - | = | 𝑠 | - 1 \geq 2$ である． $𝑠 -$ の全体は空列を含まない語頭のない集合である．空列を含まないことは長さが $2$ 以上であることによる．また $V$ が値を持つ二つのビット列 $𝑠$ と $𝑠'$ について $𝑠 -$ が $(𝑠') -$ の語頭なら，先頭に $1$ を戻した $𝑠$ は $𝑠'$ の語頭であり，命題 13.4.4 より $V$ が値を持つビット列の全体は語頭のない集合だから $𝑠 = 𝑠'$ となり，したがって $𝑠 - = (𝑠') -$ である．

$V$ が値を持つビット列の有限個の集まりを $𝐹$ とすると，いま見たことと補題 13.4.2 から

\sum 𝑠 \in 𝐹 2 - | 𝑠 | = 12 \sum 𝑠 \in 𝐹 2 - | 𝑠 - | \leq 12

である．和を有限部分和の上限として定めたことから $Ω \leq 1 / 2$ である． $◼$

形式化上の注記. 例 13.5.9 の二つの値にあたる宣言はどちらも無い．下からの評価が使った一段，すなわち $V$ が値を持つビット列の有限個の集まりについて重みの和が $Ω$ 以下であることは sum_le_chaitinOmega (InformationTheory/Shannon/Kolmogorov/OmegaNoncomputable.lean) として形式化されているが，具体的な数を下界として与える宣言は無い．命題 13.5.5 に紐付けた $0 < Ω$ の証明も，この一段を $𝑥 = 0$ を出す一本のプログラムに当てたところで止めている．上からの評価についても，形式化が持つのは命題 13.5.5 に紐付けた $Ω \leq 1$ までである．

下からの評価が使ったのは，先頭のビットが $0$ であるビット列では $U$ がつねに値を持つという定義 13.1.4 の一事だけである．そのようなビット列は長さごとに倍々に増え，その自己限定形はどれも $V$ で止まるので，それだけで $Ω$ の $1 / 4$ は埋まる．上からの評価が使ったのは，値を持つプログラムがどれも $1$ で始まるという一事だけで，それだけで命題 13.5.5 の $1$ が半分になる．定理 13.5.8 が言っているのは，こうして両側から挟んでいく作業に終わりが見えないということであって，個々の見積もりができないということではない．実際補題 13.5.7 の $Ω 𝑡$ は，予算 $𝑡$ を与えれば有限の計算で求まる．

$Ω$ が出るのは本節までである．次節が測るのは一つの自然数についての記述の長さで， $V$ が値を持つプログラムの全体にわたる重みは相手にしない．次節は $𝐾 V$ に戻り，記述を二つの部分に分ける見方を入れる．対象そのものを直に書き下すかわりに，まず対象を含む有限集合を書き，次にその中での位置を書く．前半が対象の型を，後半が型の中でのばらつきを担うという分け方で，第12章の型による二段符号と同じ考えを，分布を持たない一つの対象に当てたものである．

InformationTheory — 形式化検証つき情報理論教科書（レビュー版）．数式は MathJax + AMS Euler で事前レンダリング．