トレースと不動点 -

Traced Premonoidal Categoriesを読んだ。ある種のモノイダル圏では、traceと不動点作用素(正確には、parametrized fixpoint operatorでConway作用素と呼ぶらしい)が本質的に同じものだという、なんか不思議な話。

元々は、traced monoidal categoryの定義を探してたのだけど、ここでの定義は、symmetricityを課しているので、ダメだった。symmetricityを仮定しないtraced monoidal categoryの定義があるのかどうかは知らない(Joyal,Streetはbraidingの重要性をかなり早い時期に気付いてた人(というか、圏論的な文脈に限れば最初に言い出した人かもしれん)なので、symmetricityを仮定するようなことはしない気もするけど)。まあ、数学的に見ると、symmetricityは強すぎる制限だと思うのだけど、CS的には、symmetricityを仮定しない方が、むしろ過剰な一般化だよな〜

Haskellで言うと、MonadFixクラスに属するmonadから、「Kleisli構成」によって、得られるArrowはArrowLoopクラスに属する、というような感じのことらしい(mfixはparametrized fixpoint operatorではないけども)。

MonadFixの定義は
http://web.mit.edu/ghc/www/libraries/base/Control.Monad.Fix.html#t%3AMonadFix
から

class Monad m => MonadFix m where
mfix :: (a -> m a) -> m a

で、Instances of MonadFix should satisfy the following laws:

(1)(purity)
 mfix (return . h) = return (fix h) 
(2)(left tightening))
 mfix (\x -> a >>= \y -> f x y) = \y -> mfix (\x -> f x y) 
(3)(sliding)
 mfix (liftM h . f) = liftM h (mfix (f . h)), for strict h. 
(4)(nesting)
 mfix (\x -> mfix (\y -> f x y)) = mfix (\x -> f x x)

ということらしい。mfixの公理は、Recursive Monadic Bindingsで与えられたっぽい。

ArrowLoopの方は、

class Arrow a => ArrowLoop a where
loop :: a (b, d) (c, d) -> a b c

instance ArrowLoop (->) where
	loop f b = let (c,d) = f (b,d) in c

instance MonadFix m => ArrowLoop (Kleisli m) where
	loop (Kleisli f) = Kleisli (liftM fst . mfix . f')
		where	f' x y = f (x, snd y)

で、loopが満たすべき公理ってのは、論文の定義2.4をそのままHaskellで書き直すと

(1)(Left Tightening)
loop ((first g)>>>f) = g>>>(loop f)
(2)(Right Tightening)
loop (f>>>(first g)) = (loop f)>>>g
(3)(Dinaturality/sliding)
loop (f>>>(second g)) = loop ((second g)>>>f)
(4)(Action/Vanishing)
loop ((arr fst)>>>f>>>(arr rho')) = f where rho' x=(x,())
loop f = loop (loop ((arr c)>>>f>>>(arr c')))
 where
  c((x,y),z)=(x,(y,z))
  c'(x,(y,z))=((x,y),z)
(5)(Superposing)
loop ((arr c)>>>(second f)>>>(arr c')) = second (loop f) 
 where {c((x,y),z)=(x,(y,z)); c'(x,(y,z))=((x,y),z)}
(6)(Yanking)
loop (arr swap) = (arr id) where swap(x,y)=(y,x)

かな(合ってると思うが)。mfixが上の公理(+monadの定義)を満たすとき、そっから作ったloopが下の公理を満たすかどうかは確認してない(そのうちやる)

・HaskellでConway operatorに相当するものって、どう作ればいいんだろう

・最初の方のfootnoteで
We should note that fixIO does not actually satisfy the axioms we will propose.
と書かれてるのは、多分
Value Recursion in Monadic Computations
Semantics of fixIO
あたりの話。Continuation Monadの場合も、mfixの構成は微妙らしい
Value recursion in the continuation monad
話を消化しきれてないので、ただのリンク集

おまけ。ribbon categoryはtraced monoidal categoryになるかどうか。ribbon categoryの定義と、その周辺概念と記号は
http://d.hatena.ne.jp/m-a-o/20070215#p3
を参照。ここでは、数学的な目的意識を持ってたので、k-liearityを仮定してたけども、そのほとんどは、k-linearであるという仮定は本質的でないので、CSでもなんか役に立つかもしれないし、役に立たないかもしれない。まあ、どうでもいい。

まあ、基本的にざくざくと計算していくだけなのだけど、Left Tightening,Right Tightening,Vanishingあたりは成り立つっぽい。SuperposingとDinaturalityは見てない。Yankingが(symmetricityを仮定しても)できなかった(もうちょっとよく考える)

トレースの定義だけ、もう一回書いておく。
$Tr^{U}_{A,B}(f) = (id_{A} \otimes i_{U}) \circ (f \otimes id_{U^{*}}) \circ (id_{B} \otimes d_{U} \otimes id_{U^{*}}) \circ (id_{B} \otimes e_{U^{*}}) \hspace{3} (f:A \otimes U \rightarrow B \otimes U)$

texで書こうとしたけど、なんかキモイのでやっぱやめた。記号。i[A]とかの代わりに、i_Aと書いたり。あと、射の合成は、Haskell風な.ではなくて、;を使うことにする。*はテンソル積、Iは単位対象。f:A->Bと書く代わりに、f:Hom(A,B)と書くかもしれない。以下、left tighteningの証明。多分合ってると
f: Hom(A'*U , B*U)とg: Hom(A,A')について、



Tr^U_A,B((g*id_U);f) = g;Tr^U_A',B(f) <=>

(id_A*i_U);(((g*id_U);f)*id_U^);(id_B*d_U*id_U^);(id_B*e_U^) = g;(id_A'*i_U);(f*id_U^);(id_B*d_U*id_U^);(id_B*e_U^)<=

(id_A*i_U);(((g*id_U);f)*id_U^)=g;(id_A'*i_U);(f*id_U^)<=>

(id_A*i_U);(g*id_U*_U^);(f*id_U^)=g;(id_A'*i_U);(f*id_U^)<=

(id_A*i_U);(g*id_U*_U^) = g;(id_A'*i_U)<=>

g*i_U=g*i_U