大学数学基礎解説

Ackermann Function in CCC with weak NNO

191

Mathematical Logic Advent Calendar 2020 12/11

はじめに。

NNOという概念を知れば、これを使ってrecursive functionとか作れんかなと思うのは人間の自然な心の動きです。というわけでみんな大好きAckermann関数を作ります。

NNOではなくweak NNOを使うのは、数学的に条件は弱い方がいいよねが1割、Mathlogが現状唯一サポートしている図式描画パッケージであるamscdでは破線が使えないからが9割です。xypic対応はよ。

準備

cartesian closed category (CCC) の定義に関しては私の過去記事を見てください。記法もこれに合わせます。また自然数の集合を $N$ で表します。

weak natural numbers object (weak NNO)

CCC $C$ において、weak NNOとは三つ組 $(N \in | C |, z : T \to N, S : N \to N)$ であって、同様の三つ組のなかで弱普遍的なものを言う。つまり、任意の三つ組 $(B \in | C |, a : T \to B, f : B \to B)$ に対し、ある射 $g : N \to B$ が存在して $g z = a$ , $g S = f g$ を満たす。
$\begin{matrix} T & \overset{z}{\to} & N & \overset{S}{\to} & N \\ ∥ & ↻ & ↓ g & ↻ & ↓ g \\ T & \overset{a}{\to} & B & \overset{f}{\to} & B \end{matrix}$

weak NNOの特徴付け

任意のCCC $C$ において、三つ組 $(N \in | C |, z : T \to N, S : N \to N)$ がweak NNOであることと、 $C$ のobject $A$ を受け取って射 $R_{A} : N \to (A^{A})^{(A^{A})}$ を与える割り当てであって以下を満たすものが存在することが同値である。

$R_{A} z = ((q_{T \times A^{A}, A})^{*})^{*}$
$R_{A} S = ((e_{A, A} ⟨ q_{(A^{A})^{(A^{A})}, A^{A}} p_{(A^{A})^{(A^{A})} \times A^{A}, A}, e_{A, A} ⟨ e_{A^{A}, A^{A}} p_{(A^{A})^{(A^{A})} \times A^{A}, A}, q_{(A^{A})^{(A^{A})} \times A^{A}, A} ⟩ ⟩)^{*})^{*} R_{A}$

やるだけ。

weak NNOなら各 $A$ に対し、次の弱普遍性から従う射を1つ取ってくればよい。
$\begin{matrix} T & \overset{z}{\to} & N & \overset{S}{\to} & N \\ ∥ & ↻ & ↓ R_{A} & ↻ & ↓ R_{A} \\ T & \overset{((q_{T \times A^{A}, A})^{*})^{*}}{\to} & (A^{A})^{(A^{A})} & \overset{((e_{A, A} ⟨ q_{(A^{A})^{(A^{A})}, A^{A}} p_{(A^{A})^{(A^{A})} \times A^{A}, A}, e_{A, A} ⟨ e_{A^{A}, A^{A}} p_{(A^{A})^{(A^{A})} \times A^{A}, A}, q_{(A^{A})^{(A^{A})} \times A^{A}, A} ⟩ ⟩)^{*})^{*}}{\to} & (A^{A})^{(A^{A})} \end{matrix}$

逆にこのような割り当て $R$ が存在するとき、任意の三つ組 $(B \in | C |, a : T \to B, f : B \to B)$ に対し、 $e_{B, B} ⟨ e_{B^{B}, B^{B}} ⟨ R_{B} p_{N, B^{B}}, q_{N, B^{B}} ⟩ p_{N \times B^{B}, B}, q_{N \times B^{B}, B} ⟩ ⟨ ⟨ {id}_{N}, (f q_{T, B})^{*} o_{N} ⟩, a o_{N} ⟩ : N \to B$ が $g z = a$ かつ $g S = f g$ なる射 $g$ になる。

この補題から、CCCを10個組と定義したのと同様に、CCC with weak NNOを5個組 $(C, N, z, S, R)$ と定義することもできます。どうしてロジシャンはそんな特徴付けをしたがるの？形式体系として扱いやすいからだよ。

Ackermann function

