シーケントとスパイダー計算

スパイダー計算 ＝ シーケント計算の絵算版 ですな。

スパイダーは多圏または複圏の射だけど、一般の多圏／複圏を考えるのではなくて、ベースとなるモノイド圏Cの上でスパイダーを考える。

マニンのファインマン図の用語法を使うなら、スパイダーはカローラになる。1個の頂点とフラグの集合だ。が、有向グラフなので、フラグは有向半辺となる。入力ワイヤー群と出力ワイヤー群に完全に分かれる。有向カローラと呼ぶべきか？

Cが2つのモノイド積を持つ圏とする。ただし、2つの積が一致していてもよい（コンパクトなケース）。有向カローラがあるとき、頂点にCの射、有向フラグにCの対象を割り当てた図形がスパイダー。次の条件（意味論条件）を満たす。

• 入力フラグのラベルすべてに渡る第一モノイド積は、射の域になっている。
• 出力フラグのラベルすべてに渡る第ニモノイド積は、射の余域になっている。

コンパクトなケースでは、タングルの計算に近いが、非コンパクト（2つの積が異なるとき）は古典論理のシーケント計算に近くなる。スパイダーの全体が、スパイダー計算によりどんな圏（多圏、複圏）になるか？が最初の問題。ステファネスクの基本定理（ネットワークの圏に値を取るネットワークの全体は再びネットワークの圏になる）と同じスタイルの基本定理が成り立つとうれしい。