ユーザーブログ:P進大好きbot/変換写像による解析

巨大数界隈では長いこと表記の解析における唯一無二のツールが表解析でした。しかし表解析にはいくつかの問題があります。

1. 有限個の項の対応を正しく書いても、それ単体では停止性や解析の証明にはならない。
2. 第三者の検証が困難なほど十分強い表記と対応させる表を書いてしまえば、仮に全く間違っていたとしても誤りを指摘することが困難となる。

１つ目の問題は、解析の正確性に関わる致命的な問題です。「ペア数列までは自明だから省略」とか「原始数列の限界とペア数列の限界はこう対応するから当然トリオ数列の限界もこう対応する」といったスキップを非常によく見掛けますが、飛ばしたところで誤りがある可能性は十分にあります。また飛ばしていないところでも誤りがあったとして、表には証明等の情報が何もないため、その誤りに第三者が気付くのは至難の業です。

２年ほど前は英語版コミュニティの解析技術が日本コミュニティの遥か先を行くと言われていました。筆者はそれらのコミュニティを知ったばかりだったので「そうなんだ」としか思っていませんでしたが、いざ英語版コミュニティの上位層で常識とされていたOCFの話をすると、どうもおかしなことばかり経験するのです。

――誤った事実が、常識とされている。

日本コミュニティの遥か先を行くと言われていた彼らが参照していたのは証明でも原論文でもなく、根拠のない表や定義のない関数との直感的比較だったのです。証明付きの原論文を引用して解析の誤りを指摘してもまるで信用されない程度には証明より表が絶大な信用を得ていたのは、当時の筆者にとってはなかなかの衝撃でした。

２つ目の問題は、自己解析のI WIN性に関わる致命的な問題です。何か表記を自作して、「これはペア数列より強く、トリオ数列やカルテット数列とこう対応する」と表を書いたとしましょう。ペア数列までの解析が省略されている状況でトリオ数列までBMSを瞬時に解析できる人なんてそうはいないので、第三者がこれを検証するのは困難です。しかもトリオ数列やカルテット数列は十分強いので、表を何万行と充足させつつも「スカスカ」にできるため、パッと分かる矛盾も生じにくいでしょう。

従ってもし第三者が表の矛盾を指摘しようと思ったら、元の表より詳細な解析をする必要があるため時間も労力も作成者より掛ける必要があるという不合理な状況になります。他人の解析の検証に作成者以上に時間を割くくらいなら自分も表記を作って同じように「これはBMSより強い」と主張する方が楽ですので、結果的に界隈全体で解析の検証が行われなくなっていくかもしれません。

これらの問題を解決するためには、より正確で再現可能性の高い解析手段が必要になるわけです。そこで白羽の矢が立つのが「変換（翻訳）写像」です。ここでは変換写像を用いた解析について概略を述べようと思います。

概要

ある表記を解析をする時は、別の表記と比較することになる。つまり、「どの項がどの項に対応するのか」を明らかにする必要がある。従来の表解析は、全ての項に対して対応する項をきちんと書く代わりに、きれいな見た目の項を有限個だけ選んでそれに対応してほしい項を書いているに過ぎない。代わりに、項の対応を全域な写像として定義することで、全ての項に対して対応する項をきちんと書く、という手法が変換写像を用いた解析である。

この説明で完全に理解できた人には後の文章は不要である。以下では変換写像という概念を厳密に定式化し、それを用いると何が出来るかを解説する。

基本列付き表記

基本列付き表記とは、集合\(T\)と写像\([]_T \colon T \times \mathbb{N} \to T\)の組\((T,[]_T)\)のことである。

例1（順序数に伴う基本列付き表記）
可算順序数\(\alpha\)と\(\alpha\)未満の各極限順序数\(\beta\)に対する基本列\(\beta[n]\)が与えられている時、その基本列系が極限順序数でない順序数にも適用可能になるように(1) \(\beta = 0\)ならば\(\beta[n] = 0\)、(2) \(\beta\)が後続順序数\(\beta'+1\)ならば\(\beta[n] = \beta'\)、と拡張したものを\([]_{\alpha} \colon \alpha \times \mathbb{N} \to \alpha\)と置くと、\((\alpha,[]_{\alpha})\)が最も基本的な基本列付き表記の例となる。

