変換写像による解析

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

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

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

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

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

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

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

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

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

概要[]

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

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

基本列付き表記[]

基本列付き表記とは、

集合\(T\)
写像\([]_T \colon T \times \mathbb{N} \to T\)

の組\((T,[]_T)\)のことである。なお実際にはより抽象的な設定で

集合\(T\)
写像\([]_T \colon T^2 \to T\)
単射な写像\(\ulcorner \cdot \urcorner \colon \mathbb{N} \hookrightarrow T\)
写像\(\textrm{dom} \colon T \to T\)

の４つ組\((T,[]_T,\ulcorner \cdot \urcorner,\textrm{dom})\)を考えることも多く以下の議論はそういった状況にも自然に拡張可能であるが、煩雑さを避けるためにこの記事では前者の流儀のみ扱う。

例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}\)が整礎半順序であるならば、\((T,\leq_{T,[]_T})\)の各全順序部分集合の順序型の上限\(\textrm{Lim}_{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)\)が追加の条件

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

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

\(t[0] = t\)ならば、\(o_{T,[]_T}(t) = 0\)である。
\(t[0] = t[1] \neq t\)ならば、\(o_{T,[]_T}(t) = o_{T,[]_T}(t[0]) + 1\)である。
\(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,R_{T_1})\)と\((T_2,R_{T_2})\)を狭義（等号なし）半順序集合または（等号付き）半順序集合とし、\(\textrm{Trans}\)を写像\(T_1 \to T_2\)とする。

\(\textrm{Trans}\)が順序保存写像\((T_1,R_{T_1}) \to (T_2,R_{T_2})\)とは、「任意の\((s,t) \in T_1 \times T_1\)に対し、\(s R_{T_1} t\)ならば\(\textrm{Trans}(s) R_{T_2} \textrm{Trans}(t)\)」を満たすということである。
\(\textrm{Trans}\)が順序同型\((T_1,R_{T_1}) \to (T_2,R_{T_2})\)とは、\(\textrm{Trans}\)が全単射な順序保存写像\((T_1,R_{T_1}) \to (T_2,R_{T_2})\)でかつ\(\textrm{Trans}^{-1}\)が順序保存写像\((T_2,R_{T_2}) \to (T_1,R_{T_1})\)であるということである。なお\(R_{T_1}\)と\(R_{T_2}\)がいずれも狭義全順序であるかいずれも全順序である場合は、\(\textrm{Trans}^{-1}\)に関する条件は自動的である。

なお（等号なしまたは等号あり）半順序集合の間の写像に関する順序保存性や順序同型性は順序集合のいずれか一方または両方をより一般の\(2\)項関係付き集合に変えても同様に定義される。こういった「何かを保存する写像」はしばしば準同型と呼ばれ、「準同型であってその逆写像も準同型であるもの」はしばしば同型と呼ばれる。

