「インスティチューションとホーア論理を一緒にしたようなナニカ」は、僕にとっての一つの課題です。この課題については、次のエントリーで述べています。
「インデックス付き圏のフビニ／グロタンディーク同値」では、入れ子になったインデックス付き圏を持ち出しました。入れ子のインデックス付き圏の動機は「大量のモナド類似物（monad-like entities）を一挙に扱う方法」だと書きました。実は、「インスティチューションとホーア論理」を考える上でも、入れ子のインデックス付き圏が使えそうなのです。
内容：
ホーアトリプルの圏
以下の記述において、記号の使い方は、「インデックス付き圏のフビニ／グロタンディーク同値」と同様とします。
真偽構造が付いた圏とは、圏Cと反変関手 P:C→Ord の組 (C, P) のことです。ここで、Ordは順序集合の圏です。
順序集合はやせた圏とみなせるので Ord⊆Cat と思えば、(C, P) はインデックス付き圏です。(C, P) にグロタンディーク平坦化を適用できて、できた圏はホーアトリプルの圏になります。次のように書いてもいいでしょう。
- Hoare(C, P) := Σ(x∈C | δx P[x])
Hoare(C, P) の対象は、Cの対象Aと命題p（p∈P[A]）の組 (A, p) です。これは、「領域A上で解釈すべき命題p」と言えます。(A, p) から (B, q) への射は、p ≦ f*(q) という不等式で、これを集合ベースで解釈するなら次の論理式を表すと思っていいでしょう。（⊃ は含意記号。）
- ∀x∈A.[p(x) ⊃ q(f(x))]
あるいは、意味論的に解釈して：
- (x |= p) ⇒ (f(x) |= q)
A, Bを状態空間、fをプログラム実行による状態遷移と考えれば、たしかにホーアトリプルになっています。圏 Hoare(C, P) の射は、p{f}q : A→B のように書けます。
圏 Hoare(C, P) の射であるホーアトリプル p{f}q : A→B から、実行部分 f:A→B だけを抜き出す関手を射影として、Hoare(C, P)→C はファイバー付き圏になります。このファイバー構造まで含めたホーアトリプルの圏を考えれば、真偽値付き圏とホーアトリプルの圏は（圏同値の意味で）1：1に対応することになります。
以上のことから、真偽値付き圏は「ホーア論理が展開できる圏」とも言えます。そして、真偽値付き圏はインデックス付き圏の一種でした。
インスティチューションの精密化
インスティチューションは、インデックス付き圏に構造を追加したものとみなせます。そのことは次の記事を参照してください（系統的な説明じゃありませんが）。
Sigを指標の圏、Modを指標にモデル圏を対応させる関手とします。Mod:Sig→Cat なので、(Sig, Mod) はインデックス付き圏になります。通常のインスティチューションの定義では、Sigの対象Σに論理文の集合 Sen(Σ) を対応させる写像と、充足関係（satisfaction relation）を考えます。
ここでは、指標Σのモデル圏 Mod[Σ] を単なる圏ではなくて、真偽構造が付いた圏にします。真偽構造のベース圏を改めて Mod[Σ] と書き、Mod[Σ] 上で定義された真偽値（あるいは命題）の順序集合を対応させる関手を P[Σ] とします。(Mod[Σ], P[Σ]) が真偽構造付き圏で、これは指標Σごとに定まります。
σ:Σ→Γ が指標圏Sigの射だとすると、反変的にリダクト関手 σ*:(Mod[Γ], P[Γ])→(Mod[Σ], P[Σ]) が定まります。(Mod[Γ], P[Γ])→(Mod[Σ], P[Σ]) の関手とは、真偽値構造付き圏のあいだの準同型であり、通常の関手 F:Mod[Γ]→Mod[Σ] と、自然変換 ψ::F;(P[Σ])⇒P[Γ] からなります。
このような構造は、インスティチューションの精密化を与えていると期待できます。Senとその翻訳写像、充足関係などが出てきませんが、それらは上記の素材から再構成できると思われます。
[追記 date="2011-11-12"]いやっ、再構成できないかも。なんか足りてない。翻訳写像は、指標射と同じ向きなので、指標射と共変的に働くナニカが必要みたいです。[/追記]
依存的なインデックス付き圏
今述べたインスティチューションの精密化（と期待される構造）では、ベース圏としてSigがあり、真偽構造付き圏を値とするインデキシングの構造があります。しかし、「インデックス付き圏のフビニ／グロタンディーク同値」のように、それを二重インデックス付き圏に直すことはできません。
なぜなら、Mod[Σ] がΣごとに変わってしまうからです。Σによらず同じファイバーが生えているなら、ベース圏と典型ファイバーの直積上のインデキシングを構成できますが、そうはなっていません。Σに依存してファイバーが変わるのです。言うなれば、依存的なインデックス付き圏ですね。
しかしそれでも、「グロタンディーク平坦化の適用の順序によらず出来上がる圏は同値」という主張は意味を持ちます。「これが成立しているといいなー」と思ってますが、確認は出来てません。
いずれにしても、繰り返しされたインデキシングを持つような圏は、計算モデルにはよく出てくるみたいです。
