\(\newcommand{\e}{\varepsilon} \newcommand{\a}{\alpha} \newcommand{\w}{\omega} \newcommand{\*}{×}\) \(\e\)関数の定義ができたのですが、流石にあれを読んで\(\e\)関数を理解しろというのは無理があるので、

なるべく分かりやすく解説するということに挑戦してみたいと思います。

一度に書き切るのは無理があるので、不定期に更新する形をとらせていただきます。

ただし、

  1. あくまでも\(\e\)関数の解説であって、実際に書いた定義の解説ではないこと
  2. 不正確な部分が含まれる可能性があること
  3. 分かりやすい解説であることを保証するものではないこと

以上の点を踏まえた上で読んでいただけると助かります。

なお、不正確な部分や気になるところは、コメントかTwitterに質問してください。

もしくは下記のリンクにある\(\e\)関数の定義を読んで補完して下さい。(本末転倒)

定義

\(\e\)関数の定義のリンク

これを読むだけで十分理解できる、という方はむしろ理解の妨げになる可能性がございますので、ここから先は読まないことをお勧めします。


解説について

厳密な定義は上記にあるため、分かりやすさを優先して解説します。

それに伴い、口調も砕けたものにさせていただきます。


定義ずらし

定義ずらしそのものに厳密な定義はまだ与えられておらず、まだ概念に近い存在です。

これがなくても\(\e\)関数を解説することはできるけど、定義ずらしという概念を使った方が個人的に解説しやすいので使うことにします。


まず、定義を変数に持つ関数を考える。(I WIN!)

ここでいう定義とは\(\e([X])\)のこと。(ちなみに\(\e(0)\)はメタ定義)

そのような関数のうち、

  1. 定義を出力する関数
  2. 出力された定義の受け皿になる関数

の二つの関数を考える。

\(\e\)関数の定義において、前者は\(\e(0)\)が最も近く、後者は\(E(x)\)が最も近い

定義ずらしとは、「定義を出力する関数」によって出力された定義を、「定義の受け皿になる関数」に代入することを指す概念である。

何か勘違いされている気がするのですが、定義ずらしの本質は大きい基数(っぽいもの)を生成することではありません

それはあくまでも副産物で、定義ずらしの主目的は変数として自由に扱える定義を生成することです。

厳密性のかけらもないが我慢して欲しい。

なおこれ以降、\(r×(1)\)を\(r\)と、\(1+1+...+1 (1がn個)\)を\(n\)と省略する。

定義の加法

\(\e\)関数では、定義ずらしに加え、定義の加法というものを使っています。(さらにI WIN!)

簡単に言うと、ある定義\(R∈RT\)と、ある単項の定義\(r∈PRT\)に対し、

\(E(R+r)\)を「順序数\(E(R)\)を定義\(r\)で拡張する」ことを表すことにします。(すごくI WIN!)

拡張とは何か、については後で説明します。

\(\e\)関数は、

  1. 定義を出力
  2. 定義ずらし
  3. 拡張
  4. 出力された定義と拡張からより強い定義を出力

を繰り返すことで成長していきます。(I WIN!の極み)


やっと解説

\(E(\e(0)×(Z))=A_Z, A_1=A\)と略記する。


\(1〜EE_A(A)\)まで

まず、定義ずらしをするには最初の定義を用意してやる必要があるので、

\(EE_A(\a)\)を、\(EE_A(0)=\w\)とした加法ベースのOCFに伴う順序数表記として定めます。(以後OCF)

(\(EE_A(A)=EE_A(EE_A(EE_A(...)))\)になる。)


\(EE_A(A+E(\e([A])))\)まで

\(EE_A(A)\)が出てきたので、ここで定義ずらしが起こります。

すなわち、\(EE_{E(\e([A]))}(\a)\)は、\(EE_{E(\e([A]))}(0)=\w\)とした加法ベースのOCFになります。

ここで気をつけて欲しいのは、\(EE_{E(\e([A]))}(\a)\)内においては、定義ずらしはリセットされるという点です。

つまり、

\(EE_A(A)\)

\(EE_A(A+1)\)

\(EE_A(A+2)\)

\(EE_A(A+EE_{E(\e([A]))}(0))\)

