簡単な多重継承の略式インスティチューション

本編 なんで多重継承はそんなに嫌われるのか？ ちょっくら分析してみるか - 檜山正幸のキマイラ飼育記 (はてなBlog) の補足：

簡易インスティチューションで定式化してみる。実は簡易インスティチューションにさえなってない略式インスティチューション。どのへんが略式かというと、指標Σに対してMod[Σ]は単なる集合。よって、指標射 Σ→Δ に対するMod[Δ]→Mod[Σ]は単なる写像。さらに、文関手Senは考えない。

本編では、クラスという曖昧で直感的な概念を使ったが、ここではクラスを使わない。S={boolean, int double, string}を基本ソートの集合として固定（実はSは何でもいい）。Sの各ソートの意味（領域）も固定。T = S + S^*×S とする。Sは変数のソート、S^*×Sはメソッドのソート。

指標Σとはソート付き集合 |Σ|→T のこと。Σと|Σ|はしばしば区別しない。指標射は単射f:|Σ|→|Δ|で、f;Δ = Σ、つまりソート割り当てを保存するもの。Var(Σ) = Σ^-1(S), Var(Σ)⊆|Σ| だとする。

指標と指標射の全体をSignとすると、余完備圏。また、包含写像を考えると、inclusive category（category with inclusions）。

Mod[Σ]は、Var(Σ)をフィールド名とするレコード全体の集合、ただし、Var(Σ)上のソート割り当てに従うレコード。指標射Σで誘導されるレコード集合の写像は射影で、モデル全体の圏ModはSignの反対圏だと思ってもよい（略式だから！）。

Signが有限余完備なので、圏Modは有限完備。Sign内でスパンの余ファイバー和が作れるが、任意のinclusionsに対して余ファイバー和は作れない。よって、inclusionの部分圏（順序構造）のなかで余ファイバー和は部分的にしか定義できない。このへんが、リネームを許して余ファイバー和を作れるようにするか、余ファイバー和をあきらめてinclusionだけに制限するか、の違いを表している。