はじめに。
NNOという概念を知れば、これを使ってrecursive functionとか作れんかなと思うのは人間の自然な心の動きです。というわけでみんな大好きAckermann関数を作ります。
NNOではなくweak NNOを使うのは、数学的に条件は弱い方がいいよねが1割、Mathlogが現状唯一サポートしている図式描画パッケージであるamscdでは破線が使えないからが9割です。xypic対応はよ。
準備
cartesian closed category (CCC) の定義に関しては
私の過去記事
を見てください。記法もこれに合わせます。また自然数の集合をで表します。
weak natural numbers object (weak NNO)
CCC において、weak NNOとは三つ組であって、同様の三つ組のなかで弱普遍的なものを言う。つまり、任意の三つ組に対し、ある射が存在して, を満たす。
weak NNOの特徴付け
任意のCCC において、三つ組がweak NNOであることと、のobject を受け取って射を与える割り当てであって以下を満たすものが存在することが同値である。
やるだけ。
weak NNOなら各に対し、次の弱普遍性から従う射を1つ取ってくればよい。
逆にこのような割り当てが存在するとき、任意の三つ組に対し、がかつなる射になる。
この補題から、CCCを10個組と定義したのと同様に、CCC with weak NNOを5個組と定義することもできます。どうしてロジシャンはそんな特徴付けをしたがるの?形式体系として扱いやすいからだよ。
Ackermann function
Ackermann関数とは次で定義される関数のこと。
この子はtotally recursiveだがprimitive recursiveでない関数の例として有名ですね。ちなみに発明者はAckermannではありません。
本題
そもそもNNOで関数を作るってなんぞや?という話ですね。
representable function
CCC with weak NNO において自然数関数が representableであるとは、あるの射が存在して任意のに対し、を満たすことを言う。ただし自然数に対しでを回合成した射を表す。
定義から、たとえば Set との下では任意の自然数関数が representable です。
せっかくなので。
All primitive recursive functions are representable in any CCC with weak NNO.
帰納法。
- zero:、succ:、proj: for any が representable であるのは明らか。
- representable functionが合成で閉じてるのも明らか。
- とがそれぞれ及びでrepresentされるとき、との原始再帰で定義される関数は次の射でrepresentされる。
ただしは、weak NNOの弱普遍性から導かれる次のような射である。
今回の主役
is representable in any CCC with weak NNO.
作れば勝ち。
は射でrepresentされる。
ただしは、weak NNOの弱普遍性から導かれる次のような射である。
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とその構造を保つ関手の成す圏には始対象が存在し、any CCC with weak NNOでrepresentできることとでrepresentできることが同値になります。さらにでは任意の射がという形をしており、したがって任意の射がなんらかの自然数関数をrepresentしていることが示せます。
Q. 証明に出てきたよくわからん構成どうやって思いついてるの。
A. このくらいならCCCやNNOに慣れたら案外いけるよ。