トレース分解定理：概略

「繰り返しx*と強い繰り返しx+、長谷川の不動点補題」で言及した定理をトレース分解定理と呼ぶことにする。かなり一般的／周知の事実なので、個人名を冠するのはふさわしくない、と思い直した。

さて、このトレース分解定理によれば、デカルト圏のトレースはトランスデューサであることが分かる。双対的に、余デカルト圏のトレースは余トランスデューサである。これから、Elgotダガー／Elgotオートマトンとコンウェイ（Conway）ダガー／Conwayオートマトン（簡易トランスデューサ）の双対性も従う。トレース分解定理は、トレース付き（余）デカルト圏の構造を具体的に決定してしまう。

トレース付きデカルト圏の基本

ここでいうデカルト圏とは、極限としての終対象／直積を持つ圏というよりは、等式的に定義されるΔ（対角射、重複器）と⊥（弱終射、放電器）を持つ対称モノイド圏である。セリンガーによるcategory with diagonals、あるいはGSモノイド圏などと同じ定式化だ。Δと⊥はコモノイドの族を定義して、さらにすべての射はコピー可能／破棄可能であるとする。

射影をπ¹_A,Bのように書くとして、f:X→A×Bに対して、f¹ = f;π¹_A,B:X→A などと書く。デカルト圏では次の表現が得られる。

• f = <f¹, f²> = Δ;(f¹×f²)

これを絵に描いてルーピングさせるとトレースの表現が得られる。

コンウェイ（Conway）不動点との関係を見るためには次の絵算を使う。ループ、分岐、交差を持つ図から、分岐をループに沿ってスライドさせて交差を取り除く操作である。