雑記帳
自然数対象を持つトポスで有名な巨大数である「グラハム数」を構成してみる
(ここで議論を進めていくうえで想定している数学基礎が素朴集合論ではないことに注意してほしい)
グラハム数を構成する
Knuth の矢印表記を写像として構成する
Knuth の矢印表記とは
Wikipedia 参照 (以下にリンクを貼っておく)
- クヌースの矢印表記 [外部リンク]
指数関数、テトレーションの定義の間のパターン
グラハム数を定義するために、しばしば「Knuth の矢印表記」が用いられる。
しかし表記だけではただの記号であり、「特定の自然数対象の要素」としての意味までもは明確にすることができず、ETCS 集合論的な視点からはまだ不完全となる。
(圏論的集合論において、写像は「(合成演算の定義された) 具体的な実体ある矢印」であるわけだが、実践的な数学においては「抽象的な対応の規則」という砕けて漠然とした概念として捉えられることもある。後者の流儀の場合、「記号操作の果てに、一つの出力に辿り着くことができるのかが曖昧である記号操作のルール」も一つの写像と見做すことができるが、前者の流儀においては、そう単純な話では無くなってくる。)
要は「自然数対象公理により認められる再帰的な射の構成によって Knuth の矢印表記 に相当する写像が構成できるのか」ということをちゃんと確かめる必要がある。(言い方を変えるなら、「一つの計算可能な関数として直接構成してあげる必要がある」といったところだろうか。)
まず、構成パターンの可視化を目的として、「掛け算」から「ペンテーション」までの構成を列挙してみる。
\[
\begin{align}
(\cdot)_{{\mathbb{N}}} &= {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm zero})), \lambda[\langle {\rm prj}_2, {\rm ev} \rangle {\sf \, ⨟ \,} (+)_{{\mathbb{N}}}])\times {\mathbb{N}} {\sf \, ⨟ \,} {\rm ev} \\
(\uparrow)_{{\mathbb{N}}} &= {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ})), \lambda[\langle {\rm prj}_2, {\rm ev} \rangle {\sf \, ⨟ \,} (\cdot)_{{\mathbb{N}}}])\times {\mathbb{N}} {\sf \, ⨟ \,} {\rm ev} \\
(\uparrow \uparrow)_{{\mathbb{N}}} &= {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ})), \lambda[\langle {\rm prj}_2, {\rm ev} \rangle {\sf \, ⨟ \,} (\uparrow)_{{\mathbb{N}}}])\times {\mathbb{N}} {\sf \, ⨟ \,} {\rm ev} \\
(\uparrow \uparrow \uparrow)_{{\mathbb{N}}} &= {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ})), \lambda[\langle {\rm prj}_2, {\rm ev} \rangle {\sf \, ⨟ \,} (\uparrow \uparrow)_{{\mathbb{N}}}])\times {\mathbb{N}} {\sf \, ⨟ \,} {\rm ev} \\
\end{align}
\]
見ての通り掛け算を除いては同じ構成パターンになっていて、つまりは \(\xi_{n}\) を
\[
({\rm arrToEl}((\uparrow ^{n+1})_{{\mathbb{N}}}) {\sf \, ⨟ \,} {\rm curry}):1\rightarrow ({\mathbb{N}}^ {\mathbb{N}})^ {\mathbb{N}}
\]
と置くと、その射 \(\xi_{n}\) は次のような一般式でまとめられることに気付く。
\[
\begin{align}
\xi_0 &= {\rm arrToEl}((\cdot)_{{\mathbb{N}}}) {\sf \, ⨟ \,} {\rm curry} \\
\xi_{n+1} &= \lambda[{\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ})), {\rm elToArr}(\lambda q.(\lambda m.( \langle \xi_n {\sf \, ⨟ \,} {\rm uncurry} , \langle m, \langle q,m \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev}) )) )] \\
&= \lambda[{\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ})), {\rm elToArr}(\xi_n {\sf \, ⨟ \,} \lambda[\lambda[\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm uncurry} , \langle {\rm prj}_2, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 , {\rm prj}_2 \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev} ]]))] \\
\end{align}
\]
但し
\[
{\rm elToArr}(x) := \langle !, X \rangle {\sf \, ⨟ \,} (x \times X) {\sf \, ⨟ \,} {\rm ev}
\]
一方で、この関係式には「括りださなければいけない \(\xi_n\) が Recursor の中に含まれている」という問題がある。
定義から明らかなように、\({\rm rec}_{{\mathbb{N}}}(x_0,f)\) から \(x_0,f\) を括りだせることは自明ではない。
Recursor から2つのデータを括りだす
そもそも Recursor \({\rm rec}_{{\mathbb{N}}}(x_0,f)\) は、自然数対象公理より
- \(X\) の要素 \(x_0:1\rightarrow X\)
- \(X\) 上の自己準同形 \(f:X\rightarrow X\)
が与えられた時に引き起こされる
- 自然数 \(n:1\rightarrow {\mathbb{N}}\) の入力に対して \(f^n(x_0):1\rightarrow X\) を出力する写像 \({\mathbb{N}} \rightarrow X\) (自然数対象の普遍性が、引き起こされる射に対してこのような具体的な意味を与える)
である。
ここで、ETCS は「カルテシアン閉」ということを公理として認めていることから「内部合成 \({\rm iComp}\)」の構成が可能となり、そのような「引き起こされる射が持つ意味と実質同じ意味を持った射」の構成を写像 \({\rm iterate}:X\times X^X \rightarrow X^{{\mathbb{N}}}\) として構成できる可能性がある。
各自考えてみればわかるが、これはそこまで難しいことでもなくて、プログラミング等で高階関数の取扱いに慣れている人からすれば尚更パッと思いつくような構成になっている。
具体的には \({\rm iterate}:X\times X^X \rightarrow X^{{\mathbb{N}}}\) は次のように定義できる
\[
{\rm iterate} := \lambda[(\langle \langle {\rm prj}_2, {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 \rangle, {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 \rangle) {\sf \, ⨟ \,} (\langle {\rm const}({\rm arrToEl}({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm arrToEl}(X^X))),\lambda[\langle {\rm prj}_2,{\rm ev} \rangle {\sf \, ⨟ \,} {\rm iComp}])) {\sf \, ⨟ \,} {\rm uncurry} {\sf \, ⨟ \,} {\rm uncurry}), ({\mathbb{N}} \times X^X)\times X \rangle) {\sf \, ⨟ \,} {\rm ev}]
\]
(..)
\(\xi_{n+1}\) から \(\xi_n\) を括りだすと
\[
\begin{align}
\xi_{n+1} &= \lambda[{\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ})), {\rm elToArr}(\xi_n {\sf \, ⨟ \,} \lambda[\lambda[\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm uncurry} , \langle {\rm prj}_2, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 , {\rm prj}_2 \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev} ]] ))] \\
&= \langle {\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ})), \xi_n {\sf \, ⨟ \,} \lambda[\lambda[\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm uncurry} , \langle {\rm prj}_2, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 , {\rm prj}_2 \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev} ]] \rangle {\sf \, ⨟ \,} {\rm iterate} {\sf \, ⨟ \,} {\rm flip} \\
&= \xi_n {\sf \, ⨟ \,} \langle {\rm const}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ}))), \lambda[\lambda[\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm uncurry} , \langle {\rm prj}_2, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 , {\rm prj}_2 \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev} ]] \rangle {\sf \, ⨟ \,} {\rm iterate} {\sf \, ⨟ \,} {\rm flip} \\
\end{align}
\]
よって \(\xi:{\mathbb{N}} \rightarrow ({\mathbb{N}} ^{\mathbb{N}})^ {\mathbb{N}}\) は次のように構成できる
\[
\xi := {\rm rec}_{{\mathbb{N}}}({\rm arrToEl}((\cdot)_{{\mathbb{N}}}) {\sf \, ⨟ \,} {\rm curry}, \langle {\rm const}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ}))), \lambda[\lambda[\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm uncurry} , \langle {\rm prj}_2, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 , {\rm prj}_2 \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev} ]] \rangle {\sf \, ⨟ \,} {\rm iterate} {\sf \, ⨟ \,} {\rm flip})
\]
\(\xi\) が定義できれば、
\[
x \uparrow^{n} y := \langle n {\sf \, ⨟ \,} \xi {\sf \, ⨟ \,} {\rm uncurry}, \langle x,y \rangle \rangle {\sf \, ⨟ \,} {\rm ev}
\]
より \({\rm tower}:(({\mathbb{N}} \times {\mathbb{N}})\times {\mathbb{N}}) \rightarrow {\mathbb{N}}\) を
\[
{\rm tower} := \langle {\rm prj}_2 {\sf \, ⨟ \,} \xi {\sf \, ⨟ \,} {\rm uncurry}, {\rm prj}_1 \rangle {\sf \, ⨟ \,} {\rm ev}
\]
とすると、
\[
x \uparrow^{n} y := \langle \langle x,y \rangle, n \rangle {\sf \, ⨟ \,} {\rm tower}
\]
余談
英語版 Wikipedia によるとオリジナルの定義には \(n=0\) の場合は含まれてなく、 \(x \uparrow ^0 y\) は未定義とのこと。
(原文: Note, however, that Knuth did not define the "nil-arrow" \((\uparrow^0)\).)
(原文: Note, however, that Knuth did not define the "nil-arrow" \((\uparrow^0)\).)
ここではトポス理論を意識した グラハム数の構成の成り行きで 意図せず \(n=0\) の場合に対して自然数の積が割り当てられたが、その流儀で \(n=0\) の場合を定義することもあるらしい。
(原文: One can alternatively choose multiplication (\(a \uparrow ^0 b = a \times b\)) as the base case and iterate from there.)
(原文: One can alternatively choose multiplication (\(a \uparrow ^0 b = a \times b\)) as the base case and iterate from there.)
※ 基本的に僕は単なる関数型プログラミング言語ファンなだけで、巨大数に精通しているわけでは全くないので詳しいことはもちろんよくわからない。
グラハム数を自然数対象の一つの要素として構成する
「Knuth の矢印表記」に相当する射が構成できてしまえば、グラハム数 \(G\) を構成するのは簡単である。
\[
\begin{align}
G :&= {64}_{{\mathbb{N}}} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}(4_{{\mathbb{N}}}, \langle {\rm const}(\langle 3_{{\mathbb{N}}},3_{{\mathbb{N}}} \rangle), {\mathbb{N}} \rangle {\sf \, ⨟ \,} {\rm tower}) \\
&= {64}_{{\mathbb{N}}} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}(4_{{\mathbb{N}}}, \langle {\rm const}(\langle 3_{{\mathbb{N}}},3_{{\mathbb{N}}} \rangle), {\mathbb{N}} \rangle {\sf \, ⨟ \,} (\langle {\rm prj}_2 {\sf \, ⨟ \,} \xi {\sf \, ⨟ \,} {\rm uncurry}, {\rm prj}_1 \rangle {\sf \, ⨟ \,} {\rm ev})) \\
&= {64}_{{\mathbb{N}}} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}(4_{{\mathbb{N}}}, \langle {\rm const}(\langle 3_{{\mathbb{N}}},3_{{\mathbb{N}}} \rangle), {\mathbb{N}} \rangle {\sf \, ⨟ \,} (\langle {\rm prj}_2 {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}((\cdot)_{{\mathbb{N}}}) {\sf \, ⨟ \,} {\rm curry}, \langle {\rm const}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ}))), \lambda[\lambda[\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm uncurry} , \langle {\rm prj}_2, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 , {\rm prj}_2 \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev} ]] \rangle {\sf \, ⨟ \,} {\rm iterate} {\sf \, ⨟ \,} {\rm flip})) {\sf \, ⨟ \,} {\rm uncurry}, {\rm prj}_1 \rangle {\sf \, ⨟ \,} {\rm ev})) \\
&= {64}_{{\mathbb{N}}} {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}(4_{{\mathbb{N}}}, \langle {\rm const}(\langle 3_{{\mathbb{N}}},3_{{\mathbb{N}}} \rangle), {\mathbb{N}} \rangle {\sf \, ⨟ \,} (\langle {\rm prj}_2 {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}((\cdot)_{{\mathbb{N}}}) {\sf \, ⨟ \,} {\rm curry}, \langle {\rm const}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ}))), \lambda[\lambda[\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm uncurry} , \langle {\rm prj}_2, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 , {\rm prj}_2 \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev} ]] \rangle {\sf \, ⨟ \,} \lambda[(\langle \langle {\rm prj}_2, {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 \rangle, {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 \rangle) {\sf \, ⨟ \,} (\langle {\rm const}({\rm arrToEl}({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm arrToEl}(X^X))),\lambda[\langle {\rm prj}_2,{\rm ev} \rangle {\sf \, ⨟ \,} {\rm iComp}])) {\sf \, ⨟ \,} {\rm uncurry} {\sf \, ⨟ \,} {\rm uncurry}), ({\mathbb{N}} \times X^X)\times X \rangle) {\sf \, ⨟ \,} {\rm ev}] {\sf \, ⨟ \,} {\rm flip})) {\sf \, ⨟ \,} {\rm uncurry}, {\rm prj}_1 \rangle {\sf \, ⨟ \,} {\rm ev})) \\
&= (\langle {\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ},{\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} \rangle {\sf \, ⨟ \,} (\cdot)_{{\mathbb{N}}} {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\cdot)_{{\mathbb{N}}}) {\sf \, ⨟ \,} {\rm rec}_{{\mathbb{N}}}({\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ}, \langle {\rm const}(({\rm zero} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ} {\sf \, ⨟ \,} {\rm succ}) {\sf \, ⨟ \,} \Delta), {\mathbb{N}} \rangle {\sf \, ⨟ \,} (\langle {\rm prj}_2 {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}((\cdot)_{{\mathbb{N}}}) {\sf \, ⨟ \,} {\rm curry}, \langle {\rm const}({\rm arrToEl}({\rm const}({\rm zero} {\sf \, ⨟ \,} {\rm succ}))), \lambda[\lambda[\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm uncurry} , \langle {\rm prj}_2, \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 , {\rm prj}_2 \rangle {\sf \, ⨟ \,} {\rm ev} \rangle \rangle {\sf \, ⨟ \,} {\rm ev} ]] \rangle {\sf \, ⨟ \,} \lambda[(\langle \langle {\rm prj}_2, {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2 \rangle, {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 \rangle) {\sf \, ⨟ \,} (\langle {\rm const}({\rm arrToEl}({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\rm const}({\rm arrToEl}(X^X))),\lambda[\langle {\rm prj}_2,{\rm ev} \rangle {\sf \, ⨟ \,} {\rm iComp}])) {\sf \, ⨟ \,} {\rm uncurry} {\sf \, ⨟ \,} {\rm uncurry}), ({\mathbb{N}} \times X^X)\times X \rangle) {\sf \, ⨟ \,} {\rm ev}] {\sf \, ⨟ \,} {\rm flip})) {\sf \, ⨟ \,} {\rm uncurry}, {\rm prj}_1 \rangle {\sf \, ⨟ \,} {\rm ev})) \\
\end{align}
\]
(\(\Delta\), \((\cdot)_{{\mathbb{N}}}\), \({\rm iComp}\), \({\rm curry}\), \({\rm uncurry}\), \({\rm flip}\) 等も全て存在が公理的に認められている射の組み合わせとして書き換えることができるが、余りにも長くなってしまうため省略)
Haskell での動作確認
以上の議論を見ても「本当にそのめちゃくちゃな式が グラハム数を定めるのか」と疑う人も少なくないかもしれないので、僕がデバッグに用いた Haskell を使って議論通りに \({\rm tower}\) 関数を組み立てたソースコードを載せておく。
流石に グラハム数の全桁を10進数表記で求めることは現実問題として不可能だが、それを求めるために必要になる tower 関数の動作確認に対してはできないこともない。(但しこの \({\rm tower}\) 関数でさえも、入力する値 (特に3番目の入力) を 1 大きくするだけで出力される自然数の大きさが尋常でないレベルで跳ね上がるため、大きい値の入力に対する出力の検証はコンピュータ等の実世界の物質を使って行うことは難しい。)
流石に グラハム数の全桁を10進数表記で求めることは現実問題として不可能だが、それを求めるために必要になる tower 関数の動作確認に対してはできないこともない。(但しこの \({\rm tower}\) 関数でさえも、入力する値 (特に3番目の入力) を 1 大きくするだけで出力される自然数の大きさが尋常でないレベルで跳ね上がるため、大きい値の入力に対する出力の検証はコンピュータ等の実世界の物質を使って行うことは難しい。)
例えば以下のコードの実行例
ghci> printEl $ pair(pair(nat(2),nat(3)),nat(1)) -: tower
8
ghci> printEl $ pair(pair(nat(2),nat(3)),nat(2)) -: tower
16
ghci> printEl $ pair(pair(nat(2),nat(3)),nat(3)) -: tower
65536
ghci> printEl $ pair(pair(nat(2),nat(4)),nat(1)) -: tower
16
ghci> printEl $ pair(pair(nat(2),nat(4)),nat(2)) -: tower
65536
ghci> printEl $ pair(pair(nat(7),nat(2)),nat(2)) -: tower
823543からわかるように、
\[
\begin{align}
2 \uparrow 3 &= 8 \\
2 \uparrow\uparrow 3 &= 16 \\
2 \uparrow\uparrow\uparrow 3 &= 65536 \\
2 \uparrow 4 &= 16 \\
2 \uparrow\uparrow 4 &= 65536 \\
7 \uparrow\uparrow 2 &= 823543 \\
\end{align}
\]
が正しく計算できていることの確認ができる。
因みに
\[
3 \uparrow\uparrow 3 = 7625597484987
\]
を計算させようとしたところ、以下のようにスタックオーバーフローした。
ghci> printEl $ pair(pair(nat(3),nat(3)),nat(2)) -: tower
*** Exception: stack overflowソースコードを見ての通り、一応
ghci> :t grahamNumber
grahamNumber :: Pt -> Natというように、Haskell プログラム内でも一つの自然数対象の要素 \(G:1\rightarrow {\mathbb{N}}\) として、グラハム数を定義すること自体はできるが、当然その値を表示させようとしても
ghci> printEl $ grahamNumber
*** Exception: stack overflowというようにもちろん再びスタックオーバーフローして終わるだけとなる。
重要なのは
- グラハム数を構成するために使用している関数の中に「無限ループを引き起こせるもの」が一つも含まれてない
という点で、これによって少なくとも一つの (有限の) 自然数として定まることが保証されることである。
ソースコード
{-# LANGUAGE TypeOperators #-}
import Data.Void
main :: IO ()
main = do
printEl $ pair(pair(nat(2),nat(4)),nat(0)) -: tower
printEl $ pair(pair(nat(2),nat(3)),nat(1)) -: tower
printEl $ pair(pair(nat(2),nat(3)),nat(2)) -: tower
printEl $ pair(pair(nat(2),nat(3)),nat(3)) -: tower
printEl $ pair(pair(nat(2),nat(4)),nat(1)) -: tower
printEl $ pair(pair(nat(2),nat(4)),nat(2)) -: tower
printEl $ pair(pair(nat(7),nat(2)),nat(2)) -: tower
class (MyShow a) where
myShow :: a -> String
instance MyShow () where
myShow = const "*"
instance (MyShow a, MyShow b) => MyShow (Either a b) where
myShow = either
(\z -> if (myShow z == "*") then "inj1" else (myShow z) ++ ";inj1")
(\z -> if (myShow z == "*") then "inj2" else (myShow z) ++ ";inj2")
instance (MyShow a, MyShow b) => MyShow (a,b) where
myShow (x,y) = "(" ++ myShow x ++ "," ++ myShow y ++ ")"
instance MyShow Int where
myShow = show
instance MyShow Nat where
myShow (Nat i) = myShow (length i)
--myShow (Nat i) = "zero" ++ (foldr ((++).(const ";succ")) [] i)
instance MyShow (a -> b) where
myShow = const "(AN ARROW)"
-- X の要素を圏論に倣って終対象から X への射(Global element)として扱うための関数
el :: a -> (Pt -> a)
el = (const::a -> (Pt -> a))
-- Global elements 用 ユーティリティ
(===) :: Eq a => (Pt -> a) -> (Pt -> a) -> Bool
(===) x y = (x() == y())
showEl :: MyShow a => (Pt -> a) -> String
showEl x = (myShow $ x())
printEl :: MyShow a => (Pt -> a) -> IO ()
printEl = putStrLn . showEl
-- Diagrammatic-order な射の合成演算
(-:) = flip (.)
-- # 始対象と終対象
type Empty = Void
type Pt = ()
initArr :: Empty -> a
initArr = absurd
termArr :: a -> Pt
termArr = const ()
point :: Pt -> Pt
point = id
const' x = termArr -: x
-- # 余積対象と積対象
type (+++) a b = Either a b
type (***) a b = (a,b)
-- 入射
inj1 :: a -> a +++ b
inj1 = Left
inj2 :: b -> a +++ b
inj2 = Right
-- 射影
prj1 :: a *** b -> a
prj1 = fst
prj2 :: a *** b -> b
prj2 = snd
-- 余積対象の仲介射
coPair :: (a -> c, b -> c) -> (a +++ b -> c)
coPair = uncurry either
-- 積対象の仲介射
pair :: (c -> a, c -> b) -> (c -> a *** b)
pair = uncurry $ (<*>) . fmap (,)
-- 畳み込み
fol = coPair(id, id)
-- 対角射
dup = pair(id, id)
-- 射同士の余積
(+++) :: (a1 -> b1) -> (a2 -> b2) -> (a1 +++ a2 -> b1 +++ b2)
(+++) f g = coPair(f -: inj1 , g -: inj2)
-- 射同士の積
(***) :: (a1 -> b1) -> (a2 -> b2) -> (a1 *** a2 -> b1 *** b2)
(***) f g = pair(prj1 -: f, prj2 -: g)
-- Twist の形式的双対
coTw :: a +++ b -> b +++ a
coTw = coPair(inj2, inj1)
-- Twist
tw :: a *** b -> b *** a
tw = pair(prj2, prj1)
-- # Exponential 対象
type (^) b a = a -> b
-- 評価射
ev :: (b ^ a) *** a -> b
ev = uncurry id
-- 射の転置 (transpose) の構成
trans :: (c *** a -> b) -> (c -> b ^ a)
trans = curry
-- 射 h:a->b の Exponential 対象 (Exp b a) の要素への変換
arrToEl :: (a -> b) -> (Pt -> b ^ a)
arrToEl h = trans(prj2-:h)
elToArr x = pair(termArr, id) -: (x *** id) -: ev
curry' :: (c ^ (a *** b)) -> (c ^ b) ^ a
curry' = trans(trans(pair(prj1 -: prj1, pair(prj1 -: prj2, prj2)) -: ev))
uncurry' :: (c ^ b) ^ a -> (c ^ (a *** b))
uncurry' = trans(pair(pair(prj1,prj2 -: prj1), prj2 -: prj2) -: (ev *** id) -: ev)
iComp :: ((b^a) *** (c^b)) -> c^a
iComp = trans(pair(prj1 -: prj2, pair(prj1 -: prj1, prj2)) -: (id *** ev) -: ev)
flip' :: ((c^b)^a) -> ((c^a)^b)
flip' = uncurry' -: trans((id *** tw) -: ev) -: curry'
-- # 自然数対象 (NNO)
data Nat = Nat{imp::[()]} deriving Eq
_Nat :: Nat -> Nat
_Nat = id
zero :: Pt -> Nat
zero = el (Nat [])
succ' :: Nat -> Nat
succ' (Nat i) = Nat (():i)
-- 整数リテラルを使って NNO の Global elements としての自然数を得るための小細工
nat :: Int -> (Pt -> Nat)
-- nat i = zero -: (foldr (.) id (replicate i succ'))
nat i = el (Nat (replicate i ()))
-- recursion data x_0:1->X と f:X->X から rec_N(x_0, f):Nat->X を構成する関数
rec_N :: (Pt -> a, a -> a) -> (Nat -> a)
rec_N = ((flip ($) ())***id)-:((curry((id***(length.imp))-:uncurry(!!))).(uncurry.flip $ iterate))
iterate' :: x *** (x ^ x) -> (x ^ Nat)
iterate' =
trans(pair(pair(prj2, prj1 -: prj2), prj1 -: prj1) -:
pair(const'(arrToEl(rec_N(arrToEl(const'(arrToEl(id))),trans(pair(prj2,ev) -: iComp))) -:
uncurry' -: uncurry'), id) -: ev)
add_N = (rec_N(arrToEl(_Nat), trans(ev-:succ'))***_Nat)-:ev
mul_N = (rec_N(arrToEl(termArr-:nat(0)), trans(pair(ev,prj2)-:add_N))***_Nat)-:ev
mul_N_fast (Nat x, Nat y) = Nat (replicate (length x * length y) ()) -- デバッグ用
sq_N = dup-:mul_N
xi =
rec_N(arrToEl(mul_N) -: curry', pair(const'(arrToEl(const'(nat(1)))) , trans(trans(pair(prj1 -: prj1 -:
uncurry', pair(prj2, pair(prj1 -: prj2, prj2) -: ev)) -: ev))) -: iterate' -: flip')
tower = pair(prj2 -: xi -: uncurry', prj1) -: ev
grahamNumber = nat(64) -: rec_N(nat(4),pair(const'(pair(nat(3),nat(3))),_Nat)-:tower)タグ一覧: