スピヴァックの関手データモデルは、実に示唆に富んでいます。スピヴァックのアイディアは、データモデルに限らず、ソフトウェアシステムのさまざまな側面のモデル化に使えそうです。
関手データモデルの要点を簡略にまとめるなら：
- （データベース）スキーマは圏である。
- （データベース）スキーマの制約は可換図式である。
- （データベース）スキーマの全体は“圏の圏”である。
- （データベース）インスタンスは（データベース）スキーマからの関手である。
- （データベース）インスタンスのあいだの準同型射は自然変換である。
括弧のなかに入れた「データベース」を他の言葉で置き換えてもこの発想は通用します。実際の適用例はいずれ出すつもりですが、まずは、この発想の一般的な枠組みをハッキリさせておきましょう。
スキーマは圏なので、S, T のようなイタリック体文字で表すことにします。“スキーマの全体”もまた圏を形成しますが、個々のスキーマとは区別するために、Schのようなイタリック体太字としましょう。Schは、すべての小さな圏からなる圏Catの部分圏だとします*1。
他に、スキーマをインスタンスとして具現化するための環境となる圏（アンビエント圏）Cも考えます。Cは小さい圏である必要はありません。例えば、C = Set としてかまいません。
Sをスキーマ（S∈|Sch|）として、S上のCインスタンスとは、関手 F:S→C のことです。インスタンスのあいだの変換とか準同型射とは、自然変換 α::F⇒G:S→C のことです。関手と自然変換は圏を作るので、この圏を InstC[S] と書きます。より簡略に、CS とか [S, C] とも書きます。
圏Schの射をスキーマ射と呼びましょう。スキーマ射は、スキーマ変換を与える関手です。スキーマ射は、σ、ρなどのギリシャ小文字で表すことにします*2。ギリシャ文字で書いても自然変換ではなく関手なので注意してください。
さて、σ:S→T がスキーマ射のとき、T上のインスタンスは、σによりS上に引き戻されます。Fを F:T→C という関手、つまりT上のインスタンスだとして、
- σ*(F) := σ;F
とすれば、σ* が関手から関手への対応を定義します。同様に、自然変換（関手圏の射）α::F⇒G:T→C に対して、σ*(α)A := ασ(A) （A∈|S|）として、自然変換から自然変換への対応も構成できます。これらは全体として、関手圏 [T, C] から別の関手圏 [S, C] への関手σ*を定義します。関手データモデルでは、関手 σ*:[T, C] → [S, C] はスキーマ変換に伴う単純データマイグレーションとなっています。
いま定義した関手σ*を、InstC[σ] と書いてみると、InstC[-] がインデックス付き圏となっていることが分かります。インデックス付き圏が出てきたらとりあえずグロタンディーク構成。この場合は、特定のスキーマ上じゃなくて、すべてのスキーマに渡ってインスタンスを寄せ集めた圏が構成できます。
実は、InstC[-] = [-, C] のCが必ずしも小さくない（例：C = Set）なので、サイズの問題があるのですが、気にしないことにしましょう。
一般に、H:D→C がインデックス付き圏のとき、そのグロタンディーク平坦化を積分記号を使って ∫(x∈D | H[x]) と書くことにします*3。“積分変数”xは、対象も射も表すものとします。今回のケースでは、グロタンディーク平坦化は ∫(s∈Sch | [s, C]) と書けます。平坦化には標準的なファイブレーション射影 ∫(s∈Sch | [s, C]) → Sch が伴います。
∫(s∈Sch | [s, C]) の作り方を振り返ると、この圏の射は、異なるスキーマ上のインスタンスを比較する方法を与えることがわかります。まず、スキーマ射 σ:S→T in Sch が誘導する引き戻しにより、スキーマT上のインスタンスを、スキーマS上にマイグレーション（引き戻し）します。すると、同じ世界（InstC[S]）のなかでの比較が可能となります。
さらに、∫(s∈Sch | [s, C]) という広い世界が手に入ったおかげで、異なるスキーマ上のインスタンスを組み合わせて別なインスタンスを作り出す方法が色々と可能となります。∫(s∈Sch | [s, C]) には、SchとCという2つのパラメータが入っているので、これを動かすことによって、多様な事例を作り出すことができます。
∫(s∈Sch | [s, C]) という、自由度が高くて良い構造を持った圏を発見したことがスピヴァックの大きな功績だと言えるでしょう。しばらくは、スピヴァックが見いだした広大な地平を探索してみるつもりです。
関連するエントリー：
