2009-10-20

A survey of graphical languages for monoidal categories

http://d.hatena.ne.jp/m-a-o/20090914#p2
の続き。lemma5.7(c)の"algebraic proof"

前回の式は間違いがあったので、修正。

一応、これで合ってると思うけど、複雑すぎ。以下のように読むのが「正しそう」(式としては、等価であるはずだけど)

証明をきちんと書こうと思ったけど、一部埋まらん。

(1)=(2)は、以下の変形で言える。
[tex:Tr_L^A(f \otimes id_A) = Tr_L^A*1]
これは、braidingのnaturalityから従う。最後に、Left Traceのtightening公理を適用して、式(2)を得る。

(2)=(3)は
$Tr_R^B(c_{B,A \otimes B}^{-1}) \circ Tr_L^B(c_{B,B \otimes A}) = c_{A,B}^{-1} \circ (id_A \otimes Tr_R^B c_{B,B}^{-1}) \circ c_{A,B} \circ (Tr_L^B c_{B,B} \otimes id_A)) = \\ (Tr_R^B(c_{B,B}^{-1}) \circ Tr_L^B(c_{B,B})) \otimes id_A$
から。
$Tr_R^B(c_{B,B}^{-1}) \circ Tr_L^B(c_{B,B}) = id_B$
の証明もきちんと書く必要がある

(3)=(4)が、謎。絵では、分かるけど、式で書こうとすると???

(4)=(5)は、
[tex:Tr_L^X(c_{X,X}) \circ f = Tr_L^X(c_{X,X} \circ (id_X \otimes f)) = Tr_L^X*2 = f]
where $f:I \rightarrow X=A \otimes B$
が成り立つので。等号は、順に、tightening公理,naturality of braiding,sliding公理,vanishing公理による

(5)=(6)は、(1)=(2)の変形と同様。

*1:f \otimes id_A) \circ c_{I,A})=Tr_L^A(c_{A,A \otimes B} \circ (id_A \otimes f

*2:f \otimes id_X) \circ c_{I,X}) = Tr_L^I(c_{X,I} \circ (f \otimes id_I

2009-10-20

rigid category+α

概念の整理。

0)rigid monoidal category
left dualとright dualを持つmonoidal categoryをrigidと呼ぶ

#A survey of graphical languages for monoidal categories
http://arxiv.org/abs/0908.3347
では、autonomousと呼ばれてるけど、rigidと書いてあることが多い気がする。

1)pivotal category:
rigid monoidal categoryで $A \simeq A^{**}$ が成り立つもの(正確には、もうちょっと条件が付く)
$A^{*}$ は、Aの右双対であると同時に、 $A^{*}$ は $A^{**} \simeq A$ の左双対なので、pivotal categoryでは、右双対と左双対が同一視できる
pivotal categoryには、自然にleft traceとright traceが定義できる

2)spherical category:
pivotal categoryでleft traceとright traceが一致するもの

#traceの定義は、「型」によって2種類ある。素朴なEnd(X)->End(I)という「型」のものと、 $Hom(A \otimes X , B \otimes X) \rightarrow Hom(A,B)$ (right traceの場合)という型のもの。前者は、後者の特殊化だけれども、前者のright traceとleft traceが一致することを意味する。

#spherical categoryの初出は、
Spherical Categories
http://arxiv.org/abs/hep-th/9310164
で、Turaev-Viro理論を定式化しようという試みだったらしい。spherical Hopf algebraの定義もここにある。spherical categoryとそのDrinfeld centerについて、前者のTuraev-Viro theoryと後者のReshetikhin-Turaev theoryは等価になるという予想がある

3)ribbon category:
rigid braided monoidal categoryで、twistという構造を持つもの

#twistはbalancing isomorphismと呼ばれることもある(あった?)。ついでに、ribbon categoryはtortile categoryと呼ばれてることもある

(2012.9.16追記)
ribbon categoryは、braided spherical categoryと同じものなので、そのように定義するのが、分かりやすいように思う。

braided spherical categoryに対して、twistは
$\theta_X = (id_X \otimes \epsilon_{X^{*}}) \circ (c_{X,X} \otimes id_{X^{*}}) \circ (id_X \otimes \eta_{X})$
で定義される。但し $c_{X,X}$ はbraiding、 $X^{*}$ は双対、
$\epsilon_X : X^{*} \otimes X \to I$
$\eta_X : I \to X \otimes X^{*}$
で、途中で、pivotal categoryの定義から従う同型 $X \simeq X^{**}$ を暗に使っている。これは、上に書いた、"partial trace" $Hom(A \otimes X , B \otimes X) \rightarrow Hom(A,B)$ をbraidingに適用したものになっている

twistを持つrigid braided monoidal categoryが、pivotalであることは、braidingとrigidityから
$X \simeq X \otimes (X^{**} \otimes X^{*}) \simeq X^{**} \otimes (X \otimes X^{*}) \simeq X^{**}$
という同型射が作れる。これの前にtwistをくっつけたものは、natural isomorphism $X \simeq X^{**}$ を与える。これから、少なくともleft traceとright traceは作れる。sphericalであることの証明は簡単な計算