例2（順序数表記に伴う基本列付き表記）
拡張ブーフホルツのψ関数に伴う適当な表記を\(BT\)と置き、その標準的な基本列を\([]_{BT} \colon BT \times BT \to BT\)と置く。写像\([]_{BT}' \colon BT \times \mathbb{N} \to BT\)を\(t[n]_{BT}' = t[\underbrace{\psi_0(0) + \cdots + \psi_0(0)}_n]_{BT}\)と定めることで基本列付き表記\((BT,[]_{BT}')\)を得る。（ちなみに加法や\(\psi_0(0)\)の表し方は\(BT\)の定義の仕方に依存するがここでは分かりやすいように\(+\)と\(\psi_0(0)\)そのもので表した。この構成は拡張ブーフホルツのψ関数に限らず基本列が適切に定義された他のOCFでも同様に機能する）

例3（制限）
\((T,[]_T)\)を基本列表記とする。部分集合\(T_0 \subset T\)が\((T,[]_T)\)の制限であるとは、任意の\((t,n) \in T_0 \times \mathbb{N}\)に対し\(t[n] \in T_0\)を満たすということである。この時\([]_{T_0} \colon T_0 \times \mathbb{N} \to T_0\)を\([]_T\)の制限と定めることで、基本列付き表記\((T_0,[]_{T_0})\)を得る。（制限の典型例は、適切な条件付けにより"標準形"とされる項全体のなす部分集合や、ある固定した項に基本列を繰り返し適用して得られる項全体のなす部分集合である）

ハーディ階層や急増加関数階層と同様の関数階層を\((T,[]_T)\)に対して定めることが出来るので、それを\(\textrm{HH}_{T,[]_T}\)や\(\textrm{FGH}_{T,[]_T}\)と置く。\(\textrm{HH}_{T,[]_T}\)や\(\textrm{FGH}_{T,[]_T}\)は全域とも計算可能とも限らない部分関数\(T \times \mathbb{N} \to \mathbb{N}\)である。従ってこれらを用いて計算可能巨大数を定義したい場合は、これらが全域かつ計算可能になるような十分条件を確かめる必要がある。また全域かつ計算可能になるだけでなく、できれば解析も出来ることが望ましい。そのために順序を導入する。

順序

基本列付き表記\((T,[]_T)\)に対し、\(T\)上の二項関係\(s \leq_{T,[]_T} t\)を「ある\(k \in \mathbb{N}\)と\((n_i)_{i=0}^{k-1} \in \mathbb{N}^k\)が存在して\(t[n_0] \cdots [n_{k-1}] = s\)」と定める。ただし\(k = 0\)の時の左辺\(t[n_0] \cdots [n_{k-1}]\)は\(t\)と定める。

\(\leq_{T,[]_T}\)は反射的かつ推移的だが、一般には必ずしも半順序にならない。一方で例1の\((\alpha,[]_{\alpha})\)と例2の\((BT,[]_{BT}')\)を用いて構成される\(\leq_{\alpha,[]_{\alpha}}\)と\(\leq_{BT,[]_{BT}'}\)はそれらの通常の順序と一致するため、整列順序となる。

また\((T,[]_T)\)が再帰的であったとしても\(\leq_{T,[]_T}\)は一般に必ずしも計算可能にすらならないが、例2の\((BT,[]_{BT}')\)を用いて構成される\(\leq_{BT,[]_{BT}'}\)はその通常の順序である辞書式順序と一致するため、計算可能となる。

\(\leq_{T,[]_T}\)の性質を調べることで、\(\textrm{HH}_{T,[]_T}\)や\(\textrm{FGH}_{T,[]_T}\)の様々な性質を導くことが出来る：

命題4（順序の整礎性と関数の停止性の関係）
(1) \(\leq_{T,[]_T}\)が整礎半順序であるならば、\(\leq_{T,[]_T}\)に関する超限帰納法が証明可能であるため\(\textrm{HH}_{T,[]_T}\)や\(\textrm{FGH}_{T,[]_T}\)は全域となる（従って計算可能性や大きさを気にしなければ、これで巨大数を作ることが出来る）
(2) \(\leq_{T,[]_T}\)が整列順序であるならば、\(\leq_{T,[]_T}\)の順序型\(\textrm{Lim}_{T,[]_T}\)が順序数となり、また\(\textrm{Lim}_{T,[]_T}\)と再帰構造の順序型が一致するように\(\textrm{HH}_{T,[]_T}\)や\(\textrm{FGH}_{T,[]_T}\)の限界関数を定義することが出来る。（\(\textrm{Lim}_{T,[]_T}\)はしばしば\((T,[]_T)\)の限界の順序数と呼ばれ、これ自体は\(\textrm{HH}_{T,[]_T}\)や\(\textrm{FGH}_{T,[]_T}\)の限界関数の増大度の情報を持たないが解析の手掛かりを与えることが多い）
(3) \(\leq_{T,[]_T}\)が再帰的整列順序であるならば、\(\textrm{HH}_{T,[]_T}\)や\(\textrm{FGH}_{T,[]_T}\)やそれらの限界関数は全域な計算可能関数となる。（これにより、停止性が担保された計算可能関数であってある程度順序数を用いた解析の手掛かりを持つものを得る）

命題4 (2)により、\(\leq_{T,[]_T}\)の\(\{t' \in T \mid t' \leq t \land t' \neq t\}\)への制限が整列順序であるような各\(t \in T\)に対し、\((T,[]_T)\)の制限\(\{t' \in T \mid t' \leq t \land t' \neq t\}\)の限界の順序数が定義される。これを\(o_{T,[]_T}(t)\)と置き、\((T,[]_T)\)において\(t\)に対応する順序数と呼ぶ。

\((T,[]_T)\)が木であるとは、任意の\(t \in T\)に対し\(\leq_{T,[]_T}\)の\(\{t' \in T \mid t' \leq t \land t' \neq t\}\)への制限が整列順序であるということである。基本列を直接用いた\(o_{T,[]_T}\)の定義から即座に以下が従う：

命題5（木の項に対応する順序数の基本性質）
\((T,[]_T)\)が木であると仮定する。この時、以下が成り立つ：
(1) 任意の\((t,n) \in T \times \mathbb{N}\)に対し、\(o_{T,[]_T}(t)[n] \leq o_{T,[]_T}(t)\)である。
(2) 任意の\(t \in T\)に対し、\(t[n] = t\)を満たす\(n \in \mathbb{N}\)が存在しないならば、\(o_{T,[]_T}(t) = \inf \{\alpha \in \textrm{On} \mid \forall n \in \mathbb{N}, o_{T,[]_T}(t[n]) \in \alpha\}\)である。

特に、命題5において木\((T,[]_T)\)が追加の条件

1. \(t[0] = t\)ならば、任意の\(n \in \mathbb{N}\)に対し\(t[n] = t\)である。
2. \(t[0] = t[1] \neq t\)ならば、任意の\(n \in \mathbb{N}\)に対し\(t[0] = t[n]\)である。

を満たすならば、解析をする上で望ましい性質である

1. \(t[0] = t\)ならば、\(o_{T,[]_T}(t) = 0\)である。
2. \(t[0] = t[1] \neq t\)ならば、\(o_{T,[]_T}(t) = o_{T,[]_T}(t[0]) + 1\)である。
3. \(t[0] \neq t[1]\)ならば、\(o_{T,[]_T}(t) = \sup_{n \in \mathbb{N}} o_{T,[]_T}(t[n])\)である。

が成り立つ。

さて、\(\leq_{T,[]_T}\)の性質を調べるための手段が必要になる。そのために、基本列の整礎性という概念を導入する。

整礎性

\((T,[]_T)\)を基本列付き表記とする。\(t \in T\)が零項であるとは、任意の\(n \in \mathbb{N}\)に対し\(t[n] = 0\)を満たすということである。\((T,[]_T)\)が整礎であるとは、任意の\(t \in T\)と\((n_i)_{i=0}^{\infty} \in \mathbb{N}^{\omega}\)に対しある\(k \in \mathbb{N}\)が存在して\(t[n_0] \cdots [n_{k-1}]\)が零項となるということである。

\(\leq_{T,[]_T}\)に関する広義単調減少無限列は基本列の反復適用で得られる列の部分列となるため、以下が従う：

命題6（基本列の整礎性と順序の整礎性の関係）
\((T,[]_T)\)が整礎であることと\(\leq_{T,[]_T}\)が整礎半順序となることは同値である。特に、\((T,[]_T)\)が木ならば整礎である。

命題4と命題6より、\((T,[]_T)\)から構成される諸々の関数の全域性を示すためには\((T,[]_T)\)の整礎性を示せばよい。そのために変換写像を導入する。

変換写像

\((T_1,[]_{T_1})\)と\((T_2,[]_{T_2})\)を基本列付き表記とし、\(\textrm{Trans}\)を写像\(T_1 \to T_2\)とする。

• \(\textrm{Trans}\)が順序保存写像\((T_1,[]_{T_1}) \to (T_2,[]_{T_2})\)とは、「任意の\((s,t) \in T_1 \times T_1\)に対し、\(s \leq_{T_1,[]_{T_1}} t\)ならば\(\textrm{Trans}(s) \leq_{T_2,[]_{T_2}} \textrm{Trans}(t)\)」を満たすということである。
• \(\textrm{Trans}\)が順序同型\((T_1,[]_{T_1}) \to (T_2,[]_{T_2})\)とは、\(\textrm{Trans}\)が全単射な順序保存写像\((T_1,[]_{T_1}) \to (T_2,[]_{T_2})\)でかつ\(\textrm{Trans}^{-1}\)が順序保存写像\((T_2,[]_{T_2}) \to (T_1,[]_{T_1})\)であるということである。
• \(\textrm{Trans}\)が基本列保存写像\((T_1,[]_{T_1}) \to (T_2,[]_{T_2})\)とは、「任意の\((t,n) \in T_1 \times \mathbb{N}\)に対し、\(\textrm{Trans}(t[n]) = \textrm{Trans}(t)[n]\)」を満たすということである。
• \(\textrm{Trans}\)が基本列同型\((T_1,[]_{T_1}) \to (T_2,[]_{T_2})\)とは、\(\textrm{Trans}\)が全単射な基本列保存写像\((T_1,[]_{T_1}) \to (T_2,[]_{T_2})\)であるということである。

なお順序保存性や順序同型性は基本列付き表記のいずれか一方または両方を半順序集合（より一般に\(2\)項関係付き集合）に変えても同様に定義される。定義から、以下が成り立つ：

命題7（基本列保存性と順序保存性と整礎性の関係）
(1) \(\textrm{Trans}\)が基本列同型ならば、\(\textrm{Trans}\)と\(\textrm{Trans}^{-1}\)は基本列保存写像である。
(2) \(\textrm{Trans}\)が基本列保存写像ならば、\(\textrm{Trans}\)は順序保存写像である。
(3) \(\textrm{Trans}\)が基本列同型ならば、\(\textrm{Trans}\)は順序同型である。
(4) \(\textrm{Trans}\)が単射な順序保存写像でありかつ\((T_2,[]_{T_2})\)が整礎（または木）ならば、\((T_1,[]_{T_1})\)は整礎（または木）であり\(\textrm{Lim}_{T_1,[]_{T_1}} \leq \textrm{Lim}_{T_2,[]_{T_2}}\)である。
(5) \(\textrm{Trans}\)が順序同型でありかつ\((T_1,[]_{T_1})\)が整礎（または木）ならば、\((T_2,[]_{T_2})\)は整礎（または木）であり\(\textrm{Lim}_{T_1,[]_{T_1}} = \textrm{Lim}_{T_2,[]_{T_2}}\)である。

なお命題7 (4)と(5)のうち整礎性と限界の順序数に関する主張は基本列付き表記のいずれか一方または両方を半順序集合に変え基本列付き表記の整礎性や限界の順序数を半順序集合の整礎性や部分整列順序集合の順序型の上限に置き換えたものでも成立する。

命題4 (1)と命題6と命題7 (3)と(5)より、順序数や順序数表記に伴う基本列付き表記の部分表記へ基本列同型を取れさえすれば、自動的に整礎性の証明、各種関数の停止性の証明、表記の限界の順序数の決定が一瞬で終わる。与えられた写像が基本列同型であるか否かは、基本列の定義に現れる場合分け（計算可能なら有限個）に沿って確認するだけなので、比較的容易である。これがハイパー原始数列や段階配列表記の停止性の証明が非常に簡単であった理由である。

一方で、順序同型は必ずしも基本列同型でない。基本列同型でない写像が順序同型であることを示すことは非常に面倒である。これがペア数列の停止性の証明が非常に複雑であった理由である。しばしば英語版では「ペア数列の停止性は自明」だとか「ペア数列とブーフホルツの順序数表記との自明な対応がある」という誤った言説が（筆者がペア数列の停止性を示す前も示した後も）なされることがあるが、それはさすがにペア数列解析エアプである。

実際、ペア数列とブーフホルツの順序数表記の\(D_0 D_{\omega} 0\)（\(\psi_0(\Omega_{\omega})\)相当）未満への制限との間の順序同型は一意であり、それがまるで自明でないことからいかに英語版での表解析が（ペア数列レベルでさえ）当てにならなかったかが分かる。ブーフホルツのψ関数自体が英語版で当時全く理解されておらず、誤った認識に基づいた表解析がなされ、その表解析の読解自体も誤っていたため奇跡的に「限界がBO」という正しく主張がされていただけというオチであった。2回間違えて正しい結論を導く議論は、正しい議論ではない。証明に基づかない表解析がいかに誤りを生みやすいかを表す好例であろう。

では解析をする上で毎回証明が必要だろうか？　それはさすがに厳しいと皆が思うだろう。そこで次に１つの提案をする。

提案

表記の解析手法として、以下の２つを考える：

1. （表による解析）従来通り表解析を行う。
2. （変換写像による解析）変換写像を構成し、それがどのような性質（単射性、全射性、順序保存性、順序同型性、基本列保存性、基本列同型性、etc）を持つかを明示する。

そしてBHOを境に、表記の解析手法を以下のように切り替えることを提案する：

1. 限界の順序数がBHO未満と予測される表記は、表による解析か変換写像による解析のいずれかを行う。もちろん両方を行っても良い。
2. 限界の順序数がBHO以上と予測される表記は、変換写像による解析を行う。もちろん追加で表による解析を行っても良い。

これはただの個人的な提案であって、誰もそれに従う必要はない。そう、何なら筆者も従う必要はないのである……ッ！

ここで重要なことは、いずれの場合も証明を要請していないことである。表による解析を行ったとして、証明されるまではそれが正しい保証はない。同様に変換写像による解析をしたとして、証明されるまではそれが正しい保証はない。つまり解析の負担に証明の負担を上乗せさせないという意図である。従来との大きな違いは、（それまで第三者が検証のために作らざるを得なかった）変換写像を解析者自身が定義するというところである。

証明を解析者本人がしても良いし、予想として誰かに任せるのでも良い。重要なことは、解析が既に証明されたものなのか否かが明確に区別されていることだ。ペア数列はそれが行われていなかったため、停止性が証明される前から「停止性は自明でしょ」という空気がはびこっていた。自分で証明したことや証明を見たことがなくても、表がいっぱいあるから誰かが証明したに違いない、そう思われていたのだろう。残念ながら、これはペア数列だけでなくBM1とBM2についてもそうだった。無限ループが見つかるまでは「停止する」と断言し、無限ループが見つかってからはそのことを忘れて別の表記を「停止する」と断言するのである。これでは新規参入者も混乱して勉強の妨げになるし、将来的に実際に停止性を示そうとしている人たちにも申し訳ない。

というわけで、証明の有無を明確に区別しつつ、とりあえず上の提案のように解析するのはどうであろうか？　「証明がないなら正確性が担保されない状況は変わってないじゃないか」と思うかもしれないが、変換写像が構成されていることは非常に大きい。何故なら、変換写像の性質の誤りは表の誤りと比べて圧倒的に発見しやすいからである。これは表記の強さに関係ないことなので出任せがバレやすく、第三者の限界を超えた自己解析によるI WINもしにくい。また変換写像を作る上で「想定通りにうまく作れないぞ……？」となった場合に、自分の解析の誤りにも気付くことが出来る。

また変換写像が比較的容易に定義できる表記に対しては、表による解析と違って変換写像による解析はさほど日数を要しない。もちろん変換写像の性質の証明をしようと思うと表による解析以上の時間が掛かるだろうが、表による解析の正確性を証明しようと思ったらそれ以上の時間が掛かると思うので、そこは問題ではないだろう。変換写像が容易に定義できない表記に対しては表による解析も非常に煩雑になり、正確さがより疑わしくなるのに検証も難しいという状況となってしまう。従ってやはり変換写像が必要だ。

今後BOレベル以上の表記が増えてくることを考えると、ある程度効率的かつ検証可能な解析手段を採用していくことが望ましい。その目的にも、変換写像による解析は合致しているのではないだろうか？

具体例

変換写像を用いた解析の具体例をここに列挙する：

• ユーザーブログ:P進大好きbot/無理矢印表記観察日記（変換写像\(o\)）
• ユーザーブログ:P進大好きbot/巨界市場の木観察日記（変換写像\(o\)）
• ユーザーブログ:P進大好きbot/ペア数列の停止性（変換写像\(\textrm{Trans}\)）
• （変換写像\(\textrm{Trans}\)）
• ユーザーブログ:P進大好きbot/ヒドヒド観察日記（変換写像\(o\)）

関連項目

変換写像による解析の必要性は英語版でしばしば話題にしていた。

• Evaluation of Analysis: これまでなされた解析たちを「再現可能性」で５段階評価した記事
• New Issue on Traditional Analyses: 従来の表解析の問題点を解説した記事