等式的関手インスティチューション（概要）

昨日の記事「任意の圏を等式により2-圏とみなす」の冒頭で、「圏を2-圏とみなす」動機を書いたのですが、それは、ゴグエン／バーストル〈Joseph Goguen and Rod Burstall〉のインスティチューション〈institution〉を少し具体的に考えたい、ってことでした。

どのように具体化したいかと言うと：

• 使う論理を、等式的論理と一階述語論理に固定する。
• 指標Σに対するモデルの圏を、Model[Σ] := [FreeCat(Σ), Set]_CAT と具体的に与える。

指標圏を固定する気はないのですが、当座の指標圏としては、有向グラフの圏を採用します。ただし、単に「有向グラフ」と言ってしまうと誤解をまねきそうです。通常の有向グラフGと、両端を共有するパスの対（スピヴァックの言葉だとパス同値関係〈path equivalence relation〉、「衝撃的なデータベース理論・関手的データモデル 入門」参照）の集合を一緒にしたものです。

パス同値関係を持った有向グラフ、あるいはその構文的な表現を何と呼ぶか？ これがイッパイ呼び名があり過ぎます。「なにゆえにカン拡張なのか // 型クラスとモデル」に列挙してますが、

1. 箙〈えびら | quiver〉
2. 指標〈signature〉
3. 仕様〈specification〉
4. {形式}?セオリー〈{formal}? theory〉
5. インターフェイス〈interface〉
6. プレゼンテーション〈presentation | 表示 | 表現〉
7. {構文}?生成系〈{syntactic}? {generators | generating set | system of generators {and relations}?}〉
8. コンピュータッド〈computad〉
9. ポリグラフ〈polygraph〉

などなど。僕は、「箙」か「コンピュータッド」を使っています。単に「有向グラフ」で済ませてしまうこともあります。

話を元に戻して、当座の指標圏は*1：

• 指標圏を、コンピュータッド（パス同値関係を持った有向グラフ）とその準同型射の圏に固定する。

これで、どう具体化するかの話はオワリです。

以上の具体化のもとで、さらのモットーとして「出てくるすべての圏〈通常圏 | 1-圏〉を、等式を2-射とした2-圏と考える」を採用します。このモットーを「任意の圏を等式により2-圏とみなす」で説明しました。

通常圏Cの2-射（等式です）の集合を Eq(C) := 2-Mor(C) = |C|₂ とも書くことにします。一般的な2-圏の2-射が等式だとは限りませんが、通常圏から作られた2-圏に関しては、Eq(C) = {(f, g)∈Mor(C)×Mor(C)| f = g} が2-射の集合です。

Σが指標、つまりパス同値関係付きの有向グラフとして、Σから生成される“自由圏”を FreeCat(Σ) と書きましたが、これも誤解をまねくリスクがあります。Σ = (G, E) （Gは単なる有向グラフ、Eがパス同値関係の集合）だとして、FreeCat(Σ)は、Gから生成された自由圏ではありません！ FreeCat(G) のパス（有向グラフGから生成された自由圏の射）のあいだの同値関係をEから作って、その同値関係で商を作ります。つまり、Eから作った同値関係を ～ として、

• FreeCat(Σ) := FreeCat(G)/～

となります。"free"の語が誤解を誘発しそうなので、Σ^◇ := FreeCat(Σ) という右上付き演算記号も使います（形はダイアモンドだけど、書き方はクリーネスターを真似ています）。

今まで説明した具体化の方法と2-圏として扱うモットーにより構成されるインスティチューションを、等式的関手インスティチューション〈equational functorial institution〉と呼ぶことにします。

ここで、等式的関手インスティチューションの素材となっている構成素をすべて書き出しましょう。

1. 指標圏 S： コンピュータッド（パス同値関係を持った有向グラフ）とその準同型射の圏
2. モデル圏： Σ∈|S| ごとに、Model[Σ] := [Σ^◇, Set]_CAT 。Model[Σ] は関手圏。
3. モデル圏のリダクト関手： 指標射（指標圏の射） φ:Σ→Δ in S に対して Model^*[φ] : Model[Δ] → Model[Σ] 。Model^*[φ] を単に φ^* と略記することもある。（定義は後述。）
4. 文集合： Σ∈|S| ごとに、Sentence[Σ] := Eq(Σ^◇) = 2-Mor(Σ^◇) = |Σ^◇|₂
5. 文集合の翻訳写像： 指標射 φ:Σ→Δ in S に対して Sentence_*[φ] : Sentence[Σ] → Model[Δ] 。Sentence_*[φ] を単に φ_* と略記することもある*2。（定義は後述。）

モデル圏のリダクト関手は、関手に対するプレ結合引き戻しで定義します。

• For A∈|Model[Δ]|
  φ^*(A) := φ^◇＊A （ φ^◇＊A∈|Model[Σ]| ）
• For α:A→B in Model[Δ]
  φ^*(α:A→B) := (φ^◇＊α : φ^◇＊A → φ^◇＊B) （ φ^◇＊α : φ^◇＊A → φ^◇＊B in Model[Σ] ）

ここで、φ^◇ : Σ^◇ → Δ^◇ in Cat （Catは“小さい圏の圏”）は、φ:Σ→Δ in S から (-)^◇ = FreeCat で誘導された関手です。'＊'は関手の図式順結合の記号です。圏 Model[Δ], Model[Σ] 内で見れば、'＊'は単なる結合の記号です。同じ記号'＊'が、関手 φ^◇ と自然変換 αやβ のヒゲ結合の記号としても使われています。

文集合の翻訳写像は、φ^◇ : Σ^◇ → Δ^◇ の2-射部分です。

• For ε∈Eq(Σ^◇)
  φ_*(ε) := (φ^◇)_eq(ε) （ (φ^◇)_eq(ε)∈Eq(Δ^◇) ）

最後に、インスティチューションの充足関係〈satisfaction relation〉'|='は次のように定義します。

• For A∈|Model[Σ]|, ε∈Sentence[Σ]
  A |=_Σ ε :⇔ A_eq(ε)∈Eq(Set)

いちおう、A_eq(ε)∈Eq(Set) という条件を書いてますが、これは、Aが集合圏への関手であることから常に満たされます。充足関係が満たすべき公理（インスティチューションの主要公理）は自明に成立するのです。

• φ^*(B) |=_Σ ε ⇔ B |=_Δ φ_*(ε)

充足関係の公理が自明になることは、等式的関手インスティチューションの大きなメリットだと思います。基本性質が超簡単ってことですから。

*1:なぜ当座かと言うと、指標圏をもっと小さく取りたいときもあれば、モナドや相対モナドにより指標圏を拡張したいときもあるからです

*2:[追記] φ_* は下付きアスタリスクのつもりなんですが、環境により下付きに見えないかも。TeXで と書いたほうがいいのかな。[/追記]