「ESSSver.10」

甘露東風さんのESSSver.10に類するものを項書き換え形式で定式化し直す試みです。

構造

// 構造という概念をあらかじめ定義します。まずはざっくりした定義です。文字列の処理をしやすいように入念にカッコで囲っています。

\(0\)と\(1\)と\(+\)と\(\times\)と\((\)と\()\)と\(\langle\)と\(\rangle\)と\([\)と\(]\)のみからなる文字列が「構造」であるという性質を、以下のように再帰的に定める：

1. \(0\)と\(\langle 0 \rangle\)は構造である。
2. 構造\(X\)と\(Y\)に対し、文字列\(X + Y\)は構造である。
3. 構造\(X\)と\(Y\)に対し、文字列\((X) \times (Y)\)は構造である。
4. 構造\(X\)と\(Y\)と\(Z\)に対し、文字列\((X)[Y](Z)\)は構造である。

// この書き方でも大体通じると思いますが、逆にどんな文字列が構造でないのかやや曖昧な表現なので↓のように集合の言葉で定式化するとより確実です。

/＊

\(0\)と\(1\)と\(+\)と\(\times\)と\((\)と\()\)と\(\langle\)と\(\rangle\)と\([\)と\(]\)のみからなる文字列の集合\(S\)を以下を満たす最小の集合と定める：

1. \(0, \langle 0 \rangle \in S\)である。
2. いかなる\(X,Y \in S\)に対しても、\(X + Y \in S\)である。
3. いかなる\(X,Y \in S\)に対しても、\((X) \times (Y) \in S\)である。
4. いかなる\(X,Y,Z \in S\)に対しても、\((X)[Y](Z) \in S\)である。

\(S\)に属する文字列を「構造」と呼ぶ。

＊/

// どちらも同じことです。どれくらい曖昧さを排除するかの好みの問題ですね。ちなみに\(0\)と\(1\)と\(+\)と\(\times\)と\((\)と\()\)と\(\langle\)と\(\rangle\)と\([\)と\(]\)のみからなる文字が構造か否かは再帰的な手段で判定することが出来ます。

自然数のコード化

// 構造に使える自然数を\(0\)と\(1\)だけにしたので、代わりに自然数をコード化します。構造に自然数を入れなかった理由はこちらを参照して下さい。

自然数\(i\)に対し、構造\(a_i\)を以下のように再帰的に定める：

1. \(i = 0\)ならば、\(a_i\)は構造\(0\)である。
2. \(i > 0\)ならば、\(a_i\)は構造\(a_{i-1}+1\)である。

// 例えば\(a_3\)は構造\(0+1+1+1\)ですね。

表記

// 実際に巨大数の計算に用いる表記を「項」と呼ぶことにします。

自然数と\(\{\)と\(\}\)と\(+\)と\(\times\)と\((\)と\()\)と\(\langle\)と\(\rangle\)と\([\)と\(]\)のみからなる文字列が「項」であるという性質を、以下のように再帰的に定める：

1. いかなる自然数\(n\)に対しても\(a_n\)は項である。
2. いかなる正整数\(m\)と項\(N\)と構造\(X\)に対しても、文字列\((a_m) \{ N \} X\)は項である。

// この書き方で大体通じると思いますが、逆にどんな文字列が項でないのかやや曖昧な表現なので↓のように集合の言葉で定式化するとより確実です。

/＊

自然数と\(\{\)と\(\}\)と\(+\)と\(\times\)と\((\)と\()\)と\(\langle\)と\(\rangle\)と\([\)と\(]\)のみからなる文字列の集合\(T\)を以下を満たす最小の集合と定める：

1. いかなる自然数\(n\)に対しても、\(a_n \in T\)である。
2. いかなる正整数\(m\)と\(N \in T\)と構造\(X\)に対しても、\((a_m) \{ N \} (X) \in T\)である。

\(T\)に属する文字列を「項」と呼ぶ。

＊/

// どちらも同じことです。どれくらい曖昧さを排除するかの好みの問題ですね。ちなみに自然数と\(\{\)と\(\}\)と\(+\)と\(\times\)と\((\)と\()\)と\(\langle\)と\(\rangle\)と\([\)と\(]\)のみからなる文字列が項か否かは再帰的な手段で判定することが出来ます。

項書き換え