Ackermann関数 $A : N^{2} \to 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で関数を作るってなんぞや？という話ですね。

representable function

CCC with weak NNO $C$ において自然数関数 $f : N^{n} \to N$ が representableであるとは、ある $C$ の射 $\tilde{f} : N^{n} \to N$ が存在して任意の $(x_{1}, \dots, x_{n}) \in N^{n}$ に対し、 $\tilde{f} ⟨ S^{x_{0}} z, \dots, S^{x_{n}} z ⟩ = S^{f (x_{1}, \dots, x_{n})} z$ を満たすことを言う。ただし自然数 $m$ に対し $S^{m}$ で $S$ を $m$ 回合成した射を表す。

定義から、たとえば Set と $N$ の下では任意の自然数関数が representable です。

せっかくなので。

All primitive recursive functions are representable in any CCC with weak NNO.

帰納法。

zero: $N^{0} \to N$ 、succ: $N \to N$ 、proj $_{m}^{n}$ : $N^{n} \to N$ for any $m < n$ が representable であるのは明らか。
representable functionが合成で閉じてるのも明らか。
$g : N^{n} \to N$ と $h : N^{n + 2} \to N$ がそれぞれ $\tilde{g}$ 及び $\tilde{h}$ でrepresentされるとき、 $g$ と $h$ の原始再帰で定義される関数 $f : N^{n + 1} \to N$ は次の射 $\tilde{f}$ でrepresentされる。

$\tilde{f} = p_{N, N} e_{N \times N, N^{n}} ⟨ β q_{N^{n}, N}, p_{N^{n}, N} ⟩$

ただし $β : N \to (N \times N)^{N^{n}}$ は、weak NNOの弱普遍性から導かれる次のような射である。
$\begin{matrix} T & \overset{z}{\to} & N & \overset{S}{\to} & N \\ ∥ & ↻ & ↓ β & ↻ & ↓ β \\ T & \overset{(⟨ g, z o_{N^{n}} ⟩ q_{T, N^{n}})^{*}}{\to} & (N \times N)^{N^{n}} & \overset{(⟨ h ⟨ q_{(N \times N)^{N^{n}}, N^{n}}, ⟨ q_{N, N}, p_{N, N} ⟩ e_{N \times N, N^{n}} ⟩, S q_{N, N} e_{N \times N, N^{n}} ⟩)^{*}}{\to} & (N \times N)^{N^{n}} \end{matrix}$

今回の主役

$A$ is representable in any CCC with weak NNO.

作れば勝ち。

$A : N^{2} \to N$ は射 $e_{N, N} ⟨ α p_{N, N}, q_{N, N} ⟩$ でrepresentされる。

ただし $α : N \to N^{N}$ は、weak NNOの弱普遍性から導かれる次のような射である。
$\begin{matrix} T & \overset{z}{\to} & N & \overset{S}{\to} & N \\ ∥ & ↻ & ↓ α & ↻ & ↓ α \\ T & \overset{(S q_{T, N})^{*}}{\to} & N^{N} & \overset{(e_{N, N} ⟨ e_{N^{N}, N^{N}} ⟨ R_{N} q_{N^{N}, N}, p_{N^{N}, N} ⟩, e_{N, N} ⟨ p_{N^{N}, N}, S z o_{N^{N} \times N} ⟩ ⟩)^{*}}{\to} & N^{N} \end{matrix}$

primitive recursive $⊊$ representable in any CCC with weak NNO

余談

実はさらに representable in any CCC with weak NNO $⊊$ totally recursive であることが知られています。そもそも Curry-Howard-Lambek対応から、representable in any CCC with weak NNO とは型付きラムダ計算で表現できる関数に他なりません。

ずっとrepresentable in any CCC with weak NNOと言ってきましたが、実はCCC with weak NNOとその構造を保つ関手の成す圏には始対象 $\bar{ϕ}$ が存在し、any CCC with weak NNOでrepresentできることと $\bar{ϕ}$ でrepresentできることが同値になります。さらに $\bar{ϕ}$ では任意の射 $T \to N$ が $S^{n} z$ という形をしており、したがって任意の射 $N^{n} \to N$ がなんらかの自然数関数をrepresentしていることが示せます。