4

Ackermann Function in CCC with weak NNO

191
0

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|C|,z:TN,S:NN)であって、同様の三つ組のなかで弱普遍的なものを言う。つまり、任意の三つ組(B|C|,a:TB,f:BB)に対し、ある射g:NBが存在してgz=a, gS=fgを満たす。
TzNSNggTaBfB

weak NNOの特徴付け

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

  1. RAz=((qT×AA,A))
  2. RAS=((eA,Aq(AA)(AA),AAp(AA)(AA)×AA,A,eA,AeAA,AAp(AA)(AA)×AA,A,q(AA)(AA)×AA,A))RA
やるだけ。

weak NNOなら各Aに対し、次の弱普遍性から従う射を1つ取ってくればよい。
TzNSNRARAT((qT×AA,A))(AA)(AA)((eA,Aq(AA)(AA),AAp(AA)(AA)×AA,A,eA,AeAA,AAp(AA)(AA)×AA,A,q(AA)(AA)×AA,A))(AA)(AA)

逆にこのような割り当てRが存在するとき、任意の三つ組(B|C|,a:TB,f:BB)に対し、eB,BeBB,BBRBpN,BB,qN,BBpN×BB,B,qN×BB,BidN,(fqT,B)oN,aoN:NBgz=aかつgS=fgなる射gになる。

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

Ackermann function

Ackermann関数A:N2Nとは次で定義される関数のこと。

  1. A(0,m)=m+1
  2. A(n+1,0)=A(n,1)
  3. 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:NnNが representableであるとは、あるCの射f~:NnNが存在して任意の(x1,,xn)Nnに対し、f~Sx0z,,Sxnz=Sf(x1,,xn)zを満たすことを言う。ただし自然数mに対しSmSm回合成した射を表す。

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

せっかくなので。

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

帰納法。
  1. zero:N0N、succ:NN、projmn:NnN for any m<n が representable であるのは明らか。
  2. representable functionが合成で閉じてるのも明らか。
  3. g:NnNh:Nn+2Nがそれぞれg~及びh~でrepresentされるとき、ghの原始再帰で定義される関数f:Nn+1Nは次の射f~でrepresentされる。

f~=pN,NeN×N,NnβqNn,N,pNn,N

ただしβ:N(N×N)Nnは、weak NNOの弱普遍性から導かれる次のような射である。
TzNSNββT(g,zoNnqT,Nn)(N×N)Nn(hq(N×N)Nn,Nn,qN,N,pN,NeN×N,Nn,SqN,NeN×N,Nn)(N×N)Nn

今回の主役

A is representable in any CCC with weak NNO.

作れば勝ち。

A:N2Nは射eN,NαpN,N,qN,Nでrepresentされる。

ただしα:NNNは、weak NNOの弱普遍性から導かれる次のような射である。
TzNSNααT(SqT,N)NN(eN,NeNN,NNRNqNN,N,pNN,N,eN,NpNN,N,SzoNN×N)NN

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できることが同値になります。さらにϕ¯では任意の射TNSnzという形をしており、したがって任意の射NnNがなんらかの自然数関数をrepresentしていることが示せます。

Q. 証明に出てきたよくわからん構成どうやって思いついてるの。

A. このくらいならCCCやNNOに慣れたら案外いけるよ。

投稿日:20201212
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。
バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。

投稿者

うお。
うお。
21
2240
趣味の話をするマン。

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中