\(EE_A(A+EE_{E(\e([A]))}(0)+EE_{E(\e([A]))}(0))\)

\(EE_A(A+EE_{E(\e([A]))}(1))\)

\(EE_A(A+EE_{E(\e([A]))}(2))\)

\(EE_A(A+EE_{E(\e([A]))}(EE_A(0)))\)

\(EE_A(A+EE_{E(\e([A]))}(EE_A(0)+EE_A(0)))\)

\(EE_A(A+EE_{E(\e([A]))}(EE_A(1)))\)

\(EE_A(A+EE_{E(\e([A]))}(EE_A(2)))\)

\(EE_A(A+EE_{E(\e([A]))}(EE_A(EE_A(0))))\)

\(EE_A(A+EE_{E(\e([A]))}(A))\)

\(EE_A(A+EE_{E(\e([A]))}(A+1))\)

\(EE_A(A+EE_{E(\e([A]))}(A+EE_{E(\e([A]))}(0)))\)

\(EE_A(A+EE_{E(\e([A]))}(A+EE_{E(\e([A]))}(A)))\)

\(EE_A(A+EE_{E(\e([A]))}(A+EE_{E(\e([A]))}(A+EE_{E(\e([A]))}(0))))\)

\(EE_A(A+E(\e([A])))\)

のようになります。

なお定義ずらしのリセットは、\(EE_{X+A}(\a), EE_{E(R)}(\a)\)でのみ起こります。


\(EE_A(A+E(\e([A])×(2)))\)まで

次に、\(E(\e([A]))\)を、\(\e([A])\)で拡張する、ということを行います。

\(\e([A])\)の定義は、「加法ベースOCF」なので、

\(EE_{E(\e([A])×(2))}(\a)\)は、\(EE_{E(\e([A]))}(0)=E(\e([A]))+E(\e([A]))+...\)とした加法ベースのOCFになります。

つまり、

\(EE_A(A+E(\e([A])))\)

\(EE_A(A+E(\e([A]))+E(\e([A])))\)

\(EE_A(A+E(\e([A]))+E(\e([A]))+E(\e([A])))\)

\(EE_A(A+EE_{E(\e([A])×(2))}(0))\)

\(EE_A(A+EE_{E(\e([A])×(2))}(0)+EE_{E(\e([A])×(2))}(0))\)

\(EE_A(A+EE_{E(\e([A])×(2))}(1))\)

\(EE_A(A+EE_{E(\e([A])×(2))}(A))\)

\(EE_A(A+EE_{E(\e([A])×(2))}(A+E(\e([A]))))\)

\(EE_A(A+EE_{E(\e([A])×(2))}(A+EE_{E(\e([A])×(2))}(0)))\)

\(EE_A(A+E(\e([A])×(2)))\)

のようになります。


\(EE_A(A+A)\)まで

以降同様に\(E(\e([A])×(\a))\)を、\(\e([A])\)で拡張する、ということを繰り返します。

そして、\(E(\e([A])×(\a))\)から、より強い定義を作ります。

\(EE_{A+A}(\a)\)を、\(EE_{A+A}(0)\)を\(\a=E(\e([A])×(\a))\)の最初の不動点とした\(E(\e([A])×(\a))\)ベースのOCFとして定めます。

つまり、

\(EE_A(A+E(\e([A])×(1)))\)

\(EE_A(A+E(\e([A])×(E(\e([A])×(1)))))\)

\(EE_A(A+EE_{A+A}(0))\)

\(EE_A(A+EE_{A+A}(0)+EE_{A+A}(0))\)

\(EE_A(A+EE_{E(\e([A])×(EE_{A+A}(0)+1))}(0))\)

\(EE_A(A+EE_{E(\e([A])×(EE_{A+A}(0)+1))}(0)+EE_{E(\e([A])×(EE_{A+A}(0)+1))}(0))\)

\(EE_A(A+EE_{E(\e([A])×(EE_{A+A}(0)+1))}(1))\)

\(EE_A(A+EE_{E(\e([A])×(EE_{A+A}(0)+1))}(A))\)

\(EE_A(A+EE_{E(\e([A])×(EE_{A+A}(0)+1))}(A+EE_{E(\e([A])×(EE_{A+A}(0)+1))}(0)))\)

