ベキのKleisli圏とKleisli圏のベキは違う

過去のエントリーを読み直した。

• ウッギャーッ！！ テンプレートを忘れてた - 檜山正幸のキマイラ飼育記 メモ編

指標Σの項モナドをT_Σ(-)とする（もともとはTI_Σと書いてあった）。L_Σ(-) := Pow(T_Σ(-))と定義する。ここで、Powは共変ベキ・モナドである。一方、圏Cに対する木下ベキ構成をPOW(C)とする。

C上のモナドFのKleisli圏をKl(C, F) = Kl(F) と書くことにする。モナドT_Σ(-)とL_Σ(-) を十分に大きな圏（アンビエント圏）A上で考える。そのとき、POW(Kl(A, T_Σ(-))) と Kl(A, L_Σ(-)) が一致する（圏同値）と言ったが、これは間違い。

実際は、POW(Kl(A, T_Σ(-)))のほうが大きくて、Kl(A, L_Σ(-)) からの埋め込み（忠実関手）が存在する。

まず、Kleisli射を{y_j ::= e_j(x₁, ..., x_n) } の形の方程式系として表す。Kl(A, L_Σ(-)) の射は、{y_j ::= E_j(x₁, ..., x_n) | E_j ∈L_Σ(X)} の形に書ける。E_j は、E_j⊆T_Σ(X) である（定義より）。jが1からmまで動くとすると、この方程式系は、(Pow(T_Σ(X)))^m （m個の直積）でエンコードできる。

一方、POW(Kl(A, T_Σ(-)))の射は、方程式系 Y→T_Σ(X)))の集まりなので、Pow[(T_Σ(X))^m]でエンコードできる。明らかに、標準的な埋め込み (Pow(T_Σ(X)))^m→Pow[(T_Σ(X))^m]が存在する。

テンプレートとコンテキストの用語で言えば：

• POW(Kl(A, T_Σ(-))) -- コンテキストセットの圏
• Kl(A, L_Σ(-)) -- セット値コンテキストの圏

セット値コンテキストから導かれるあらゆるインスタンス・コンテキストの集まりは、コンテキストセットになっている。これが標準的な埋め込み。POW(Kl(A, T_Σ(-)))を使うことがホントにあるかどうか？ よく分からない。

ほとんど（すべて？）のスキーマ言語は、Kl(A, L_Σ(-))しか使わないだろう。別にスキーマ・メタ項のモナドM_Σ'があると、Y→M_Σ'(X)とKleisli射（セット値コンテキスト） X→L_Σ(S) があると、Y→L_Σ(S) という新しいセット値コンテキストが作れる。この“代入”を可能とするには、M_Σ'(X)に含まれる項を、X→L_Σ(S)のコンテキスト（むしろ環境）により評価する意味写像が必要になる。この“メタ項の意味写像”が、2つのモナドを接着することになる。

いま書いたようなことが次にも書いてある。

• モナドの作用乗法（action multiplication） - 檜山正幸のキマイラ飼育記 メモ編