このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

インスティチューションと型階層

インスティチューションは、さまざまな型理論を統一的に扱うための便利な枠組みになります。与えられたインスティチューションをインデックス付き圏(indexed category)とみなして、グロタンディーク構成を行うことは有効なテクニックです。

このテクニックの簡単な応用例を紹介します。この方法は、オブジェクト指向のクラス、抽象クラス、インターフェースなどを全部ひっくるめた型階層(type hierarchy)を作りたいときなどに使えます。

Σを指標だとして、M[Σ]をモデル圏とします。H[Σ]はM[Σ]の部分圏で次の性質を持つとします。

  1. H[Σ]は、M[Σ]の広い(broad, wide)部分圏である。
  2. H[Σ]は、M[Σ]のやせた(thin)部分圏である。

広い部分圏という条件だけでもいいのですが、話をハッキリさせるためにやせていることも仮定します。

A, B∈|M[Σ]| のあいだのプレ順序関係≦を次のように定義します。

  • A≦B ⇔ (f:A→B であるH[Σ] の射が存在する)

この関係≦を、型のあいだの階層関係、つまりサブタイプ/スーパータイプの関係だと解釈します。H[Σ]の射は、型階層を構成する素材となります。

指標Σはインターフェースとみなせますが、別なインターフェース(=指標)Γがあって、インターフェースの変換(指標射)ρ:Σ→Γ がある状況を考えます。この状況で、A∈|M[Σ]|, X∈|M[Γ]| を取ると、AとXのあいだには階層的な関係(プレ順序関係)が定義されていません。AとXのあいだの階層的な関係を定義してみます。

以下では、すべての指標に対して上で説明したようなH[Σ]が付随していて、指標射 ρ:Σ→Γ に対するリダクト関手 ρ*:M[Γ]→M[Σ] は、H[Γ]をH[Σ]に移すものと仮定します。

A∈|M[Σ]|, X∈|M[Γ]| に関する2つの関係 *≦、≦* を次のように定義します。

  • X *≦ A ⇔ ρ*(X) ≦ A
  • A ≦* X ⇔ A ≦ ρ*(X)

*≦ と ≦* のどちらが適切かはケースバイケースですが、いずれにしても、すべてのモデルのあいだに階層的な関係を定義することができます。一例としてこれは、異なるインターフェースを持つクラスのあいだでも、インターフェースのあいだの関係をもとにサブクラス/スーパークラスの関係を定義できることを意味します。

[追記] 一般論としては、階層構造を記述するための部分圏H[Σ]を入れておいたほうがいいと思いますが、実際にはH[Σ] = M[Σ] で間に合ってしまうケースが多いかもしれません。それと、「H[Σ]がやせている」という条件は外したほうがいいときもあるでしょう。

ファイバーであるモデル圏M[Σ]が同じでも、ベースとなる指標圏の射の選び方で、状況は随分と変わります。例えば、インターフェース(指標)のリネーミング変換を許すかどうかで階層構造の雰囲気がガラっと変わります。[/追記]