運算的振る舞い関手

僕の作業仮説であるマンダラ仮説だと、計算の世界は複雑だ。単純化しすぎた定式化はうまくいかないだろうと思っている。だが、扱いにくい複雑性ではどうにもならない。扱いやすい「単純な複雑さ」を探さなくてはならない。

今知っている具体例から抽象して、次のような枠組みを考えている。

1. 二重圏Diag：図の圏。コボルディズム圏がお手本になっている。
2. 二重圏Mat：行列の圏。順序半環係数の行列の圏がお手本になっている。
3. 二重関手CB:Diag→Mat：ファインマン／クリーネ総和による計算がお手本になっている。

二重圏の各次元のセルは次のように解釈する。

1. 0セル：境界、入出力ポート／ピン
2. 1セル：グラフ、オートマトン、ラベル付き遷移系、カテグラフ、圏ラベル付きタングルなど
3. 2セル：模倣関係、書き換え、変形、移動（move）など

二重圏の水平方向（ってどっちだ？）の1-骨格(1-切り落とし）には半環構造が入っていて、半環圏になっている。2セルは半環構造と協調している。

幾つかの問題がある。

1. ペトリネットをどうやって取り入れるか。拡張が必要かもしれない。
2. ペトリネットと関係しそうだが、時間概念をどうするか。
3. マイヒル／ネロードの定理の定式化
4. 正規形の定義や合流性の証明
5. ステファネスクの基本定理の証明

「ステファネスクの基本定理」は僕が命名したものだが、だいたいは次の主張。

• トレース付き対称モノイド圏MとVがあるととき、M→V というトーレス付きモノイド関手の全体は再びレース付き対称モノイド圏となる。

もともとの記述は、「networksに圏係数を付けて拡張してもnetworksになる」といった話でちょっと曖昧なところがある。必要に応じて係数を拡張できる、という意味では非常に重要なことだと思う。

TrSySMonをトレース付き対称厳密モノイド圏の圏（レルム）として、TrSySMon(A×B, C) ≒ TrSySMon(A, [B,C]) という閉構造として定式化できるとうれしいが、×の定義が素朴じゃない気もする。仮に閉構造の形になっても、2セルとどう関係するかが問題だし。

それと、加法的なトレースはエルゴット繰り返しなのはわかるが、乗法的トレースがよくわからない。インターフェースの隠蔽がそれにあたる気もするが。