\((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})\)であるとは、\(\textrm{Trans}\)が順序保存写像\((T_1,\leq_{T_1,[]_{T_1}}) \to (T_2,\leq_{T_2,[]_{T_2}})\)であるということである。
\(\textrm{Trans}\)が順序同型\((T_1,[]_{T_1}) \to (T_2,[]_{T_2})\)とは、\(\textrm{Trans}\)が順序同型\((T_1,\leq_{T_1,[]_{T_1}}) \to (T_2,\leq_{T_2,[]_{T_2}})\)であるということである。
\(\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\)項関係付き集合）に変えても同様に定義される。例えば順序同型\((T_1,[]_{T_1}) \to (T_2,\leq_{T_2})\)とは順序同型\((T_1,\leq_{T_1,[]_{T_1}}) \to (T_2,\leq_{T_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)のうち整礎性と限界の順序数に関する主張は基本列付き表記のいずれか一方または両方を半順序集合に変え基本列付き表記の整礎性や限界の順序数を半順序集合の整礎性や部分整列順序集合の順序型の上限に置き換えたものでも成立する。

なお実用上は基本列に付随する順序そのものではなくそれ以外の全順序（辞書式順序など）を比較したい状況も多い。そういった状況で役立つ命題もいくつか紹介する。集合\(T\)上の\(2\)項関係\(R_1\)と\(R_2\)に対し、\(R_1\)が\(R_2\)を含意するとは任意の\((s,t) \in T^2\)に対し\(s R_1 t\)ならば\(s R_2 t\)であるということである。

命題8（全順序が非自明な含意を持たないこと）
(1) \(<_1\)と\(<_2\)を集合\(T\)上の狭義全順序とする。\(<_1\)が\(<_2\)を含意するならば、\(<_1\)と\(<_2\)は等しい。
(2) \(\leq_1\)と\(\leq_2\)を集合\(T\)上の全順序とする。\(\leq_1\)が\(\leq_2\)を含意するならば、\(\leq_1\)と\(\leq_2\)は等しい。

証明

(2)は(1)から即座に従うため、(1)のみ示す。\((s,t) \in T^2\)が\(s <_2 t\)を満たすとする。\(s <_1 t\)となることを示せばよい。そうでないと仮定し矛盾を導く。\(s <_1 t\)でないので、\(<_1\)が狭義全順序であることから\(s = t\)または\(t <_1 s\)である。

\(s = t\)ならば、\(s <_2 t\)であることと\(<_2\)が狭義全順序であることに反し矛盾する。
\(t <_1 s\)ならば、仮定より\(t <_2 s\)となり、\(s <_2 t\)であることと\(<_2\)が狭義全順序であることに反し矛盾する。

以上よりいずれの場合も矛盾するので、\(s <_1 t\)である。

命題8単体で使うことはあまりないが、命題8の応用である次の命題はそこそこ使用しやすいものであろう。

命題9（基本列と辞書式順序の比較手法）
\((T_1,[]_{T_1}\)を基本列付き表記とし、\(\leq_{T_1}\)を\(T_1\)上の全順序とする。\(\leq_{T_1,[]_{T_1}}\)が\(\leq_{T_1}\)を含意しかつある全順序集合\((T_2,\leq_{T_2})\)と順序同型\(\textrm{Trans} \colon (T_1,[]_{T_1}) \to (T_2,\leq_{T_2})\)が存在するならば、\(\leq_{T_1,[]_{T_1}}\)と\(\leq_{T_1}\)は一致する。

証明: \(\textrm{Trans}\)が順序同型であり\(\leq_{T_2}\)が全順序であることから、\(\leq_{T_1,[]_{T_1}}\)は全順序である。以上より命題8より従う。□

命題9は主に、基本列付き表記が整礎であることが変換写像により示された後でその表記が「適切な」標準形に制限した上で別の標準的な順序に関して順序数表記となることを示すために役立つものである。ただし「適切な」標準形を定めることはさほど容易でないことが多い。というのも、再帰的集合の計算可能な基本列を直接使って定義される標準形は再帰的枚挙可能であることがすぐに分かっても再帰的であることは自明でないことが多いからである。一応、そのような標準形でも再帰的であることを保証できる状況があるのでそれを次に紹介する。

命題10（基本列による再帰的枚挙の基本性質）
\(T\)を再帰的集合とし、\([]_T \colon T \times \mathbb{N} \to \mathbb{N}\)を計算可能写像とし、\(\leq_T\)を\(T\)上の計算可能全順序とし、\(\textrm{dom} \colon T \to \{0,1,2\}\)を計算可能写像とし、\(T_0 \subset T\)を有限部分集合とし、各\(n \in \mathbb{N}\)に対し再帰的枚挙可能部分集合\(OT_n \subset T\)を以下のように再帰的に定める：
(i) \(n = 0\)ならば、\(OT_n := T_0\)である。
(ii) \(n \neq 0\)ならば、\(OT_n := \{t[n]_T \mid (t,n) \in OT_{n-1} \times \mathbb{N}\}\)である。
\(T\)の再帰的枚挙可能部分集合\(\bigcup_{n \in \mathbb{N}} OT_n\)を\(OT\)と置く。\(\leq_{T,[]_T}\)が\(\leq_T\)を含意しかつ以下を満たす可算順序数\(\alpha\)と写像\(\textrm{Trans} \colon T \to \alpha\)が存在するならば、\(OT\)は\(T\)の再帰的部分集合である：
(a) \(\textrm{Trans}\)の\(OT\)への制限が全単射\(OT \to \alpha\)である。
(b) \(\textrm{cof}(\textrm{Trans}(a)) = 0\)を満たす任意の\((a,n) \in OT \times \mathbb{N}\)に対し、\(a[n]_T = a\)である。
(c) \(\textrm{cof}(\textrm{Trans}(a)) = 1\)を満たす任意の\((a,n) \in OT \times \mathbb{N}\)に対し、\(\textrm{Trans}(a[n]_T) + 1 = \textrm{Trans}(a)\)である。
(d) \(\textrm{cof}(\textrm{Trans}(a)) = \omega\)を満たす任意の\(a \in OT\)に対し、\((\textrm{Trans}(a[n]_T))_{n \in \mathbb{N}}\)は\(\textrm{Trans}(a)\)の基本列である。
(e) 任意の\(a \in OT\)に対し、\(\textrm{dom}(a) = \min \{\textrm{cof}(\textrm{Trans}(a)),2\}\)である。

証明: バシク行列の標準形判定アルゴリズムを与えることが予想されているふぃっしゅさんのアルゴリズム（通称rpakr法）と同様の手法を用いる。計算可能部分写像

\begin{eqnarray*} \downarrow \colon OT \times T \times \mathbb{N} & \to & \{0,1\} \\ (s,a,n) & \mapsto & \downarrow_s(a,n) \end{eqnarray*}

を以下のように再帰的に定める：

\(a = s\)ならば、\(\downarrow_s(a,n) := 1\)である。
\(a \neq s\)とする。
1. \(s \leq_T a\)ならば、\(\downarrow_s(a,n) := 0\)である。
2. \(s \leq_T a\)でないとする。
  1. \(\textrm{dom}(s) = 0\)ならば、\(\downarrow_s(a,n) := 0\)である。
  2. \(\textrm{dom}(s) \neq 0\)とする。
    1. \(a \leq_T s[n]_T\)を満たすならば、\(\downarrow_s(a,n) := \downarrow_{s[n]_T}(a,0)\)である。
    2. \(a \leq_T s[n]_T\)を満たさないとする。
      1. \(\textrm{dom}(s) = 1\)ならば、\(\downarrow_s(a,n) := 0\)である。
      2. \(\textrm{dom}(s) = 2\)ならば、\(\downarrow_s(a,n) := \downarrow_s(a,n+1)\)である。

条件(a)と(d)より、分岐22222は有限回の反復で分岐2221に移行する。条件(c)と(d)より、分岐2221において

\begin{eqnarray*} \textrm{Trans}(s[n]_T) < \textrm{Trans}(s) \end{eqnarray*}

が成り立つ。従って\(\alpha\)の整礎性から、分岐22222と分岐2221は有限回の反復で分岐1か分岐21か分岐221か分岐22221に移行する。以上より\(\downarrow\)は全域である。

ここで\([]_T\)の定義域と終域をそれぞれ\(OT \times \mathbb{N}\)と\(OT\)に制限したものを\([]_{OT}\)と置く。条件(a),(b),(c),(d)より\(\textrm{Trans}\)の\(OT\)への制限が順序同型\((OT,\leq_{OT,[]_{OT}}) \to (\alpha,\subset)\)である。命題9より\(\leq_{OT,[]_{OT}}\)は\(\leq_T\)の\(OT\)への制限と一致し、特に\(\leq_{OT,[]_{OT}}\)は全順序である。

\(\downarrow\)の計算の条件分岐における\(\leq_T\)を全て\(\leq_{T,[]_T}\)に置き換えて得られる部分写像を\(\downarrow'\)と置く。\(\downarrow\)が全域であることと\(\leq_{OT,[]_{OT}}\)が\(\leq_T\)の\(OT\)への制限と一致することから、\(\downarrow'\)の定義域は\(OT^2 \times \mathbb{N}\)を含み、かつ任意の\((s,a,n) \in OT^2 \times \mathbb{N}\)に対し\(\downarrow_s(a,n) = \downarrow'_s(a,n)\)である。\(\leq_{OT,[]_{OT}}\)が全順序であることから、\(a \neq s\)を満たす任意の\((a,s) \in OT^2\)に対し\(s \leq_{OT,[]_{OT}} a\)でないことと\(a \leq_{OT,[]_{OT}} s\)であることは同値である。

以下、任意の\((s,a) \in OT^2\)に対し\(a \leq_{OT,[]_{OT}} s\)ならば\(\downarrow'_s(a,0) = 1\)であることを示す。

\(\textrm{Trans}\)の\(OT\)への制限が順序同型\((OT,\leq_{OT,[]_{OT}}) \to (\alpha,\subset)\)であるので、\(\textrm{Trans}(a) \leq \textrm{Trans}(s)\)である。\(\downarrow'_s(a,0)\)の再帰式は第\(1\)引数に\([]_T\)を適用するか第\(3\)引数を変更するだけであり、かつ条件(c)と(d)から第\(1\)引数の\(\textrm{Trans}\)での像が\(\textrm{Trans}(a)\)を上回っている限り、再帰式において第\(1\)引数に\([]_T\)を適用した結果の\(\textrm{Trans}\)での像は\(\textrm{Trans}(a)\)以上となる。従って\(\alpha\)の整礎性から\(\downarrow'_s(a,0)\)の計算は最終的に分岐1に達する。すなわち\(\downarrow'_s(a,0) = 1\)である。

以下、任意の\((s,a) \in OT \times T\)に対し、\(a \leq_{T,[]_T} s\)であることと\(\downarrow_s(a,0) = 1\)であることが同値であることを示す。

\(a \leq_{T,[]_T} s\)であるとする。この時\(s \in OT\)より\(a \in OT\)である。従って\(a \leq_{OT,[]_{OT}} s\)であるので、\(\downarrow_s(a,0) = \downarrow'_s(a,0) = 1\)である。

\(\downarrow_s(a,0) = 1\)であるとする。この時\(\downarrow\)の定義から最終的に分岐1を通る必要があるが、\(\downarrow\)の再帰式は第\(1\)引数に\([]_T\)を適用するか第\(3\)引数を変更するだけなので、\(a \leq_{T,[]_T} s\)である。

以上より\(OT = \{a \in T \mid \sum_{s \in S_0} \downarrow_s(a,0) \neq 0\}\)となるので、\(OT\)は\(T\)の再帰的部分集合である。□

なお命題10は現状ではバシク行列に適用可能でない。というのも\(\alpha\)や\(\textrm{Trans}\)の取り方がバシク行列では知られておらず、仮にうまく取れたとしても条件(b)と(c)と(d)は簡単に示せても条件(a)を示すことが極めて困難だからである。例えば単射性は順序数の適当なnormal form表示の一意性に帰着させるのが常套手段である。全射性は困難を伴うことが多いが、例えばユーザーブログ:p進大好きbot/亜原始数列とVeblen関数#停止性の定理（\(OT\)が\(\Lambda\)に対応すること）(2)で用いられた次の手法を参考にして欲しい。

命題11（変換写像の全射性の判定法）
\((T,[]_T)\)を基本列付き表記とし、\(\alpha\)を可算順序数とする。写像\(\textrm{Trans} \colon T \to \alpha\)が以下を満たすならば、\(\textrm{Trans}\)は全射である：
(a) \(\textrm{Trans}\)の像は\(\alpha\)で非有界である。
(b) \(\textrm{cof}(\textrm{Trans}(a)) = 1\)を満たす任意の\(a \in T\)に対し、\(\textrm{Trans}(a[0]_T) + 1 = \textrm{Trans}(a)\)である。
(c) \(\textrm{cof}(\textrm{Trans}(a)) = \omega\)を満たす任意の\(a \in T\)に対し、\((\textrm{Trans}(a[n]_T))_{n \in \mathbb{N}}\)は\(\textrm{Trans}(a)\)の基本列である。

証明

条件(b)と(c)より\(\textrm{Trans}\)は順序保存写像\((T,\leq_{T,[]_T}) \to (\alpha,\in)\)を定める。従って\(\textrm{Trans}\)の像を\(X\)と置く。\(X \neq \alpha\)と仮定して矛盾を導く。

仮定より\(\alpha \setminus X\)は空でないので、\(\alpha\)の整礎性から\(\alpha \setminus X\)の最小元\(\beta\)が存在する。各\(i \in \mathbb{N}\)に対し\(s_i \in T\)を以下のように再帰的に定める：

\(i = 0\)ならば、条件(a)より\(\beta \in \textrm{Trans}(s)\)を満たす\(s\)が存在するので、\(s_i\)をそのような\(s\)の１つとして定める。
\(i \neq 0\)ならば、条件(b)と(c)と\(\beta \notin X\)より\(\{n \in \textrm{cof}(\textrm{Trans}(s_i)) \mid \beta \in s_{i-1}[n]_T\)が空でないので\(n_i\)をその最小値と定め、\(s_i := s_{i-1}[n_i]_T\)と定める。

すると\([]_T\)の反復適用を用いた\((s_i)_{i \in \mathbb{N}}\)の構成と条件(b)と(c)から\((\textrm{Trans}(s_i))_{i \in \mathbb{N}}\)が\(\alpha\)の無限降下列となり、\(\alpha\)の整礎性に反し矛盾する。以上より\(X = \alpha\)である。□

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

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

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

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

提案[]

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

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

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

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

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

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

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

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

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

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

具体例[]

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

ユーザーブログ:P進大好きbot/無理矢印表記観察日記（変換写像\(o\)）
複素数を使った面白い巨大数の解析スレッド（変換写像\(o\)と\(p\)）
ユーザーブログ:P進大好きbot/巨界市場の木観察日記（変換写像\(o\)）
ユーザーブログ:P進大好きbot/ペア数列の停止性（変換写像\(\textrm{Trans}\)）
en:Hyper primitive sequence system#Termination（変換写像\(\textrm{Trans}\)）
ユーザーブログ:P進大好きbot/ヒドヒド観察日記（変換写像\(o\)）
ユーザーブログ:P進大好きbot/亜原始数列とVeblen関数（変換写像\(o_T\)）