インスティチューションだのプロ関手だのなんだの

クリスマスで連休で、その後は正月で、ってなわけで、こういうときは、普通どおりに仕事するのもナンだし、最近は子供と遊ぶことも少ないしで、なんだかボーッとしている。すると、ボーッとしたことを思いつく。はたして意味があることかどうかわからないが、メモしておこう。

インスティチューションの定式化と例

ボーッと考えていたのは、インスティチューション。

1. インスティチューションを、もっと使いやすいように変形や拡張ができないか？
2. インスティチューションの実例で、わかりやすいものはないか？
3. インスティチューションをバキバキに使いたいなー。

とか。

階層付き圏

まず、category with inclusions / inclusive category って言葉がどうもイヤだ。category with hierarchy / hierarchical category で、階層付き圏と呼びたい。階層が実際にモノな包含（inclusion）のときもあるが、階層を表現する射がエピのこともある。

階層付き圏の例は、オブジェクト指向のクラスをモデル化するような圏で、B extends A のとき、B ≧ A （または、B ≦ A、向きはどっちでもいい）の順序があるような圏。B extends A かどうかは、なんらかの方法で決定できるとする（ダックタイピングでも良い）。B extends A かつ A extends B は A = B だとするなら、extendsで生成される圏は“とてもやせた圏＝順序集合”となる。

インスティチューションのモデル圏 Mod[Σ] に、とてもやせた部分圏（単にやせた部分圏でもいいだろう）が指定された構造を持たせて階層付き圏としたい。Mod[Σ] 自体は模倣を射とする遷移系（広義のオートマトン）の圏とするのが現実的／実務的だろう。

メイヤー指標とメイヤー・オートマトン

インスティチューションの具体例として、メイヤー指標の圏の上に、メイヤー・オートマトンのモデル圏を考えるのがいいと思う。形容詞「メイヤー」は、メイヤー先生の「Command-Query分離の原則」を守ったモノという意味。

メイヤー指標Σは、オペレーション記号の集合Σで：

1. Σ = Σ_command + Σ_query と直和分解される。
2. Σ_command は単なる記号の集合。
3. Σ_query は、記号と基本ソート（集合と思ってよい）のペアの集合。
4. Σ_command も Σ_query も無限集合でよい。

q∈Σ_query だと、q = (op_q, V_q) と書けるが、q = (q, V_q) と略記する。さらに、十分大きな集合Vを用意して、V_q⊆V と考える。

A = (State_A, tran_A, obs_A) が指標Σ上の決定性メイヤー・オートマトンだとは：

1. tran_A: Σ_command×State_A→State_A は写像
2. obs_A: Σ_query×State_A→V は写像

A = (A, tran obs) のように略記する。集合としてのAが状態空間、tranが遷移、obsが観測。非決定性メイヤー・オートマトンは、圏Setの代わりに圏Relで考える。メイヤー・オートマトン射は、模倣か双模倣で定義する。

メイヤー・オートマトンの圏は、インスティチューションの例だけでなくて、マイヒル／ネロードの定理の説明にも使える。

Senを圏と考える

インスティチューションのSen[Σ]を集合ではなくて圏と考える。その圏は、やせたデカルト閉圏。

1. 圏の対象は論理文（閉じた論理式）p, q など。
2. pからqへの射は、証明可能性 p |- q 。
3. pとqのデカルト積はp∧q。
4. pとqの指数は含意 p⊃q。
5. pとqの同型は、論理的同値 p≡q。
6. 指数に関する随伴は演繹定理 p∧q |- r ⇔ p |- q⊃r
7. 終対象でもあり、かつ積∧の単位対象は、論理定数true。

充足関係はブール値のプロ関手

プロ関手（副関手）は、profunctor、distributor、module、bimoduleとか色々な呼び方があるが、最近 correspondence と呼んでいる例を見た（http://dl.dropbox.com/u/8165870/Unicity.pdf）。ウヒャー。さらに用語を増やしてコノヤローとも思ったが、correspondenceが一番適切な気がする。

それはそーと、Bを{0, 1}からなるブール代数に 0 ＜ 1 という順序を入れて、順序からできる圏に論理ANDでモノイド積を入れた対称モノイド圏とする。Bには含意演算があるから、実はBは対称モノイド閉圏である。

それで、Bに関して豊饒化（enriching）した豊饒圏（enriched categories）の枠内で考える。B-圏のなかでプロ関手を考えると、それは順序付き関係となる。順序付き関係はプロ関手なので、プロ関手の結合で圏になるが、そうじゃなくて別な圏構造を入れる。

AからBへの順序付き関係を A+→B のように表す。順序付き関係を1セルと考えて、2セルを考える。2セルをTRペアと呼ぶ。TRはtranslation-reductのこと。インスティチューションを意識している。α::(R:A+→B)⇒(S:C+→D) がTRペアとする。TRペアとは：

1. f:C→A という単調写像（関手）
2. g:B→D という単調写像（関手）
3. 可換性

