対指標とパラメータ化指標
相対指標とパラメータ化指標は同じ概念である。が、相対指標は原理的で、パラメータ化指標は実用的。
Σが指標のとき、指標に出現するすべての名前の集合を全名前集合〈whole name set〉と呼ぶ。全名前集合の部分集合を単にΣの名前集合〈name set〉と呼ぶ。
指標やインスタンス／トランスフォーマーの記述レコードは、宣言／定義の集合ではない。順序依存性があるのでリストに近い。ただし、一部の順序は交換可能で、ようするにコンピュータッド（集合のリスト）だ。
相対指標〈relative signature〉は、指標とその部分指標のペアだが、形式上、指標を前半と後半に分けた形で書くことができる。部分指標をΔ、全体指標（親指標）をΣとすると、[Δ]Σ と書く。Δ#Σ' = ΣであるΣ'を使って、[Δ]Σ' でもよい。重複記述を避けるには、Σ'を最小に取る。Σ'からΣを再現するには、Δとマージ（#演算）すればよい。
指標演算とパラメータ化
最も重要な指標演算はマージで、'#'か'+'で表す。一般には直和ではなくて、余ファイバー和になる。余ファイバー和を作るには、スパンが必要だが、スパンは指標のラベリング（名前付け）に基づいて作れる。要するに、同じ名前は同一視するだけ。マージと余ファイバー和はまったく同じ。
AをΣの名前集合とする。このとき、Aを含む最小の部分指標＝グラフをAのハル〈hull | 外皮 | 外殻〉と呼び、Hull(A, Σ)と書く。
ハルを使うと、指標から名前を削除する“引き算”が定義できる。
- Σ - A := Hall( (|Σ|・ ＼ A), Σ)
＼は単なる集合差。|Σ|・ := Σ0∪Σ1。Aが部分指標Δであっても、Δの全名前集合をAとして、Σ - Δ = Σ - A として指標の差を定義できる。
- Aが名前集合のとき、named param A Σ は、relative signature [Hull(A, Σ)]Σ と同じ。
- Xが名前のタプル、AはXの順序を忘れたものだとして、ordered param X Σ は、relative signature [Hull(A, Σ)]Σ と同じ。
こうして見ると、順序パラメータは、相当に複雑なメカニズムを導入してしまっていることがわかる。順序と名前のあいだの対応関係を挟んでいるので、束縛を作る手間がかかる。
相対指標、部分インスタンス、半指標
相対指標 [Δ]Σ があるとき、ΔのインスタンスAを付けた (A, [Δ]Σ) を部分インスタンス〈partial instance〉と呼ぶ。部分インスタンスの表現として、[A]Σ も使う。部分インスタンスは実は指標でもあるので、半指標〈semi signature〉とも呼ぶ。
なぜ2つの名前を準備するか、というと、人は「名前の呪縛」＝「名は体を表すものだという強い思い込み」を持つから。インスタンスと呼んでしまうとインスタンスだと思ってしまう。指標だと思いたいときに、半指標と呼ぶ。
[A]Σ が半指標のとき、instance of [A]Σ というインスタンスを考えることができる。これは、もともとあった全指標Σのインスタンスになる。
次の手順になる。
- 指標Σがある。
- 部分指標Δを選ぶ。Δ⊆Σ。
- 相対指標 [Δ]Σ を作る。Σ' を使って、[Δ]Σ' と書けるが、それは単なる略記。
- ΔのインスタンスAを選ぶと、半指標 [A]Σ ができる。
- 半指標も指標なので、半指標のインスタンスBができる。instance B of [A]Σ := {...}
- Bは指標Σのインスタンスとなっている。
指標Σから一気にBを作る代わりに、ΔのインスタンスAをあいだに挟んで、二段階でインスタンスを作るような指示を含むのが相対指標である。相対指標のインスタンス化は、部分指標のインスタンス化と残った半指標のインスタンス化の二段階になる。
相対指標の解釈として、マージ演算#を対称モノイド積とするモノイド圏における閉構造として捉えることができる。大枠としては、
- Cat(Mod[Δ#Γ], Mod[Σ])
Cat(Mod[Γ], [Mod[Δ], Mod[Σ]])
であり、
- Mod[[Δ]Σ]
圏Trfを次のように定義するとよいと思う。
- Trf(Γ, Σ) := Cat(Mod[Γ], Mod[Σ])
実際には、Mod[]の定義がシステム (Ω, ω:Ω→Set)と相対的になる。また、ホントは、
- Trf(Γ, Σ) ⊆ Cat(Mod[Γ], Mod[Σ])
であり、置換子〈サブスティテューター〉により実現できる関手だけがTrfに含まれる。トランスフォーマー〈変換子〉より、置換子のほうがより本質的な存在で、トランスフォーマーは、置換子の相対的な反変表現になっている。換言すれば、置換子の圏の相対化（＋反対化）によりトランスフォーマーの圏が生まれる。
