リファクタリングとPインスティチューション
Fが圏C上のモナドだとして、DがFのKleisli圏だとする。f∈C(A, B)に対して、fにモナド単位εB:B→F(B)を後結合すれば、B-resulticな射f':A→F(B)ができる。これを使えば、CをDに埋め込めるから、C⊆Dと考えてよい。この埋め込みを込めて、DをCのKleisli F-拡張とも呼ぶことにする。
Pインスティチューションでは、圏Progは圏SignのKleisli拡張になっている。Σ、Γを指標として、射p∈Prog(Σ, Γ)は、"uses Γ, provides Σ"なプログラムである。pの“意味”（varianceは反変）は、ModΓ→ModΣ の関手として与えられるはずだから、localには、Prog(Σ, Γ)→Functor(ModΓ, ModΣ)という写像がある。
ところで、Functor(ModΓ, ModΣ)は、関手を対象、自然変換を射として、so-called縦結合の圏になる。とするなら、Prog(Σ, Γ)も圏になっていて、localにProg(Σ, Γ)→Functor(ModΓ, ModΣ)が関手になっているのが望ましい。
で、問題はProg(Σ, Γ)はどんな圏か？ 対象はソースコードだから、射は明らかにプログラム変換。ΣとΓでしばられているから、勝手な変換ではない。制約（セオリー）が入ることを考えると、外部仕様を変えないプログラム変換となる。つまり、世間的に言えばリファクタリングだ。
モデルの実体として余代数（オートマトン、トランスデューサなど）を考えると、リファクタリングは振る舞い同値、観測的弁別不可能性を導くから、ツジツマはあっている。Progは、localに圏になっているから、Cat-enriched categoryで、双圏（だから2-圏だか）になる。
- 0セル -- 指標、仕様
- 1セル -- プログラム
- 2セル -- リファクタリング
Mod側では、
- 0セル -- モデル圏
- 1セル -- 関手
- 2セル -- 自然変換
となる。具体的実体に移って：
- 0セル -- 入出力領域（境界）
- 1セル -- 余代数
- 2セル -- 余代数の準同型
終対象を取れば、1セルは状態空間の点になり、2セルが状態遷移になるのだろう（たぶん、イマイチわからん？）。ただし、代数仕様と余代数仕様を整合させる問題は残っているし、振る舞い関手も定義してない。
終対象はモジュライに似ているし、双圏構造はコボルディズムやホモトピーと似ている。アティヤのTQFT公理にもほぼ合致する -- やっぱり計算現象は物理的・幾何的現象なのかもしれないな。
ウーム、どっから攻める？ 嗚呼、物理が分かっていれば手持ち道具がもっとあるだろうに、無念。
