Ackermann Function in CCC with weak NNO
Mathematical Logic Advent Calendar 2020 12/11
はじめに。
NNOという概念を知れば、これを使ってrecursive functionとか作れんかなと思うのは人間の自然な心の動きです。というわけでみんな大好きAckermann関数を作ります。
NNOではなくweak NNOを使うのは、数学的に条件は弱い方がいいよねが1割、Mathlogが現状唯一サポートしている図式描画パッケージであるamscdでは破線が使えないからが9割です。xypic対応はよ。
準備
cartesian closed category (CCC) の定義に関しては 私の過去記事 を見てください。記法もこれに合わせます。また自然数の集合を$\mathbb{N}$で表します。
CCC $\mathcal{C}$において、weak NNOとは三つ組$(N\in |\mathcal{C}|,z:T\rightarrow N,S:N\rightarrow N)$であって、同様の三つ組のなかで弱普遍的なものを言う。つまり、任意の三つ組$(B\in |C|,a:T\rightarrow B,f:B\rightarrow B)$に対し、ある射$g:N\rightarrow B$が存在して$gz=a$, $gS=fg$を満たす。
\begin{CD}
T @>{z}>> N @>{S}>> N \\
@|{\circlearrowright} @VV{g}V{\circlearrowright} @VV{g}V \\
T @>{a}>> B @>{f}>> B
\end{CD}
任意のCCC $\mathcal{C}$において、三つ組$(N\in |\mathcal{C}|,z:T\rightarrow N,S:N\rightarrow N)$がweak NNOであることと、$\mathcal{C}$のobject $A$を受け取って射$R_A:N\rightarrow (A^A)^{(A^A)}$を与える割り当てであって以下を満たすものが存在することが同値である。
- $R_Az=((q_{T\times A^A,A})^*)^*$
- $R_AS=((e_{A,A}\langle q_{(A^A)^{(A^A)},A^A}p_{(A^A)^{(A^A)}\times A^A,A},e_{A,A}\langle e_{A^A,A^A}p_{(A^A)^{(A^A)}\times A^A,A},q_{(A^A)^{(A^A)}\times A^A,A}\rangle\rangle)^*)^*R_A$
weak NNOなら各$A$に対し、次の弱普遍性から従う射を1つ取ってくればよい。
\begin{CD}
T @>{z}>> N @>{S}>> N \\
@|{\circlearrowright} @VV{R_A}V{\circlearrowright} @VV{R_A}V \\
T @>{((q_{T\times A^A,A})^*)^*}>> (A^A)^{(A^A)} @>{((e_{A,A}\langle q_{(A^A)^{(A^A)},A^A}p_{(A^A)^{(A^A)}\times A^A,A},e_{A,A}\langle e_{A^A,A^A}p_{(A^A)^{(A^A)}\times A^A,A},q_{(A^A)^{(A^A)}\times A^A,A}\rangle\rangle)^*)^*}>> (A^A)^{(A^A)}
\end{CD}
逆にこのような割り当て$R$が存在するとき、任意の三つ組$(B\in |C|,a:T\rightarrow B,f:B\rightarrow B)$に対し、$e_{B,B}\langle e_{B^B,B^B}\langle R_Bp_{N,B^B},q_{N,B^B}\rangle p_{N\times B^B,B},q_{N\times B^B,B}\rangle\langle\langle\mathsf{id}_N,(fq_{T,B})^*o_N\rangle,ao_N\rangle:N\rightarrow B$が$gz=a$かつ$gS=fg$なる射$g$になる。
この補題から、CCCを10個組と定義したのと同様に、CCC with weak NNOを5個組$(\mathcal{C},N,z,S,R)$と定義することもできます。どうしてロジシャンはそんな特徴付けをしたがるの？形式体系として扱いやすいからだよ。
Ackermann関数$A:\mathbb{N}^2\rightarrow\mathbb{N}$とは次で定義される関数のこと。
- $A(0,m)=m+1$
- $A(n+1,0)=A(n,1)$
- $A(n+1,m+1)=A(n,A(n+1,m))$
この子はtotally recursiveだがprimitive recursiveでない関数の例として有名ですね。ちなみに発明者はAckermannではありません。
本題
そもそもNNOで関数を作るってなんぞや？という話ですね。
CCC with weak NNO $\mathcal{C}$ において自然数関数$f:\mathbb{N}^n\rightarrow\mathbb{N}$が representableであるとは、ある$\mathcal{C}$の射$\tilde{f}:N^n\rightarrow N$が存在して任意の$(x_1,\dots,x_n)\in\mathbb{N}^n$に対し、$\tilde{f}\langle S^{x_0}z,\dots,S^{x_n}z\rangle=S^{f(x_1,\dots,x_n)}z$を満たすことを言う。ただし自然数$m$に対し$S^m$で$S$を$m$回合成した射を表す。
定義から、たとえば Set と$\mathbb{N}$の下では任意の自然数関数が representable です。
All primitive recursive functions are representable in any CCC with weak NNO.
- zero:$\mathbb{N}^0\rightarrow\mathbb{N}$、succ:$\mathbb{N}\rightarrow\mathbb{N}$、proj${}^n_m$:$\mathbb{N}^n\rightarrow\mathbb{N}$ for any $m< n$ が representable であるのは明らか。
- representable functionが合成で閉じてるのも明らか。
- $g:\mathbb{N}^n\rightarrow\mathbb{N}$と$h:\mathbb{N}^{n+2}\rightarrow\mathbb{N}$がそれぞれ$\tilde{g}$及び$\tilde{h}$でrepresentされるとき、$g$と$h$の原始再帰で定義される関数$f:\mathbb{N}^{n+1}\rightarrow\mathbb{N}$は次の射$\tilde{f}$でrepresentされる。
$\tilde{f} = p_{N,N}e_{N\times N,N^n}\langle\beta q_{N^n,N},p_{N^n,N}\rangle$
ただし$\beta:N\rightarrow (N\times N)^{N^n}$は、weak NNOの弱普遍性から導かれる次のような射である。
\begin{CD}
T @>{z}>> N @>{S}>> N \\
@|{\circlearrowright} @VV{\beta}V{\circlearrowright} @VV{\beta}V \\
T @>{(\langle g,zo_{N^n}\rangle q_{T,N^n})^*}>> (N\times N)^{N^n} @>{(\langle h\langle q_{(N\times N)^{N^n},N^n}, \langle q_{N,N}, p_{N,N}\rangle e_{N\times N,N^n}\rangle ,Sq_{N,N}e_{N\times N,N^n}\rangle)^*}>> (N\times N)^{N^n}
\end{CD}
$A$ is representable in any CCC with weak NNO.
$A:\mathbb{N}^2\rightarrow\mathbb{N}$は射$e_{N,N}\langle\alpha p_{N,N},q_{N,N}\rangle$でrepresentされる。
ただし$\alpha:N\rightarrow N^N$は、weak NNOの弱普遍性から導かれる次のような射である。
\begin{CD}
T @>{z}>> N @>{S}>> N \\
@|{\circlearrowright} @VV{\alpha}V{\circlearrowright} @VV{\alpha}V \\
T @>{(Sq_{T,N})^*}>> N^N @>{(e_{N,N}\langle e_{N^N,N^N}\langle R_Nq_{N^N,N},p_{N^N,N}\rangle,e_{N,N}\langle p_{N^N,N},Szo_{N^N\times N}\rangle\rangle)^*}>> N^N
\end{CD}
primitive recursive $\subsetneq$ representable in any CCC with weak NNO
余談
実はさらに representable in any CCC with weak NNO $\subsetneq$ totally recursive であることが知られています。そもそも Curry-Howard-Lambek対応から、representable in any CCC with weak NNO とは型付きラムダ計算で表現できる関数に他なりません。
ずっとrepresentable in any CCC with weak NNOと言ってきましたが、実はCCC with weak NNOとその構造を保つ関手の成す圏には始対象$\bar{\phi}$が存在し、any CCC with weak NNOでrepresentできることと$\bar{\phi}$でrepresentできることが同値になります。さらに$\bar{\phi}$では任意の射$T\rightarrow N$が$S^nz$という形をしており、したがって任意の射$N^n\rightarrow N$がなんらかの自然数関数をrepresentしていることが示せます。
$ $
Q. 証明に出てきたよくわからん構成どうやって思いついてるの。
A. このくらいならCCCやNNOに慣れたら案外いけるよ。
