CatyのWeb処理の背景
ひとつ前の記事「CatyのWeb処理： Webフィーチャとメタプログラミング」の背景の理屈を少し追加説明しておく。メモ書き程度だが。
背景は、入れ子の、あるいは多段のインスティチューション。いろいろな圏が出てくる。
- Graph -- 有向グラフの圏。自己ループも多重辺も認める、まったく任意のグラフの圏。ただし小さい（たかだか加算で十分）なグラフが対象。
- Syn -- 構文的対象（syntactic objects）の圏。対象は、頂点ラベルと辺ラベルが付いたグラフだが、ラベルを頂点そのもの、辺そのものと同一視して、SynはGraphの部分圏と考える。
- Exp -- 構文モナド。ExpはSynの上のモナドで、乗法と単位は、入れ子になった式の展開と基本記号を式とみなす操作。
- Sig -- 指標の圏。インスティチューションの指標を与える。Sig⊆Syn⊆Graph と考える。指標も有向グラフとなる。
- V -- 計算モデルの圏、Vはvalueから。もちろん、射もあるのだが、評価の結果が入るのがVという感じ。
Sigは指標の圏だが、指標は構文的なグラフとなっている。Σが指標＝グラフとして、Mod[Σ] := [Σ, V] と定義する。ここで、[Σ, V] は、グラフΣから圏Vへのグラフ写像の全体を、自然変換と同様な感じで圏とみなしたもの。関手圏とほとんど同じ構成だ。
Σ∈|Sig| として、Exp(Σ) はΣから構成された式の全体。(m:Σ→V)∈|Mod[Σ]| があれば、mをExp(Σ) にまで拡張できる。というか、拡張できるようなフレームワークを考える。m:Σ→V の拡張を Exp(m):Exp(Σ)→V とする。この拡張は、Mod[Σ] → Mod[Exp(Σ)] という関手を与える。
具体例に移る。Σ = ΣWeb をWebフィーチャの指標（インターフェイス）だとする。Σは、圏Sigに属する固有の指標になる。指標だから意味は持たない。Mod[Σ] = Mod[ΣWeb] を、単に Web ともかく。Web = Mod[ΣWeb] の対象がWebフィーチャになる。W0∈|Web| が標準モデル＝標準Webフィーチャで、他のWebの対象はすべて非標準ということになる。
指標Σ上で組み立てられた式eは、e∈Exp(Σ+Γ) であり、Σ=ΣWebなら、eはWebシステムの一部となるものである。ΓはΣ以外に依存している指標。Γの意味を固定すると、e∈Exp'(Σ) と考えることができて、eの評価は Mod[Σ] の要素に依存することになる。これは、指標 Σ=ΣWeb に従った実装である W∈Mod[Σ] = [Σ, V] を変えると、Webシステムの挙動が変わることを意味する。
なんか中途半端だが、メモだからここまでだ。