可換性の基本は、充足関係の公理：

• R(f(c), b) = S(c, g(b))

随伴ペア(f, g)の随伴性と同じ形をしている。R:A+→A のとき、RはA上のhomset関手だと思ってよい。ホントのhomset関手（標準homset）がプロ関手圏の恒等を与える。

充足関係がプロ関手である状況証拠

細かい計算を全然してない。雰囲気だけ。

B extends A のことを B≧A あるいは A≦B と書くことにする。pが論理文だとして、メタ命題 A |= p の（メタの立場の）ブール論理値を [A |= p] と書くことにする。（<A |= p> のほうが感じが出てるが、はてなダイアリーで書くのがメンドイ。）

次の事実がある。

• B≧A ならば、任意のpに対して [B |=p]≧[A |= p]。
• p |- q ならば、任意のAに対して [A |=p]≦[A |= q ]。

Mod[Σ]の階層構造の圏と、やせたデカルト閉圏とみなした Sen[Σ] に対して、R(A, p) := [A |= p] として定義された写像が、プロ関手になっていることは示せると思う。

Mod[Σ]の階層構造の圏をHier[Σ]とすると、[- |=_Σ -] :Hier[Σ]+→Sen[Σ] となっている。つまり、3つ組 (Hier, Sen, [- |= -]) は、指標圏からプロ関手を対象として（1セルではなくて）2セルを射とする圏への関手となっている。

多段インスティチューション

実は、一連のことをボーッと考えたきっかけは、多段インスティチューションなのだ。Hier[-], Sen[-] のような意味が固定された関手ではなくて、指標の圏SigからB-豊饒圏への関手 F[-], G[-] があったとして、R[-]:F[-]+→G[-] がプロ関手となっている状況を考える（TRペアも一緒に考えている）。これは普通のインスティチューションを少し抽象化しただけ。

別に、S[-]:G[-]+→H[-] というプロ関手を値とする関手があるとする。これもインスティチューションと考えてよい。R[-]とS[-]は、プロ関手の普通の結合で結合できる。RとSを結合すると、(R*S)[-] : F[-]+→H[-] というインスティチューションができる。

もちろん、プロ関手圏の1セル（水平セル）と2セルの計算をちゃんと定義しないといけない。

多段インスティチューションを使うと、「要件、仕様、論理モデル、実装モデル」のように順に詳細化／具体化する設計プロセスを定式化できると思われる。「実装が要件を満たす」といった言明に正確な定義を与えられる可能性がある。

何が必要か

豊饒圏をベースにしたプロ関手の理論が必要なんだが、通常のプロ関手結合以外に、2セルを入れて2次元化することも必須。インスティチューションでは、指標射に対して2セルのほうを対応させる。1セル（プロ関手）の水平結合は、多段インスティチューションを縮退させるときに使う。

豊饒化の基礎圏（enrichedじゃなくてenriching cat. のほう）も取り替えるような定式化が必要な気もする。

多段インスティチューションは、充足関係（2つの圏とプロ関手）の横チェーンのことだ。それとは別に縦方向の2セル（面）もある、という構造。2セルが、translation-reduct pairだ。通常のインスティチューションでは、2セルの部分の定式化が弱い。ここを強化しないとな。

ローヴェルの距離空間

非負実数を対象として、順序（ただし逆向き）を射とする圏は、maxを直積、minを直和とするデカルト半環圏となる。この圏の同型は等しいこと。積は厳密に対称となる。他に足し算もモノイド積となり、制限引き算が指数となりモノイド閉圏。

非負実数の圏には、モノイド積が3つもある。有限次元ベクトル空間の圏のように直積直和が退化していることもない。なかなかに面白い圏だ。

非負実数の圏を豊饒基礎圏（enriching cat.）として豊饒圏が（多少拡張した）距離空間であることはローヴェルが指摘している。直積距離空間は和距離で定義すると、距離空間の圏は積を持つことになる。また非負実数自体も差の絶対値で距離空間になる。

距離空間の圏をある種の圏の圏（レルム）と考えると、関手は縮小写像（正確には非拡大写像）となる。プロ関手は、積距離空間からの縮小写像で与えられる。プロ関手の結合は、不等号評価を色々使えば出る。

この距離空間の圏においても、プロ関手とTRペアのようなものを考えることが出来ると思うが、どうだろう。

用語

プロ関手は、まー「プロ関手」でもいいと思う。「対応」のほうが望ましい気はするが少数派だからな。

プロ関手のあいだの２セルは「随伴対」でもいいのかな。プロ関手を一般化されたホムセットと考えれば、ホムセットを使った随伴の定義と同じ形をしている。随伴とのアナロジーを追うのも悪くない気がする。

記号とキーワード

記号	キーワード
p⊃q	p implies q
|- A	Provable[A]
A |- B	A derives B
A |= p	A satisfies p
B≧A	B extends A
A∈Mod[Σ]	A implements Σ
α⊆β	β contains α