\(EE_A(A+E(\e([A])×(EE_{A+A}(0)+1)))\)

\(EE_A(A+E(\e([A])×(E(\e([A])×(EE_{A+A}(0)+1)))))\)

\(EE_A(A+EE_{A+A}(1))\)

\(EE_A(A+EE_{A+A}(A))\)

\(EE_A(A+EE_{A+A}(A+EE_{A+A}(0)))\)

\(EE_A(A+A)\)

のようになります。


\(EE_A(A+A+E(\e([A+A]))\)まで

\(EE_A(A+A)\)が出てきたので、ここで定義ずらしが起こります。

すなわち、\(EE_{E(\e([A+A]))}(\a)\)は、\(EE_{E(\e([A+A]))}(0)\)を\(\a=E(\e([A])×(\a))\)の最初の不動点とした\(E(\e([A])×(\a))\)ベースのOCFになります。

つまり、

\(EE_A(A+A+E(\e([A])×(1)))\)

\(EE_A(A+A+E(\e([A])×(E(\e([A])×(1))))\)

\(EE_A(A+A+EE_{E(\e([A+A]))}(0))\)

\(EE_A(A+A+EE_{E(\e([A+A]))}(0))\)

\(EE_A(A+A+E(\e([A])×(EE_{E(\e([A+A]))}(0)+1)))\)

\(EE_A(A+A+E(\e([A])×(E(\e([A])×(EE_{E(\e([A+A]))}(0)+1)))))\)

\(EE_A(A+A+EE_{E(\e([A+A]))}(1))\)

\(EE_A(A+A+EE_{E(\e([A+A]))}(A+A))\)

\(EE_A(A+A+EE_{E(\e([A+A]))}(A+A+EE_{E(\e([A+A]))}(A+A)))\)

\(EE_A(A+A+E(\e([A+A]))\)

のようになります。


\(EE_A(A+A+E(\e([A+A])\*(2))\)まで

同様に、\(E(\e([A+A]))\)を、\(\e([A])\)で拡張する、ということを行います。

つまり、\(EE_{E(\e([A+A])+\e([A]))}(\a)\)は、\(EE_{E(\e([A+A])+\e([A]))}(0)=E(\e([A+A]))+E(\e([A+A]))+...\)とした加法ベースのOCFになります。

\(\e([A])\)による拡張を繰り返すことで、\(E(\e([A+A])+\e([A])\*(\a))\)を定義できます。

\(\e([A])\)と同様に、\(E(\e([A+A]))\)を、\(\e([A+A])\)を使って拡張します。

すなわち、\(EE_{E(\e([A+A])\*(2))}(\a)\)は、\(EE_{E(\e([A+A])\*(2))}(0)\)を\(\a=E(\e([A+A])+\e([A])×(\a))\)の最初の不動点とした\(E(\e([A+A])+\e([A])×(\a))\)ベースのOCFになります。

つまり、

\(EE_A(A+A+E(\e([A+A])+\e([A])×(1))\)

\(EE_A(A+A+E(\e([A+A])+\e([A])×(E(\e([A+A])+\e([A])×(1))))\)

\(EE_A(A+A+EE_{E(\e([A+A])\*(2))}(0))\)

\(EE_A(A+A+EE_{E(\e([A+A])\*(2))}(0)+EE_{E(\e([A+A])\*(2))}(0))\)

\(EE_A(A+A+EE_{E(\e([A+A])+\e([A])×(EE_{E(\e([A+A])\*(2))}(0)+1))}(0))\)

\(EE_A(A+A+EE_{E(\e([A+A])+\e([A])×(EE_{E(\e([A+A])\*(2))}(0)+1))}(0)+EE_{E(\e([A+A])+\e([A])×(EE_{E(\e([A+A])\*(2))}(0)+1))}(0))\)

\(EE_A(A+A+EE_{E(\e([A+A])+\e([A])×(EE_{E(\e([A+A])\*(2))}(0)+1))}(1))\)

\(EE_A(A+A+EE_{E(\e([A+A])+\e([A])×(EE_{E(\e([A+A])\*(2))}(0)+1))}(A+A))\)

\(EE_A(A+A+E(\e([A+A])+\e([A])×(EE_{E(\e([A+A])\*(2))}(0)+1))\)

\(EE_A(A+A+E(\e([A+A])+\e([A])×(E(\e([A+A])+\e([A])×(EE_{E(\e([A+A])\*(2))}(0)+1)))\)

\(EE_A(A+A+EE_{E(\e([A+A])\*(2))}(1))\)

\(EE_A(A+A+EE_{E(\e([A+A])\*(2))}(A+A))\)

\(EE_A(A+A+E(\e([A+A])\*(2))\)

のようになります。


\(EE_A(A+A+A)\)まで

\(EE_{A+A}(\a)\)と同様に\(EE_{A+A+A}(\a)\)を定義します。

すなわち、\(EE_{A+A+A}(\a)\)を、\(EE_{A+A+A}(0)\)を\(\a=E(\e([A+A])×(\a))\)の最初の不動点とした\(E(\e([A+A])×(\a))\)ベースのOCFとして定めます。

つまり、

\(EE_A(A+A+E(\e([A+A])×(1))\)

\(EE_A(A+A+E(\e([A+A])×(E(\e([A+A])×(1)))\)

\(EE_A(A+A+EE_{A+A+A}(0))\)

\(EE_A(A+A+EE_{A+A+A}(0)+EE_{A+A+A}(0))\)

\(EE_A(A+A+EE_{E(\e([A+A])×(EE_{A+A+A}(0))+\e([A]))}(0))\)

\(EE_A(A+A+E(\e([A+A])×(EE_{A+A+A}(0))+\e([A])))\)

\(EE_A(A+A+E(\e([A+A])×(EE_{A+A+A}(0)+1)))\)

\(EE_A(A+A+E(\e([A+A])×(E(\e([A+A])×(EE_{A+A+A}(0)+1)))))\)

\(EE_A(A+A+EE_{A+A+A}(1))\)

\(EE_A(A+A+EE_{A+A+A}(A+A))\)

\(EE_A(A+A+A)\)

のようになります。

\(EE_A(X+A)\)及び、\(\e([X+A])\)は同様に定義されます。


\(EE_A(EE_{E(\e(0)+\e([A]))}(1))\)まで

さて、ここからが\(\e\)関数の本領発揮?です。

\(A\)を\(\e([A])\)で拡張します。

すなわち、\(EE_{E(\e(0)+\e([A]))}(\a)\)は、\(EE_{E(\e(0)+\e([A]))}(0)=A+A+...\)とした加法ベースのOCFになります。

そして、\(A\)以上の全ての加法で閉じている\(X\)は定義ずらしの対象になります。

なので\(\e([EE_{E(\e(0)+\e([A]))}(0)])\)も定義されます。

実は\(\e([X])=\e([X'+A])\)の形にならない\(\e([X])\)の定義は簡単で、

\(EE_{E(\e([X]))}(\a)\)は、\( EE_{E(\e([X]))}(0)[n]=E(\e([X[n]]))\)とした加法ベースのOCFになります。

ただし、\(E(\e([X[n]]))\)を\(EE_A(X)[n]\)とみなして\(X[n]\)を展開します。

さて、\(\e([EE_{E(\e(0)+\e([A]))}(0)])\)が定義されたので、この定義から\(EE_{EE_{E(\e(0)+\e([A]))}(0)+A}(\a)\)が定義され、

以後同様に\(EE_{X+A}(\a)\)が定義されていきます。

つまり、

\(EE_A(EE_{E(\e(0)+\e([A]))}(0))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(0)+E(\e([EE_{E(\e(0)+\e([A]))}(0)])))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(0)+E(\e([EE_{E(\e(0)+\e([A]))}(0)])\*(2)))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(0)+A)\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(0)+A+A)\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(0)+EE_{E(\e(0)+\e([A]))}(0))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(0)+EE_{E(\e(0)+\e([A]))}(0)+E(\e([EE_{E(\e(0)+\e([A]))}(0)+EE_{E(\e(0)+\e([A]))}(0)])))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(0)+EE_{E(\e(0)+\e([A]))}(0)+A)\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(0)+EE_{E(\e(0)+\e([A]))}(0)+EE_{E(\e(0)+\e([A]))}(0))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(1))\)

のようになります。

\(EE_A(EE_{E(\e(0)+\e([A]))}(A))\)まで

さて、ここから少しややこしくなります。

まず、\(A<E(\e(0)+\e([A]))\)なので、\(EE_{E(\e(0)+\e([A]))}(\a)\)の中では定義ずらしのリセットが起きません。

理由はすぐに分かります。

\(EE_A(EE_{E(\e(0)+\e([A]))}(1))\)からさらに大きくしていくと、いずれ\(EE_A(EE_{E(\e(0)+\e([A]))}(E(\e([A]))))\)になります。

\(A<EE_{E(\e(0)+\e([A]))}(\a)\)なので、任意の標準形\(\a\)に対し、\(\e([EE_{E(\e(0)+\e([A]))}(\a)])\)が定義されます。

そのため、\(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([A])))]))\)が存在し、\(EE_A(EE_{E(\e(0)+\e([A]))}(E(\e([A]))))\)からさらに大きくしていくと

いずれ\(EE_A(EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([A])))]))))\)になります。

