簡単なインスティチューション

[追記 date="2006-03-04"]文言、わずかに手直しをした。[/追記]

本編のコレとかでは、簡単なインスティチューションの例を提供しようとしている。インスティチューションの定義くらいは仮定して、本編の例が実際にインスティチューションの例になっていることをザッと説明する。

まず、インターフェースは指標のことである。Javaのインターフェースのような形を使っているので余代数指標、あるいは隠蔽ソートを1つだけ持つ隠蔽代数ソートになる。話を簡単にしたいなら、可視ソートは基本ソート（int, booleanなど）だけに限定してもよい。

J extends I のとき、おおざっぱにいえば I⊆J と考えてよい。つまり、extendsはinclusion（の逆向き；反対）を意味している。inclusionを射と考えれば、インターフェース（指標）の全体は圏になる。inclusionより複雑な射を考えてもいいが、とりあえずinclusionだけでも圏Signができるのは確か。

指標Iに関するホーア制約式を適切に定義すれば、Iのホーア制約式の全体Hoare(I)が定まる。特に自由変数を含まないホーア制約式をSen(I)とすれば、Signの対象ごとに文集合が定まる。I⊆J のとき、Sen(I)⊆Sen(J) と、共変関手が定まる。よって、SenはSign上のSet値の関手。

インターフェース（指標）Iに対して、A⊆Sen(I)を選んだ組(I, A)が仕様である。2つの仕様(I, A), (J, B)に対して、I⊆J、A⊆Bのとき、(I, A)⊆(J, B) として仕様のinclusion圏も定義できる。ここで、A⊆Sen(I)⊆Sen(J) なので、A⊆Bが意味を持つ点に注意。

以上のように定義した仕様のinclusion圏は、Sign上のPow(Sen(-)) で定義したindexed category（Powは共変ベキ関手、varianceは適当に細工する）の平坦化になっている。ModをSign上に定義してもよいが、今定義した平坦化圏Spec上に定義して、Mod:Spec→Cat と考えるのは自然である。ただし、これがうまく定義できることを保証するために、Sign上での充足条件は必要になる。