ここでは項\(N\)と\(N'\)に対して\(N = N'\)と書いたら\(N\)を\(N'\)に書き換える項書き換えを表す。ただし項書き換えは部分文字列への適用を許さない。また自然数\(n\)と構造\(A\)と\(B\)に対して\(A \mapsto_n B\)と書いたら項書き換え\((a_1) \{ a_n \} (A) = (a_1) \{ a_n \} (B)\)を表す。

// \(A \mapsto_n B\)はあくまで\((a_1) \{ a_n \} (A) = (a_1) \{ a_n \} (B)\)の略記（いわゆる糖衣構文）ですので、\((a_1) \{ a_n \} ((A)[\langle 0 \rangle](\langle 0 \rangle)) = (a_1) \{ a_n \} ((B)[\langle 0 \rangle](\langle 0 \rangle))\)のような項書き換えを自動的に許すわけではないことに注意して下さい。

\(n\)と\(m\)を自然数とし、\(N\)と\(N'\)を項とし、\(A\)と\(B\)と\(X\)と\(Y\)と\(Z\)を構造とする。項の書き換え規則が「許容される」という性質を以下のように再帰的に定める：

1. \((a_1) \{ a_n \} (0) = a_{n+1}\)は許容される。
2. \((a_{m+1}) \{ N \} (A) = (a_1) \{ (a_m) \{ N \} (A) \} (A)\)は許容される。
3. \((a_1) \{ a_n \} (A+1) = (a_n) \{ a_n \} (A)\)は許容される。
4. \(\langle 0 \rangle \mapsto_n a_n\)は許容される。
5. \(X+0 \mapsto_n X\)は許容される。
6. \((X) \times (0) \mapsto_n 0\)は許容される。
7. \((X) \times (a_1) \mapsto_n X\)は許容される。
8. \((X) \times (Y+1) \mapsto_n ((X) \times (Y)) + X\)は許容される。
9. \((X)[Y](0) \mapsto_n a_1\)は許容される。
10. \((X)[Y](a_1) \mapsto_n X\)は許容される。
11. \((X)[0](Y+1) \mapsto_n ((X)[0](Y)) \times (X)\)は許容される。
12. \((X)[Y+1](Z+1) \mapsto_n (X)[Y]((X)[Y+1](Z))\)は許容される。
13. \(N = N'\)が許容されるならば、\((a_m) \{ N \} (A) = (a_m) \{ N' \} (A)\)は許容される。
14. \(A \mapsto_n B\)が許容されるならば、\(X + A \mapsto_n X + B\)は許容される。
15. \(A \mapsto_n B\)が許容されるならば、\((X) \times (A) \mapsto_n (X) \times (B)\)は許容される。
16. \(A \mapsto_n B\)が許容されるならば、\((X)[A](Z) \mapsto_n (X)[B](Z)\)は許容される。
17. \(A \mapsto_n B\)が許容されるならば、\((X)[0](A) \mapsto_n (X)[0](B)\)は許容される。
18. \(A \mapsto_n B\)が許容されるならば、\((X)[Y+1](A) \mapsto_n (X)[Y+1](B)\)は許容される。

// 項や構造と同様に、集合の言葉できちんと書くことももちろん可能です。

巨大数

項\(N\)に対し自然数\(f(N)\)を、許容される項書き換えのみを用いて\(N\)を\(a_i\)に書き換えることができる（実は一意な）自然数\(i\)として定める。定義からは明らかではないが、たぶん\(f\)は項全体で定義される計算可能関数である。

自然数\(f((a_1) \{ a_3 \}((\langle 0 \rangle)[(\langle 0 \rangle)[(\langle 0 \rangle)[\langle 0 \rangle](\langle 0 \rangle)](\langle 0 \rangle)](\langle 0 \rangle)))\)を「数ver.10」と名付ける。名称に「」は含める。

解析

\(f((a_1) \{ a_n \} ((\langle 0 \rangle)[a_2](\langle 0 \rangle)))\)はWainer階層における\(f_{\varepsilon_0}(n)\)と一致する。\(i > 2\)に対して\(f((a_1) \{ a_n \} ((\langle 0 \rangle)[a_i](\langle 0 \rangle)))\)はWainer階層の基本列に高々\(f_{\omega}\)程度の変更を加えた基本列系に関する\(f_{\varepsilon_0}(n)\)で近似できるので、\(n\)が十分大きい時はWainer階層の延長における\(f_{\varepsilon_0+1}(n)\)で上から抑えられる。

\([]\)を入れ子にすることは、FGHにおいては\(\varepsilon_0\)の基本列に高々\(f_{\varepsilon_0+1}\)程度の変更を加えるものであるので、十分大きな\(n\)に対しては恐らく \begin{eqnarray*} f((a_1) \{ a_n \} (\underbrace{(\langle 0 \rangle)[ \cdots (\langle 0 \rangle)[}_n \langle 0 \rangle](\langle 0 \rangle) \cdots](\langle 0 \rangle))) < f_{\varepsilon_0 + 2}(n) \end{eqnarray*} となる。