めっちゃ太りましたね・・・

既に察していると思いますが、\(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([A])))])))]))\)から

\(EE_A(EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([A])))])))]))))\)が定義でき、

このようにして\(EE_{E(\e(0)+\e([A]))}(\a)\)は大きくなっていきます。

任意の\(X∈AT\)に対し、\(A>E(\e([X]))\)なので、

\(EE_A(EE_{E(\e(0)+\e([A]))}(A))\)を\(EE_A(EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([...])))]))))\)と定義します。

\(E(\e([X]))\)をOCFのように見なすわけです。

\(EE_{EE_{E(\e(0)+\e([A]))}(A)}(\a)\)を定義しない理由は、

\(EE_A(EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(A)))\)の展開を

\(EE_{EE_{E(\e(0)+\e([A]))}(A)}(\a)\)で行うのか、

\(EE_{EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(A))}(\a)\)で行うのかの区別をつけられないからです。

(区別を付けようとすると無限個の場合分けが必要になる)

さて、実はここまでやってきたことの繰り返しで\(EE_A(A_2)\)未満の定義は全て説明可能です。

なのでこれ以降はかなり速を上げていきたいと思います。


\(EE_A(A_2)\)まで

というわけで速を一気に上げてざっくりした流れを垂れ流すだけにします。

