自然数対象を持つカルテシアン閉圏の一般論の中でアッカーマン関数を構成する。

一方、圏論的に「自己参照 (self-reference)」の概念を考えることができないわけでもなく、「ローヴェアの不動点定理 (Lawvere's fixed-point theorem)」で説明されるような射の不動点として、特定の写像を繰り返し終わりなく合成し続けて得られるような要素の概念の定式化は可能である。

そういった理由もあり、アッカーマン関数の実装に使用する関係式には以下の

\[ A(m,n) = \begin{cases} n+(m+1) & \text{ if } m=0,1 \\ 2\uparrow^{m-2}(n+3) - 3 & \text{ otherwise } \end{cases} \]

を採用する。

アッカーマン関数を構成するうえでの障壁

まずポイントとなるのは、周囲圏として想定しているのは「カルテシアン閉圏」であるため、トポスが持つような強力な論理式の組み立て機構が無いという点である。

とはいえ、C言語のようなプログラミング言語と同様に

0 を偽
0 以外を真

というように考えることで、ブール論理演算を自然数の間の演算として表すことはできる。

これを上手く使って、条件分岐を含むような自然数に関する写像の構成が実現できる。

余談

この数を使ったブール論理は、もちろんトポスの一般論の中で展開される直観主義論理とは異なる。

条件分岐を自然数の演算で無理やり実装する

論理和

論理和は、単に自然数の和として与えることができる。

\[ m \>|\,|\> n = n+m \]

つまり

\[ (|\,|) = (+_{{\mathbb{N}}}) \]

論理積

論理積は、単に自然数の積として与えることができる。

\[ m \>\&\&\> n = n\cdot m \]

つまり

\[ (\&\&) = (\cdot_{{\mathbb{N}}}) \]

否定

否定は、次の関係式

\[ m-n = \begin{cases} m-n & \text{ if } m \le n \\ 0 & \text{ otherwise } \\ \end{cases} \]

を満たすような (つまり、計算結果を与えるのに負の数が必要になる組み合わせの場合、全て 0 を出力するように振舞いを設定した) 引き算を構成できれば、以下の

\[ {\rm Not}(x) = 1 - x \]

という関係式を満たす写像として定義できる。

写像の具体的な構成についてだが、引き算の方についてはまず以下のように前者関数 (Predecessor)

\[ {\rm pred} = {\rm rec}_{{\mathbb{N}}}(\langle {\rm zero}, {\rm zero} \rangle, \langle {\rm prj}_2, {\rm prj}_2 {\sf \, ⨟ \,} {\rm succ} \rangle) {\sf \, ⨟ \,} {\rm prj}_1 \]

を構成した後、足し算の時と同じ要領で

\[ ({-}_{\mathbb{N}}) = {\rm tw} {\sf \, ⨟ \,} ({\rm rec}_{{\mathbb{N}}}({\rm arrToEl}({\mathbb{N}}),\lambda[{\rm ev} {\sf \, ⨟ \,} {\rm pred}])\times {\mathbb{N}}){\sf \, ⨟ \,} {\rm ev} \]

というように構成することができる。

よって否定 \({\rm Not}\) は

\[ {\rm Not} = \langle {\rm const}(1), {\mathbb{N}} \rangle {\sf \, ⨟ \,} ({-}_{\mathbb{N}}) \]

となる。

順序関係

自然数の順序を判定する写像は、否定のセクションで定義した引き算と否定を用いた以下の関係式を満たすものとして構成できる。

\[ m \le' n = {\rm Not}(m-n) \]

つまり

\[ (\le') = ({-}_{\mathbb{N}}) {\sf \, ⨟ \,} {\rm Not} \]

である。

相等関係

相等関係は順序と論理積を使って

\[ m ==' n = (m\le' n)\>\&\&\>(n \le' m) \]

と与えることができる。

つまり

\[ (==') = \langle(\le'),{\rm tw}{\sf \, ⨟ \,} (\le')\rangle{\sf \, ⨟ \,} (\&\&) \]

条件分岐

自然数で表された真偽を規格化する以下の関係式

\[ {\rm normalize}(t) = \begin{cases} 0 & \text{ if } t = 0 \\ 1 & \text{ otherwise } \\ \end{cases} \]

を満たす写像 \({\rm normalize}\) を定義できれば \({\rm if'}\) は

\[ {\rm if'}(t,m,n) = {\rm normalize}(t)\cdot m + {\rm normalize}({\rm Not}(t))\cdot n \]

を満たすものとして与えることができる。

写像の具体的な構成についてだが、\({\rm normalize}\) は

\[ {\rm normalize} = {\rm rec}_{{\mathbb{N}}}(\langle {\rm zero}, {\rm zero} {\sf \, ⨟ \,} {\rm succ} \rangle, \langle {\rm prj}_2, {\rm prj}_2 \rangle) {\sf \, ⨟ \,} {\rm prj}_1 \]

として構成できるので、よって

\[ {\rm if'} = \langle \langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm normalize}, {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_2\rangle {\sf \, ⨟ \,} ({\cdot}_{{\mathbb{N}}}),\langle {\rm prj}_1 {\sf \, ⨟ \,} {\rm prj}_1 {\sf \, ⨟ \,} {\rm Not} {\sf \, ⨟ \,} {\rm normalize},{\rm prj}_2\rangle {\sf \, ⨟ \,} ({\cdot}_{{\mathbb{N}}}) \rangle {\sf \, ⨟ \,} ({+}_{{\mathbb{N}}}) \]

となる。

余談

ここで定義した If-Else 分岐は、「出力が自然数でなければならない」という縛りがあるが、周囲圏に課される仮定に「全ての有限余積が存在する」という条件を追加で含めれば、「圏論的にIf文を組み立てる」で説明するような縛りの少ないバージョンの「if」を構成することが可能となる。

条件分岐のある式を一行の式へ変形する

これらの写像を用いると、アッカーマン関数が満たすべき関係式を以下のように書き換えることができる。

\[ A(m,n) = {\rm if'}(m ==' 0 \>|\,|\> m ==' 1, n + (m+1), 2\uparrow^{m-2}(n+3) - 3) \]

ここまでできればあとはいつも通り、式変形することで

\[ \begin{align} A(m,n) &= {\rm if'}(m ==' 0 \>|\,|\> m ==' 1, n + (m+1), 2\uparrow^{m-2}(n+3) - 3) \\ &= \langle m,n \rangle {\sf \, ⨟ \,} (\langle \langle \langle \langle {\rm prj}_1, {\rm const}({\rm zero}){\sf \, ⨟ \,} (=='), \langle {\rm prj}_1, {\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} (==') \rangle {\sf \, ⨟ \,} (|\,|),\langle {\rm prj}_1,\langle {\rm prj}_2,{\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} ({+}_{{\mathbb{N}}})\rangle {\sf \, ⨟ \,} ({+}_{{\mathbb{N}}}) \rangle,\langle \langle \langle {\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ}),\langle {\rm prj}_2,{\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} ({+}_{{\mathbb{N}}})\rangle ,\langle {\rm prj}_1,{\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} ({-}_{{\mathbb{N}}})\rangle {\sf \, ⨟ \,} {\rm tower},{\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} ({-}_{{\mathbb{N}}}) \rangle {\sf \, ⨟ \,} {\rm if'}) \end{align} \]

よって

\[ A = \langle \langle \langle \langle {\rm prj}_1, {\rm const}({\rm zero}){\sf \, ⨟ \,} (=='), \langle {\rm prj}_1, {\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} (==') \rangle {\sf \, ⨟ \,} (||),\langle {\rm prj}_1,\langle {\rm prj}_2,{\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} ({+}_{{\mathbb{N}}})\rangle {\sf \, ⨟ \,} ({+}_{{\mathbb{N}}}) \rangle,\langle \langle \langle {\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ}),\langle {\rm prj}_2,{\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} ({+}_{{\mathbb{N}}})\rangle ,\langle {\rm prj}_1,{\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} ({-}_{{\mathbb{N}}})\rangle {\sf \, ⨟ \,} {\rm tower},{\rm const}({\rm zero}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ}{\sf \, ⨟ \,}{\rm succ})\rangle {\sf \, ⨟ \,} ({-}_{{\mathbb{N}}}) \rangle {\sf \, ⨟ \,} {\rm if'} \]

Haskell での動作確認

グラハム数の時と同様、以上の定義を見ても信じ難いと思うので Haskell でちゃんと検証しておく。

以下のコードの実行例

ghci> printEl $ pair(nat(2),nat(2)) -: ackermann
7
ghci> printEl $ pair(nat(2),nat(3)) -: ackermann
9
ghci> printEl $ pair(nat(1),nat(3)) -: ackermann
5
ghci> printEl $ pair(nat(3),nat(3)) -: ackermann
61
ghci> printEl $ pair(nat(4),nat(1)) -: ackermann
65533
ghci> printEl $ pair(nat(4),nat(0)) -: ackermann
13
ghci> printEl $ pair(nat(5),nat(0)) -: ackermann
65533

からわかるように、

\[ \begin{align} A(2,2) &= 7 \\ A(2,3) &= 9 \\ A(1,3) &= 5 \\ A(3,3) &= 61 \\ A(4,1) &= 65533 \\ A(4,0) &= 13 \\ A(5,0) &= 65533 \\ \end{align} \]

が正しく計算できていることの確認ができる。

ソースコード

{-# LANGUAGE TypeOperators #-}

import Data.Void

main :: IO ()
main = do
  printEl $ pair(nat(2),nat(2)) -: ackermann
  printEl $ pair(nat(2),nat(3)) -: ackermann
  printEl $ pair(nat(1),nat(3)) -: ackermann
  printEl $ pair(nat(3),nat(3)) -: ackermann
  printEl $ pair(nat(4),nat(1)) -: ackermann
  printEl $ pair(nat(4),nat(0)) -: ackermann
  printEl $ pair(nat(5),nat(0)) -: ackermann


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

pred' = rec_N(pair(nat(0),nat(0)), pair(prj2, prj2 -:succ')) -: prj1
sub_N = tw-:(rec_N(arrToEl(_Nat), trans(ev-:pred'))***_Nat)-:ev

ackermann =
  pair(pair(pair(pair(prj1,const'(nat(0)))-:eq',pair(prj1,const'(nat(1)))-:
  eq')-:or',pair(prj1,pair(prj2,const'(nat(1)))-:add_N)-:
  add_N),pair(pair(pair(const'(nat(2)),pair(prj2,const'(nat(3)))-:
  add_N),pair(prj1,const'(nat(2)))-:sub_N)-:tower,const'(nat(3)))-:sub_N) -: if'

true :: Pt -> Nat
true = nat(1)

false :: Pt -> Nat
false = nat(0)

if' :: (Nat *** Nat) *** Nat -> Nat
if' =
  pair(pair(prj1-:prj1-:normalize, prj1-:prj2)-:mul_N, pair(prj1-:prj1-:
  not'-:normalize,prj2)-:mul_N)-:add_N

le' :: Nat *** Nat -> Nat
le' = sub_N -: not'

eq' :: Nat *** Nat -> Nat
eq' = pair(le',tw-:le')-:and'

not' :: Nat -> Nat
not' = pair(const'(nat(1)),id) -: sub_N

and' :: Nat *** Nat -> Nat
and' = mul_N

or' :: Nat *** Nat -> Nat
or' = add_N

normalize :: Nat -> Nat
normalize = rec_N(pair(nat(0),nat(1)), pair(prj2, prj2)) -: prj1

Show ALL

タグ: 数学圏論 Haskell

タグ一覧:

物理学 (18)
古典力学 (9)
量子力学 (5)
数学 (56)
圏論 (32)
位相 (1)
線形代数 (7)
高校数学 (4)
プログラミング (28)
C言語 (4)
Haskell (32)
Java (1)
Python (2)
PureScript (3)
日記 (40)
小ネタ (17)
音楽 (4)
ピアノ (12)
ゲーム (18)
YouTube (36)

ページの先頭へ

TakuLabo

自然数対象を持つカルテシアン閉圏の一般論の中でアッカーマン関数を構成する。