circ-Kleisli構成

circ-Kleisli構成をきまじめにかつ一気に定義すると、かなり面倒。circ-Kleisli構成＝Circ構成の後にKleisli構成だと思う。このことを確認できれば、話は単純になる。←勘違い、そんなことではない。

現象の観察結果なので、“一気の定義”が先に来てしまった。以下、現象論的定義：

Cはを有限余完備圏として、直和構造(+, 0)で対称モノイド圏とみなす。i, jは直和の標準入射、∇が余対角射だとする。自己関手F:C→Cが、自然変換ε:I→F、μ:FF→Fでモナドになっているとする。自然変換δ_A,B:F(A)+F(B)→F(A+B) は、F(i):F(A)→F(A+B), F(j):F(B)→F(A+B) から δ_A,B = (F(i_A,B)+F(j_A,B));∇_A+B:F(A)+ F(B)→F(A+B)として定義する。δ: +(F(-),F(-)) →F(+(-, -)):C×C→C。δは余分配（変換）とでもいうべきか。

新しい圏Dを次のように定義する。|D| = |C|、α:A+X → F(B+X) in C がDの射:A→Bとする。α:A→B, β:B→C in D（'C'がだぶった、心眼で区別する）とは、α:A+X→F(B+X), β:B+Y→F(C+Y) in Cのこと。α':A+X+Y→F(B+X+Y) in Cは、(α+ε_Y);δで定義する。このδは、F(B+X)+F(Y)→F(B+X+Y)である。同様に、β":B+X+Y→F(C+X+Y) は (B+σ);(β+ε_X);δ;ηとして定義する。σは対称、ηはF(C+Y+X)→F(C+X+Y)の同型。

α'とβ"のKleisli結合*を圏Dでのαとβの結合とする。つまり

• α;β in D = α'*β" in C

ここで、f*g = (f;F(g));μ_C in C。

---

定義の途中で、余対角∇や余分配δが出てくるから、余対角を持つ対称モノイド圏とか余分配を持つモナドとかの条件が付くのだろう。が、計算してないからいまいちハッキリしない。

モナドFは色々変化させたい。モナドFに従ってcirc-Kleisli(F)も変わる。C上の全モナドは比較や構成を射として圏だから、F|→circ-Kleisli(F)は、Monad(C)→Ext(C)のような関手となるだろう。Ext(C)はCの拡張圏の圏。これは、現象的には、

• 「プログラミング言語を作ると、インターフェースの実装手段が得られる」
• 「プログラミング言語のあいだの翻訳規則があれば、実装の変換手段も対応して作れる」
• 「プログラミング言語にはIDLからのマッピング（言語バインディング）が必要」
• 「マクロ展開＝構文的代入が潜在的に存在する」
• 「言語間翻訳では、言語バインディングとマクロ展開が保存されるべき」

などなど。

IDL、CDL(constraint def./desc. language)の意義や使い道はいちおう分かった。プログラミング言語とデータ記述言語、エルブラン型定理との関係をハッキリさせたい。公理的意味論≒プログラム証明はうまくいかない気がしているのだが、その理由が知りたい。プログラム証明をやるには、プログラミング言語に推論規則が最初から付いている必要がある -- が、それっていったいどういうことだ？

どうでもいいけど、インスティチューションはSignを中心とした村だな。村と村の交通／交流が必要だ。町村合併とかも。