ここの部分もっと細かくして欲しいとかあったらコメントにどうぞ。

では、上のおさらいも兼ねて\(EE_A(EE_{E(\e(0)+\e([A]))}(1))\)からいきます。


\(EE_A(EE_{E(\e(0)+\e([A]))}(1))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(1)+A)\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(1)+EE_{E(\e(0)+\e([A]))}(0))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(1)+EE_{E(\e(0)+\e([A]))}(1))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(2))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(3))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(EE_{E(\e([A]))}(0)))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(E(\e([A]))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([A])]))))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A)+EE_{E(\e(0)+\e([A]))}(E(\e([A]))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A)+EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(E(\e([A])))]))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A)+EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(A)]))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A)+EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(A)+EE_{E(\e(0)+\e([A]))}(E(\e([A])))]))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A)+EE_{E(\e(0)+\e([A]))}(A))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A+1))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A+E(\e([A]))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A+E(\e([EE_{E(\e(0)+\e([A]))}(A+E(\e([A])))]))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A+A))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(A+A+A))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(0)))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(E(\e([A])))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(E(\e([EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(E(\e([A]))))])))))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(A)))\)

\(EE_A(EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(EE_{E(\e(0)+\e([A]))}(0))))\)

\(EE_A(E(\e(0)+\e([A])))\)

\(EE_A(E(\e(0)+\e([A]))+E(\e(0)+\e([A])))\)

\(EE_A(EE_{E(\e(0)+\e([A])\*(2))}(0))\)

\(EE_A(E(\e(0)+\e([A])\*(2)))\)

\(EE_A(E(\e(0)+\e([A])\*(3)))\)

\(EE_A(E(\e(0)+\e([A])\*(3)))\)

\(EE_A(E(\e(0)+\e([A])\*(E(\e([A])))))\)

