トレース、ダガー、スター

トレース付きモノイド圏（対称性は当然に仮定）がデカルトのとき、f:A×X→Xの不動点f^†は次のように定義できる。

• f^† = Tr^X_A,X(f;Δ_X)

さらに双デカルトなら、f:X→X の繰り返し（repetition）f*は：

• f* = Tr^X_X,X(∇_X;f;Δ_X)

これらから、双デカルト・モノイド圏では：

• f* = (∇;f)^†

逆に、スターでダガーを定義できる。f:A×X→Xのとき

• f^† = ((Δ_A+X);(A+f))*

ダガーによるトレースの定義は：

• Tr^X_A,B(f) = (π¹_2A,B;f)^†;π²_2B,X

ここで、π¹₂、π²₂は、それぞれ第一、第二射影（直積因子は２つ）。

これらは、絵算を使った“次元解析”で直観的かつ容易に得られる。

起源は誰だ

繰り返しを表すスターはKleeneスターと呼んでよいだろう。ダガーのほうは誰を起源とすべきか？ Cazanescu/Stefanescu（カザネスク／ステファネスク）は"Feedback, iteration and repetition"のなかで、Elgot's iteration (dagger) と言っている。一方、Hyland/Bentonの"Traced Premonoidal Categories"では、圏論的に都合がいい不動点オペレータはConwayオペレータと呼んでいる。Conwayオペレータ公理：

• [対角自然性] f:A×U→V, g:U→V に対して、(f;g)^† = (A×g;f)^†;g
• [対角性(diagonal prop.)] f:A×U×U→Uとして、(((A×Δ);f)^† = (f^†)^†

適当な条件化で、圏CのConwayオペレータは、半環End(U)（U∈C）上の単項演算^†で、次のConway等式を満たすものに対応するらしい。

• (ab)^† = 1 + a(ba)^†b
• (a + b)^† = (a^†b)^†a^†

仮にそういう半環をConway代数とすると、「Conway圏⇔Conway代数」ってことだね。同様なことは「Kleene圏⇔Kleene代数」でも起きるのだろうか？まー、Kleene圏の定義次第だな。フロベニウス代数でも同じようなことがあったな。行列Lawvere理論と関係しそうだ。Cazanescu/Stefanescu、Gadducci/Corradini（カザネスク／ステファネスク／ガダッチ／コラディニ）がだいたいやっていると思うが。

んで結局、ダガーはElgotダガーかConwayダガーか？ Elgot/Conway（エルゴット／コンウェイ）ダガーにするか？