Categorical Programming(3)

CPL/CHARITYでは、CoListとunfoldが定義できるはずなので、無限リストを生成するとかすると、停止しない計算が書けてしまうんじゃなかろうかという気がする

http://d.hatena.ne.jp/m-a-o/20091101#p2
から続き。

その1。CPLの原論文でCartesian Closed Categoryがnatural number objectを持つとき、足し算は、
add = apply . (iter(curry(pi2) , curry(succ . apply)) × id_Nat)
というように書けるとある。

微妙に記号を変えたけど、iterはNatに対するfold関数。Iはterminal object(直積の単位対象)。(.)は射の合成。全部型を書くと
iter : Hom(I,X) × Hom(X,X) -> Hom(Nat , X)
pi2 : Hom(A × B , B)
succ : Hom(Nat , Nat)
curry : Hom(A × B , C) -> Hom(A , B => C)
apply : Hom((B => A) × B , A)
id_Nat : Nat -> Nat
ついでに、
zero:Hom(I , X)
で、iter(zero , succ) = id_Nat
iterの型は、Hom(I+X,X)->Hom(Nat,X)の方がいいけど、あんま細かく書くとめんどい

Haskellだと、Homと->と=>は区別されず、敢えて明示的にcurry化まで書くと

import Prelude hiding (curry)

data Nat = Zero | Succ Nat deriving Show

apply(f,x) = f x
iter(z , f) Zero = z()
iter(z, f) (Succ n) = iter((\_ -> f $ z ()), f) $ n
pi2(x,y) = y
curry f = (\x -> \y -> f(x,y))
prod(f,g) = (\(x,y)->(f x , g y))

add = apply . prod(iter(curry(pi2) , curry(Succ . apply)) , id)

上の定義を見ても、ぱっと見て足し算だとは(少なくともわたしには)分からないのだけど、Haskellであれば

add(n,m) = iter(\_->n , Succ) m

と書くのが自然で分かりやすい。けど一般の圏ではXとI=>Xは同型になるけど、何の仮定もなしにHomとinternal homを関係付けることができないので、(\_->n)に相当するものを作ることができないので、上のような定義になっているんだと思う

Charityでは

def add: nat * nat -> nat
       = (m,   n)  => {| zero: () => n
                       | succ: x  => succ x
                       |}
                          m.

で済むらしい

あと、上のpi2の型は、Hom(I × Nat , Nat)なので、一般のsymmetric monoidal closed categoryでも足し算くらいはできる。foldとunfoldがあるので、symmetric monoidal closed categoryでもcartesian closed categoryと「同じ計算能力がある」かもしれない

その2。高階原始帰納関数の正確な定義はよく分からないけど、Ackermann関数は、頑張るとiterを使って書ける。

ack 0 n = n + 1
ack m 0 = ack (m-1) 1
ack m n = ack(m-1) $ ack m (n-1)

で、これは

ack Zero = Succ
ack (Succ m) = iter(\_->(ack m (Succ Zero)) , ack m)

で、もう一段頑張ると

ack = iter(\_->Succ , \f -> iter(\_ -> (f $ Succ Zero) , f))

パズルの世界。不安なので、普通にHaskellで書いておくと

iter x f 0 = x
iter x f (n+1) = iter (f x) f n
ack = iter (+1) (\f-> iter (f 1) f)