以上より、以下の包含関係が成り立つ
・ribbon = braided spherical (=> braided pivotal) => spherical => pivotal (=> rigid traced)

Hopf代数のmoduleの圏は、pivotalではあるけれど、一般にはribbon structureも入らないし、sphericalでもなく、圏の概念に対応して、spherical Hopf algebraとかribbon Hopf algebraとかが定義される。当然、ribbon Hopf algebraはspherical Hopf algebraになる。けど数学では大抵の場合、(abelian) ribbon category+αを考えてれば事足りる気がする

数学の場合、rigidである(どころかpivotalである)ことは基本的な要請であるけれども、プログラムの世界では、rigidであることは特に必須ではないと思う。代わりに(?)、物事は大抵symmetricな世界で話が進む。symmetricだと、そもそも色々な話は極めて簡単。
Traced Monoidal Categories
http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=2102776&fulltextType=RA&fileId=S0305004100074338
には、Traced Monoidal Categoryの定義と一般化したGoI構成『braided traced categoryは、ribbon categoryに充満忠実に埋め込める』が証明されているらしい(けど、openな文献ではないので読んでない)。特に、symmetric traced categoryは、symmetric rigid category(= compact closed category)に充満忠実に埋め込める。昔どっかで見た構成をおぼろげに思い出すと、対象をペア(X,A)として、(X,A)から(Y,B)への射を $f:X \otimes B \rightarrow Y \otimes A$ の全体とするような圏を考えると、(X,A)のdualが(A,X)で定義できて、Xを(X,I)に埋め込めてetc..という感じだった気がする。半群から群を作るGrothendieck構成の圏論版みたいな感じだけど、これだと、symmetricな場合、tracedの仮定は要らない気がする。braidedの場合は、twistを定義するあたりに、元の圏のtraceが必要なのかもしれないけど、謎

2009-10-20

CPL

メモ。
http://www.tom.sfc.keio.ac.jp/~sakai/hiki/?CPL

論文。Categorical Programming Language
http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf

Charity。
http://pll.cpsc.ucalgary.ca/charity1/www/home.html

論文。About Charity
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.2805
Charity is a categorical programming language based on distributive categories (in the sense of Schanuel and Lawvere) with strong datatypes (in the sense of Hagino)
だそうな。後はまあどうでもいい(酷

とりあえず、CPL。何を言ってるのか理解するのに30分くらいかかったけど、全部普遍性が基礎になってるらしい。

right object prod(a,b) with pair is
  pi1: prod -> a
  pi2: prod -> b
end object;

は「任意の対象xと射f:x->a,g:x->bが与えられているとき、射h:x->prod(a,b)で
pi1.h=f
pi2.h=g
を満たすものが一意的に存在し、これをpair(f,g)と書く」と読むらしい。分かりづらい。

結局、上のように書くと
pair :: (x->a) -> (x->b) -> (x -> prod a b)
prod :: a -> b -> prod a b
pi1 :: prod a b -> a
pi2 :: prod a b -> b
という4つの関数と、
pi1.(pair f g) = f
pi2.(pair f g) = g
という2つの書き換え規則が定義されると考えればいいっぽい？

right objectがあれば、left objectもあって

left object coprod(a,b) with case is
  in1: a -> coprod
  in2: b -> coprod
end object;

は「任意の対象xと射f:a->x,g:b->xが与えられているとき、射h:coprod(a,b)->xで、
h.in1=f
h.in2=g
を満たすものが一意的に存在し、これをcase(f,g)と書く」と読む。

CHARITYの方では、直積は組み込みであるらしい。直和は、

data coprod(A, B) -> X = in1: A -> X
                       | in2: B -> X.

で定義される。

Haskellだと

data Coprod a b = In1 a
                | In2 b

なので、まあ似ている。

とりあえず感想と疑問(論文をちゃんと読めば書いてあるのかもしれないけど)
・圏論の概念を用いているけども、普遍性は「存在すれば一意的」であることしか保証しないのに対して、こっちは定義できるものはなんでも存在できる世界。terminal objectは若干別腹
・Categorical Combinatory Logicのような体系だと、書き換え規則は、天下り的に与えられる(圏論にinspireされたものだけど)のに対して、こっちは書き換え規則は定義から生成されるのが大きな違いっぽい
・CPLの方が、CHARITYよりもprimitiveなとこから始めてるっぽい
・CPLとCHARITYの差は？
・CHARITYは、distributive categoryを基礎にしているらしいけど、CPLではdistributiveあることは保証されない？(そもそも、CHARITYがdistributiveである理由も分かってないけど)
・CHARITYでは、全ての計算は停止するらしいけど、CPLでは?(停止しそうな気はするけど)
・CPLやCHARITYで計算の合流性は保証されるんだろうか？