\(EE_A(E(\e(0)+\e([A])\*(E(\e([E(\e(0)+\e([A])\*(E(\e([A]))))])))))\)

\(EE_A(E(\e(0)+\e([A])\*(A)))\)

\(EE_A(E(\e(0)+\e([A])\*(E(\e(0)+\e([A])\*(1))))\)

\(EE_A(EE_{E(\e(0)+\e([A+A]))}(0))\)

\(EE_A(E(\e(0)+\e([A+A])))\)

\(EE_A(E(\e(0)+\e([A+A+A])))\)

\(EE_A(E(\e(0)+\e([EE_{E(\e(0)+\e([A]))}(0)])))\)

\(EE_A(E(\e(0)+\e([E(\e(0)+\e([A])])))\)

\(EE_A(E(\e(0)+\e([E(\e(0)+\e([E(\e(0)+\e([A])]))])))\)

\(EE_A(E(\e(0)×(2))) = EE_A(A_2)\)


こんな感じになります。

\(EE_A(A_2+A_2)\)まで

\(A_{\a +1}\)の展開は\(EE_{E(\e(0)+\e([A]))}(A)\)の応用になります。

つまり\(A_{\a +1}\)に対し、\(E(\e(0)×(\a)+\e([X])\)をOCFとみなして展開するわけです。

実際に流れを見てみればわかると思います。

\(EE_A(A_2)\)

\(EE_A(A_2+E(\e(0)+\e([A])))\)

\(EE_A(A_2+E(\e(0)+\e([E(\e(0)+\e([A]))])))\)

\(EE_A(A_2+EE_{E(\e(0)+\e([A_2]))}(0))\)

\(EE_A(A_2+E(\e(0)+\e([A_2])))\)

\(EE_A(A_2+E(\e(0)+\e([A_2+E(\e(0)+\e([A_2]))])))\)

\(EE_A(A_2+A_2)\)


こんな感じになります。

これ以降は今までやってきたことの繰り返しになるので、これで解説するべきことは終わりです。

あとは流れをざっくりした流れを垂れ流すだけにします。


\(EE_A(A_{A_{...}})\)まで

気になるところとかあったらコメントかTwitterにお願いします。


\(EE_A(E(\e(0)×(2)))\)

\(EE_A(E(\e(0)×(2))+E(\e(0)×(2)))\)

\(EE_A(E(\e(0)×(2))+E(\e(0)×(2))+E(\e(0)×(2)))\)

\(EE_A(E(\e(0)×(2)+\e([A])))\)

\(EE_A(E(\e(0)×(2)+\e([E(\e(0)×(2))])))\)

\(EE_A(E(\e(0)×(2)+\e([E(\e(0)×(2)+\e([A]))])))\)

\(EE_A(E(\e(0)×(2)+\e([E(\e(0)×(2)+\e([E(\e(0)×(2)+\e([A]))]))])))\)

\(EE_A(E(\e(0)×(3)))\)

\(EE_A(E(\e(0)×(4)))\)

\(EE_A(E(\e(0)×(E(\e([A])))))\)

\(EE_A(E(\e(0)×(E(\e([E(\e(0)×(2))])))))\)

\(EE_A(E(\e(0)×(E(\e([E(\e(0)×(E(\e([A]))))])))))\)

\(EE_A(E(\e(0)×(A)))\)

\(EE_A(E(\e(0)×(E(\e(0)+\e([A])))))\)

\(EE_A(E(\e(0)×(E(\e(0)+\e([E(\e(0)×(E(\e(0)+\e([A]))))])))))\)

\(EE_A(E(\e(0)×(E(\e(0)×(2)))))\)

\(EE_A(E(\e(0)×(E(\e(0)×(E(\e([A])))))))\)

\(EE_A(E(\e(0)×(E(\e(0)×(E(\e([E(\e(0)×(E(\e(0)×(E(\e([A]))))))])))))))\)

\(EE_A(E(\e(0)×(E(\e(0)×(A)))))\)

\(EE_A(E(\e(0)×(E(\e(0)×(E(\e(0)×(A)))))))\)

...


ね、簡単でしょう?

特に記載のない限り、コミュニティのコンテンツはCC-BY-SA ライセンスの下で利用可能です。