一般関手モデルは、スピヴァックの関手データモデルをデータベース以外にも適用する試みです。とはいえ実際のところ、特別に一般化する必要性は薄いですね、スピヴァック理論が既に十分に一般的に作られているので。今回の話も二番煎じで、関手データモデルがインスティチューションを定義することは既にスピヴァックが示しています。この事実を、観点と記述スタイルを若干変えて説明してみます。
内容：
- 言葉と記号の約束
- だいたいのところ（概要）
- 有向グラフに対する圏的演繹系とグラフ制約の圏
- Pathモナドと有向グラフの圏の拡張
- グロタンディーク構成による表示の圏の再現
- インスティチューションの構成
- 関手モデルとインスティチューションの同値性
言葉と記号の約束
Catは、小さい圏と関手からなる圏です。Graphは、有向グラフとグラフの準同型写像からなる圏です。グラフの準同型写像とは、頂点を頂点に、辺を辺に移す写像。有向グラフGから作られた自由圏を FreeCat(G)、小さい圏Cから圏の演算を忘れた有向グラフを Graph(C) とします。Graph(-) は忘却関手ですね。
一般に、関手 F:X→A と U:A→X が随伴になっているとき、F -| U : A←→X のように書くことにします。A∈|A|, X∈|X| に対して、自然な同型 A(F(X), A) ＝ X(X, U(A)) が存在します。自由圏の生成関手と忘却関手のあいだの随伴 FreeCat -| Graph : Cat←→Graph は今回よく使います。Cat(FreeCat(G), C) と Graph(G, Graph(C)) は自然に同型です。
F = (F:C→C, μ::FF⇒F, η::IdC⇒F) が圏C上のモナドのとき、そのクライスリ圏は、Kl(C, F) と書きます。後で出てくる実例は、Kl(Graph, Path) です。ここでPathは、随伴 FreeCat -| Graph から作られるモナドです。
関手モデルのアンビエント圏として、大きい圏（小さくない圏）、例えばSetが登場します。Set∈|Cat|とはみなせないので、SetやCatを対象として含む“圏の圏”をCAT（全部大文字）としましょう。Catに比べるとCATはかなり怪しい／あやうい概念で、使うのがためらわれるのですが、なんらかの安全対策をする前提でCATを使うことにします。A∈|Cat| のとき、Aは圏なので A∈|CAT| にもなります。つまり、Cat∈|CAT| であり、Cat⊆CAT（部分圏）でもあるわけです。CATは単に、説明を短くするための方便と思ってもかまいません。
だいたいのところ（概要）
スピヴァックの関手モデルは、Sch⊆Cat に対して、M:Sch→CAT という反変関手を定義します。（反変の）関手Mは M(S) := [S, C] で与えられます。ここで [S, C] は CAT(S, C) の意味ですが、アンビエント圏Cが大きくてもSが小さいなら [S, C] は取り扱い可能な関手圏です。[S, C] は圏なので、[S, C] = M(S) ∈|CAT| であり、関手 σ:S→T in Sch に対する M(σ):M(T)→M(S) in CAT も関手の引き戻しで定義できます。
以下では、Sch = Cat の場合を考えることにします。Catと圏同値な圏Pres（圏の表示の圏）を作って、モデル関手Mを M:Pres→CAT と変更します（本質的には変えてません）。それとは別に、Graphを拡張したXGraph（後述）上のインスティチューションを作り、インスティチューションのモデル関手 Mod:XGraph→CAT をグラフ制約（後述）でパラメトライズすると、パラメトライズされたModがスピヴァックの意味のモデル関手Mと同じものであることを示します。
スピヴァック理論の魅力のひとつは、既存の概念だけで出来ていることです（解釈が斬新）。新しい概念や道具を導入しなくても、よく知られた圏論の方法を坦々と適用するだけで、解釈してみるとそれなりに面白い結果が得られるのです。これは楽しいですね。圏論の方法を学ぶモチベーションにもなるでしょう。
有向グラフに対する圏的演繹系とグラフ制約の圏
インスティチューションの構成には演繹系（推論系、証明系）が必要になります。この演繹系を、以下ではCDS（Categorical Deduction System、圏的演繹系）と呼ぶことにします。CDSは有向グラフGごとに決まるので、それを CDS(G) と書きます。
圏的演繹系の推論規則を具体的に述べることはしませんが、有向グラフGに対する圏的演繹系 CDS(G) の論理文（logical sentence）の集合 Sen(G) と証明可能性 |-G を非形式的にザッと説明します。Sen(G) と |-G により、CDS(G) が決まります； CDS(G) = (Sen(G), |-G) 。
Gを有向グラフとして、Path(G) をGのパス全体の集合だとします。パスpの始点と終点を dom(p)、cod(p) と書くことにして、{(p, q)∈Path(G)×Path(G) | dom(p) = dom(q), cod(p) = cod(q)} という集合を考えます。この集合の要素 (p, q) を p = q という等式だと考えて、この集合を Sen(G) とします。
s1, ..., sn, t∈Sen(G) に対して、s1, ..., sn |-G t は、「s1, ..., sn を仮定すると t が証明できる」と読みます。その意味は、s1, ..., n, t を等式とみなして、s1, ..., n を仮定した等式的な推論を積み重ねて t が得られることです。
Sen(G) の部分集合で演繹に関して閉じているものをセオリーと呼びます。詳しく言うと、T⊆Sen(G) がセオリーだとは、
- s1, ..., sn∈T かつ s1, ..., sn |-G t ならば、t∈T 。
Sen(G) の任意の部分集合Aに対して、Aを含む最小のセオリーが決まるので、それを Th(A) とします。A, B⊆Sen(G) が、A⊆Th(B) のとき、A≦B と書くことにします。関係≦はプレ順序になります。このプレ順序関係を入れた Pow(Sen(G))（Senのベキ集合）を Constr(G) と書きましょう。Constr(G) = (Pow(Sen(G)), ≦) 。'Constr'は制約（constraint）のつもりです。Constr(G) の要素（連立のパス方程式）を、Gのグラフ制約と呼ぶことにます。スピヴァックのパス同値関係（の集合）と同じものです。
Constr(G) はプレ順序集合なので、やせた圏とみなすことができます。圏とみなしたConstr(G)も同じ記号で表して、Gのグラフ制約の圏と呼びます。
今述べた内容に関して、次の記事が参考になるかもしれません。
Pathモナドと有向グラフの圏の拡張
グラフGに対して、パスの全体をPath(G)と書きますが、Path(G)は再びグラフになっています。圏の場合と同様に、|G| = (Gの頂点の集合）、G(A, B) = (AからBに向かう辺の集合) としましょう。G' = Path(G) として、G'の有向グラフ構造を次のように定義します。
- |G'| = |G|
- G'(A, B) = (Aから出発してしてBに至るGのパスの集合)
f:G→H がグラフ準同型のとき、Path(f):Path(G)→Path(H) は自明に決まります。したがって、Pathは Graph→Graph という自己関手になります。そればかりでなく、入れ子のパスを平坦化する写像 Path(Path(G))→Path(G) を乗法、埋め込み G→Path(G) を単位として、Pathは圏Graph上のモナドになります。このモナドPathは、随伴 FreeCat -| Graph : Cat←→Graph から作られたモナドと同じもので、Path(G) = Graph(FreeCat(G)) となっています。
モナドPathによるクライスリ圏 Kl(Graph, Path) を XGraph とします。XGraph := Kl(Graph, Path) 。定義より XGraph(G, H) = Graph(G, Path(H)) で、Path(H) = Graph(FreeCat(H)) でした。随伴 FreeCat -| Graph による同型 Graph(G, Graph(C)) ＝ Cat(FreeCat(G), C) のCのところに FreeCat(H) を代入すると Graph(G, Graph(FreeCat(H)) ＝ Cat(FreeCat(G), FreeCat(H)) なので、XGraph(G, H) ＝ Cat(FreeCat(G), FreeCat(H)) 、つまり、圏XGraphは小さい自由圏の圏と圏同値です。
|XGraph| = |Graph| なので、対象は拡張してません。(f:G→H in XGraph) ⇔ (f:G→Path(H) in Graph) なので射のほうが増えているのです。もともとのグラフ準同型写像＝Graphの射は、XGraphでも射なので、Graph⊆XGraph と埋め込めます（クライスリ圏なので当然）。
XGraphの射 f:G→H は、Path(G)→Path(H) in Graph を誘導します。パスをパスに移すので、Sen(G)→Sen(H)、さらには Constr(G)→Constr(H) という関手（プレ順序集合の準同型写像）も誘導します。この事実は後で利用されます。
グロタンディーク構成による表示の圏の再現
小さい圏の表示（presentation）Pとは、有向グラフGとグラフ制約Aの組 P = (G, A) です。Pから作られる圏 Cat(P) = Cat(G, A) は、Gから生成される自由圏 FreeCat(G) に対して、(p, q)∈Th(A) であるパスpとqを同一視して作ります。Th(A) は、圏的演繹系 CDS(G) = (Sen(G), |-G) に基いて定義されます。
P = (G, A)、Q = (H, B) （A⊆Sen(G)、B⊆Sen(H)）を2つの表示だとして、表示のあいだの準同型射とは、f:G→Path(H) というグラフ準同型写像（つまり、XGraphの射）であって、fが誘導する f*:Sen(G)→Sen(H) が、
- (p, q)∈A ならば、f*(p, q)∈Th(B)
を満たすことです。これは、f*(A) ⊆ Th(B) と簡略に書くこともできます。また、Constr(H) のプレ順序関係≦を使って書けば：
- f*(A)≦B
以上の定義により、圏の表示を対象、表示のあいだの準同型射を射とする圏が構成できます。恒等射と単位律は自明ですが、結合律はいちおう確認してみてください。こうして作った圏の表示の圏をPresとします。
さて、「ホーア論理の圏論的な定式化」や「インスティチューションとホーア論理」に、p≦f*(q) という不等式が出てきますが、上の f*(A)≦B はそれとよく似た不等式です。その背景はグロタンディーク構成です。
XGraphをベースの圏として、XGraphの対象（有向グラフ）GごとにConstr(G)を対応させると、XGraphの射 f:G→H は、関手（プレ順序の準同型写像）f*:Constr(G)→Constr(H) を誘導します。Constr(f) := f* とすると、Constr(-) は、XGraph→Cat という関手になります。これは共変のインデックス付き圏（余インデックス付き圏）です。
余インデックス付き圏 Constr:XGraph→Cat にグロタンディーク構成をしてみると、でき上がる圏∫(g∈XGraph | Constr(g)) は表示の圏Presに他ならないことがわかります。
インスティチューションの構成
いよいよインスティチューションを作ってみます。これから構成するインスティチューションを (Sign, Mod, Sen, |=) とします。それぞれの構成素の意味はインスティチューションの資料（例えば、http://cseweb.ucsd.edu/users/goguen/projs/inst.html）を参照してください。
関手モデルのアンビエント圏Cは適当に選んで固定します。Sign := XGraph とします。G∈|Sign|（= |XGraph|）に対して Mod(G) := [FreeCat(G), C] とします。G|→Mod(G) を (f:G→H)|→(Mod(f):Mod(H)→Mod(G)) に拡張して関手にしましょう。f:G→H in XGraph（f:G→Path(H) in Graph）があると、これは f*:FreeCat(G)→FreeCat(H) に拡張できます。K∈[FreeCat(H), C] に対して Mod(f)(K) := f*;K と定義すれば、Mod(-) は、Sign→CAT という関手（インデックス付き圏）になります。
G∈|Sign| に対するSen(G)は、既に定義した圏的演繹系のSen(G)をそのまま使います。F∈Mod(G) と (p, q)∈Sen(G) に対する充足関係 F |=G (p, q) は次のように定義します。
- (F |=G (p, q)) ⇔ (F(p) = F(q))
Fは FreeCat(G)→C という関手なので、パスp, qに対してF(p)、F(q)はCの射として定義されます。それらが同じ射であるかどうかの真偽が |=G の定義になります。
このようにして作った (Sign, Mod, Sen, |=) が実際にインスティチューションになっていることは、定義を追いかけるだけで確認できます。
関手モデルとインスティチューションの同値性
スピヴァックの意味の関手デモル（の檜山による若干の変更）は、圏の表示の圏Presとその上の関手 M:Pres→CAT です。関手Mは、M(P) = [Cat(P), C] として定義されています。このMと同値となるようにインスティチューションをパラメトライズします。
A⊆Sen(G) として、Mod(G, A) を定義します。Mod(G, A) は Mod(G) の充満部分圏です。充満なので、|Mod(G)| の部分集合 |Mod(G, A)| さえ決まれば、自動的に部分圏が決まります。|Mod(G, A)| は次のように定義します。
- {F∈|Mod(G)| | すべての (p, q)∈A に対して F |=G (p, q) }
グラフGとグラフ制約Aの組 (G, A) は圏の表示だったので、(G, A)|→Mod(G, A) は圏の表示の圏Presの上で定義されているとみなすことができます。Modを Pres→CAT とみなすと、これは M:Pres→CAT と一致します。Mod = M は、定義の言い換えに過ぎません。
以上から、関手モデルは、グラフ制約をパラメータとするインスティチューションによっても表現できることが分かりました。長ったらしい定義の連鎖で、追いかけるのは面倒かも知れませんが、それぞれのステップは当たり前の話です。これは、関手モデルを別な視点から眺めたことになってます。多様な解釈を許すことは関手モデルの豊かさの証左のように思えます。
