思い付いた事があるんですが、ほっておくと忘れそうなので、ここに書いておきます。
指標の一部をパラメータにするという行為が、いったい何をしているのだろう? この行為を合理的に説明する枠組みは何だろう? ということがずっと分からなくてモヤモヤしてました。背後にある枠組みは、グロタンディーク構成じゃなかろうか、と思います。
内容:
用語と書き方の約束
指標と仕様の区別は相変わらず決めてません。ここでは、「指標〈signature〉」という言葉だけを使い、指標に法則を書いてもいいとします。次は、法則も書いてあるモノイドの指標です。
signature Monoid { sort A operation i:1→A operation m:A×A→A equation assoc:: (m×idA);m ⇒ (idA×m);m equation lunit:: (i×idA);m ⇒ idA equation runit:: (idA×i);m ⇒ idA }
これから出てくる指標はすべて集合圏で解釈すると約束します。つまり、sortは集合を宣言し、operationは写像を宣言します。1は特定された単元集合で、×はデカルト積です。
法則は等式的法則〈equational law〉だけを考えます。上記の等式的法則(equationで宣言)において、'='ではなくて'⇒'を使っているのは、厳密にはイコールではなくて自然同型だからです。自然同型は、デカルト積に関する律子〈りつし〉である α, λ, ρ を使って(自明に)構成されます。
上記モノイドの例は、名前付きの指標を定義する構文ですが、名前がない指標そのものを書くときは、ML言語をまねて sig {...} としてみましょう。行先頭が必ずキーワード〈予約語〉なので、改行しなくても区切り記号なしでも読めるはずです(とても読みにくいけど)。
sig {sort A operation i:1→A operation m:A×A→A equation assoc:: (m×idA);m ⇒ (idA×m);m equation lunit:: (i×idA);m ⇒ idA equation runit:: (idA×i);m ⇒ idA}
指標の話をしている文脈なら、先頭のsigも不要かもね。
{sort A operation i:1→A operation m:A×A→A equation assoc:: (m×idA);m ⇒ (idA×m);m equation lunit:: (i×idA);m ⇒ idA equation runit:: (idA×i);m ⇒ idA}
これでいいや -- 混乱のおそれがないときは、sigも省略する(波括弧で囲むだけ)にします。
指標において、(今の構文だと)sort, operation equation で始まる構文的単位を宣言文〈declaration〉と呼ぶことにします。指標は宣言文のリストだと捉えましょう。つまり、宣言文の順序も考慮します。宣言文の順序を入れ替えたら異なる指標になります。
リストとみなした指標の連接演算を記号 +> で書きます。例えば:
{sort A operation i:1→A} +> {operation m:A×A→A} = {sort A operation i:1→A operation m:A×A→A}
空な指標 {} が、連接演算 +> の単位元になります。
指標を表す変数は、(習慣に従い)ギリシャ文字大文字 Σ, Δ, Γ などを使います。空指標は小文字イプシロン ε で表します。例えば、連接演算 +> がモノイドの法則を満たすことは次のように書きます。
- (Σ +> Γ) +> Δ = Σ +> (Γ +> Δ)
- ε +> Σ = Σ
- Σ +> ε = Σ
指標の分割とパラメータ化/平坦化
与えられた指標Σを、Σ = Δ +> Σ' の形に書くことを、指標Σの分割〈partitioning〉と呼びましょう。この場合、Δはそれ自身で指標になりますが、Σ'が指標になるとは限りません。例えば:
{sort A operation i:1→A operation m:A×A→A} = {sort A operation i:1→A} +> {operation m:A×A→A}
という分割において、{operation m:A×A→A} は構文的に指標とは認められません。なぜなら、Aの宣言が存在しないからです(未宣言な記号がいきなり登場するのはダメ)。
Σの分割 Σ = Δ +> Σ' が与えられたとき、Δを頭部〈head〉、Σ'を残余部〈rest〉と呼ぶことにします。
指標Σの部分指標Γが、分割の頭部として含まれるとき、ΓはΣの頭部部分指標〈head subsignature〉と呼びます。部分指標として、頭部部分指標だけでも十分なので、今後は単に部分指標と言っても頭部部分指標の意味だとします*1。
指標Γが指標Σの部分指標(頭部部分指標)のとき、Γ ≦ Σ と書くことにします。次が成立します。
- Γ ≦ Σ ⇔ (Σ = Γ +> Σ' という分割が存在する)
- Σ ≦ Σ
- Γ ≦ Σ, Σ ≦ Δ ⇒ Γ ≦ Δ
- Γ ≦ Σ, Σ ≦ Γ ⇒ Γ = Σ
- ε ≦ Σ
指標Δと、指標とは限らない宣言文のリストΣ'があるとき、Δ +> Σ' が指標になるならば、ΔとΣ'は(この順で)許容ペア〈admissible pair〉と呼びましょう。
ΔとΣ'が指標と宣言文リストの許容ペアのとき、(Δ)Σ' という構文的形式を新たに指標とみなします。この形の指標をパラメータ付き指標〈signature with parameter | parameterized signature〉と呼び、Δをパラメータと呼びます。
Σ = Δ +> Σ', Γ = Σ +> Γ' のとき、入れ子のパラメータ付き指標 ((Δ)Σ')Γ' も認めます。次は入れ子のパラメータ付き指標の例です。
( ({sort A operation i:1→A}) {operation m:A×A→A} ){ equation assoc:: (m×idA);m ⇒ (idA×m);m equation lunit:: (i×idA);m ⇒ idA equation runit:: (idA×i);m ⇒ idA }
指標Σに対して、その分割 Σ = Δ +> Σ' をみつけてパラメータ付き指標 (Δ)Σ' を作ることをパラメータ化〈parameterize〉、その逆に、パラメータ付き指標 (Δ)Σ' から Δ +> Σ' を作ることを平坦化〈flattening〉と呼びます。
意味論は?
前節で述べた、指標のパラメータ化や平坦化は、構文的な操作としてはハッキリしています。しかし、対応する意味的〈セマンティック〉操作は何でしょうか? パラメータ化した指標は、平坦に書いた指標とは何か違う感じはします。何が違うのでしょう?
具体例を挙げます。いきなり平坦に書いたモノイドの例は最初に挙げました。いきなりではなくて、少しずつモノイドを定義してみます。
signature PointedSet { sort A operation i:1→A } signature PointedMagma { sort A operation i:1→A operation m:A×A→A } signature Monoid { sort A operation i:1→A operation m:A×A→A equation assoc:: (m×idA);m ⇒ (idA×m);m equation lunit:: (i×idA);m ⇒ idA equation runit:: (idA×i);m ⇒ idA }
これから、PointedSet ≦ PointedMamga ≦ Monoid だと分かります。別な言い方をすれば:
- PointedMagma = PointedSet +> {operation m:A×A→A}
- Monoid = PointedMagma +> {equation assoc:: (m×idA);m ⇒ (idA×m);m equation lunit:: (i×idA);m ⇒ idA equation runit:: (idA×i);m ⇒ idA}
この例の、「少しずつ順に定義が進む」感じは、入れ子のパラメータ化でも表現できます。
signature Monoid ( signature PointedMagma ( signature PointedSet { sort A operation i:1→A } ) { operation m:A×A→A } ) { equation assoc:: (m×idA);m ⇒ (idA×m);m equation lunit:: (i×idA);m ⇒ idA equation runit:: (idA×i);m ⇒ idA }
差分記述になっているので、クラス継承を連想する人もいるでしょう。
signature PointedSet { sort A operation i:1→A } signature PointedMagma extends PointedSet { operation m:A×A→A } signature Monoid extends PointedMagma { equation assoc:: (m×idA);m ⇒ (idA×m);m equation lunit:: (i×idA);m ⇒ idA equation runit:: (idA×i);m ⇒ idA }
いずれにしても、「いきなり一度に vs. 少しずつ順に」という対立/相互関連の意味論が問題になります。
指標と相対指標の意味論
ここまで問題意識を説明してきたのですが、ここから先は急ぎ足、あるいは雑です。未確認なことも含まれます。
まず、単一の指標Σがあったとき、その意味とは何か? を決めましょう。色々な立場がありますが、指標Σのモデルの圏〈category of models〉Mod[Σ] が“Σの意味”だとします*2。Mod[Σ] が何であるかをちゃんと述べると長くなるので、事例で雰囲気だけ。
- 例に出しているモノイドの指標 Monoid に関して Mod[Monoid] = Mon = (モノイドの圏)
- 例に出している付点集合の指標 PointedSet に関して Mod[PointedSet] = PtSet = (付点集合の圏)
- Mod[{sort A}] = Set = (集合の圏)
- Mod[ε] = Mod[{}] = I = (単一の対象と恒等射だけの圏)
Δ ≦ Σ である指標のペア (Δ, Σ) を相対指標〈relative signature〉と呼びます。以下の言い方はすべて同じことです。
- (Δ, Σ) は相対指標である。
- Σ = Δ +> Σ' は指標の分割である。
- (Δ, Σ') は(指標と宣言文リストの)許容ペアである。
相対指標 (Δ, Σ) に対して、Mod[Δ], Mod[Σ] の二つの圏が考えられます。この二つの圏は、もちろん無関係ではありません。すぐに分かる関係性は、Mod[Σ]からMod[Δ]への忘却関手の存在です。例えば:
- Mod[Monoid] = Mon から Mod[PointedSet] = PtSet への忘却関手が存在する。モノイドの乗法と法則を忘れて、台集合と単位元だけを残す。
- Mod[PointedSet] = PtSet から Mod[{sort A}] = Set への忘却関手が存在する。付点集合の点を忘れて、台集合だけを残す。
Mod[{sort A}] = Set から Mod[ε] = I への自明な関手も存在します。これを忘却関手と呼んでいいかは議論があるでしょうが(忠実関手であることを仮定することもあるので)、「なにもかも忘れてしまう」ことなので、極端で自明な忘却関手といってもいいでしょう。
相対指標を忘却関手により意味付けることは、分かりやすく、2個以上の指標の系列にも適用できます。例えば、ε ≦ {sort A} ≦ PointedSet ≦ Monoid という指標の系列には、Mon→PtSet→Set→I という忘却関手の系列が対応します。
相対指標 (Δ, Σ) に対する忘却関手を U(Δ, Σ) または UΔ≦Σ と書くことにします。
- UΔ≦Σ:Mod[Σ]→Mod[Δ]
相対指標を忘却関手で意味付けることは、指標のあいだの射を順序 ≦ だとした圏 ThinSign からのモデル圏関手*3を考えることと同じです。つまり、ModU:ThinSign→CAT という反変関手を次のように定義します。
- For Σ∈|ThinSign|, ModU[Σ] := Mod[Σ]
- For (Δ ≦ Σ)∈ThinSign(Δ, Σ), ModU[Δ ≦ Σ] := UΔ≦Σ:Mod[Σ]→Mod[Δ]
パラメータ付き指標の意味論
さて、本論であるパラメータ付き指標の意味論です。記法を簡略化するために、前節で述べた意味論をスコットブラケット*4で書くことにします。CATは、小さいとは限らない圏の圏です。
- 指標Σに対して、〚Σ〛 := Mod[Σ] ∈|CAT|
- 相対指標 Δ ≦ Σ に対して、〚Δ ≦ Σ〛 := (UΔ≦Σ:〚Σ〛→〚Δ〛) in CAT
(Δ)Σ' の形のパラメータ付き指標に対しても、〚(Δ)Σ'〛 は圏として意味付けます。それとは別に、もうひとつの意味割り当て 《(Δ)Σ'》 も定義します。〚(Δ)Σ'〛と《(Δ)Σ'》を行ったり来たりしながら、解釈を構成しましょう。
(Δ)Σ' はパラメータ付き指標で、Δはパラメータ無しだとします。したがって、〚Δ〛 = Mod[Δ] ∈|CAT| は定義できます。〚Δ〛は、パラメータΔのモデルの圏です。圏〚Δ〛の対象Xを取ると、指標Δに実体Xを“代入”することができて、新しい指標 (X)Σ' が生まれます。例えば、パラメータ付き指標 (PointedSet)Monoid' に、〚PointedSet〛 = PtSet の対象である (N, 0) を代入すると、((N, 0))Monoid' は、自然数の集合N上の0を単位元とするモノイドの指標になります。
|〚Δ〛|∋X Mod[(X)Σ'] という対応は、〚Δ〛→CAT という関手に拡張できて、〚Δ〛をインデックスの圏〈indexing category〉とするインデックス付き圏になります。パラメータ付き指標 (Δ)Σ' からこの手順で作られたインデックス付き圏を 《(Δ)Σ'》 と書きます。
- 《(Δ)Σ'》:〚Δ〛→CAT (インデックス付き圏)
インデックス付き圏があれば、グロタンディーク構成ができます。グロタンディーク構成に関しては、「グロタンディーク構成と積分記号」で述べた記号法を使って、《(Δ)Σ'》の平坦化圏を次のように書きます。
あるいは無名変数(ハイフン)を使って、
グロタンディーク構成は、平坦化圏だけでなくフィイバー付き圏を定義するので、ファイバー付き圏は次のように書きます。
ここで、 は、パラメータ付き指標 (Δ)Σ' が定義する射影関手です。
さて、パラメータ付き指標 (Δ)Σ' に対する〚(Δ)Σ'〛は次のように定義します。
この記法を使うと、(Δ)Σ' が定義するファイバー付き圏は:
ここまで、Δはパラメータ無しだと仮定してきましたが、〚(Δ)Σ'〛の定義ができたので、帰納的な定義により、入れ子になったパラメータ付き指標に対しても 〚(Δ)Σ'〛と《(Δ)Σ'》を定義できます。
パラメータ無し指標に対する《Σ》は、空指標を使って 《Σ》 := 《(ε)Σ》 として定義します。この定義から、《Σ》はインデックス付き圏で、《Σ》:〚ε〛→CAT となります。〚ε〛 = I だったので、《Σ》:I→CAT、つまり、《Σ》は単一の圏と思ってかまいません。その単一の圏は 〚Σ〛= Mod[Σ] です。
指標のパラメータ化の基本的な性質
指標のパラメータ化に関して、今まで疑問に思ってきたことがあります。
- 指標Σの分割 Δ +> Σ' と、パラメータ付き指標 (Δ)Σ' が同じように見えるのはなぜなのか?
- しかし、指標Σの分割 Δ +> Σ' と、パラメータ付き指標 (Δ)Σ' はやはり違うように見えるのはなぜなのか?
おそらく、「同じように見える」理由は、〚Δ +> Σ'〛と〚(Δ)Σ'〛が同型だからでしょう。そして、「違うように見える」理由は、《Δ +> Σ'》と《(Δ)Σ'》がまったく別物だからでしょう。
〚Δ +> Σ'〛と〚(Δ)Σ'〛が同型性は次の可換図式で与えられます。(Σ = Δ +> Σ' とします。)
問題は、図式中にFとラベルされた関手の構成です。これは、定義を追いかければ出るでしょう(ちゃんとやってないけど)。
今回の思い付きのキモは、指標Σがパラメータ無しでもパラメータ付きでも、〚Σ〛と《Σ》という二種類の(互いに関連する)セマンティクスが使えることです。〚Σ〛は《Σ》からグロタンディーク平坦化で得られるので、大雑把に書けば 〚Σ〛 = ∫《Σ》 という関係で結ばれています。
〚-〛と《-》を利用することにより、(少なくとも僕にとっては)ハッキリしなかった指標のパラメータ化のメカニズムと性質が、少しは分かる気がします(期待感)。
型理論へ
指標は、オブジェクト指向の言葉では(アサーション付きの)インターフェイスです。関数型言語の言葉では(制約付きの)型クラスです。インターフェイス/型クラスは、一種の“型”とみなせます。よって、指標の理論とは型理論だと言えます。
我々は「指標の意味は圏だ」としているので、対応する型理論は、
- Categories-as-Types の型理論
です。パラメータ付き指標 (Δ)Σ' に対して、インデックス付き圏としての意味 《(Δ)Σ'》 を定義しました。これは、
- IndexedCategories-as-Types の型理論
になります。インデックス付き圏にグロタンディーク構成を施すとファイバー付き圏ができるので、それに注目すると、
- FibredCategories-as-Types の型理論
になります。
インデックス付き圏 《(Δ)Σ'》:〚Δ〛→CAT は、型インスタンス(対象)ごとに型(圏)が決まるので、依存型といえます*5。ファイバー付き圏 ∫《(Δ)Σ'》 →〚Δ〛 は、「派生型→基底型」という階層構造を定義するので、階層的型といえます。依存型←→階層的型 と、グロタンディーク構成(とその逆)で相互に移りあえます。
型〈type〉と一緒に項〈term〉を考える必要があります。Categories-as-Typesの立場で項を考えるならば:
- Functors-as-Terms
- IndexedFunctors-as-Terms
- FiberedFunctors-as-Terms*6
と考えるのが自然でしょう。
指標(インターフェイス/型クラス)を型として、それに依存性と階層性を入れ、型と共に項を扱う型理論 -- そのスタートとして、パラメータ化の明確化が必要です。
*1:これは話の単純化のためです。実用上は、頭部部分指標ではない部分指標もちゃんと扱ったほうがいいでしょう。
*2:Mod は Model の先頭3文字です。Mod は Module〈加群〉の先頭3文字でもあるので、Mod[R] はR係数の加群の圏の意味で使われることがあります。これは単なるコンフリクト(偶発的な衝突)です。
*3:「モデルの圏」を「モデル圏」と書いてますが、ホモトピー理論などに出てくる「モデル圏」はまったく別物なので注意してください。
*4:括弧記号自体は "white square brackets"〈白抜き角括弧〉と呼ぶようです。
*5:依存型は値に依存する型で、型に依存する型は総称型だとか区別する人もいるでしょう。が、なにか(それが値であれ型であれ)に依存する型を依存型と呼んでいます。
*6:圏論の用語法は整合性がないので、フィイバー付き圏のあいだの構造を保つ関手をファイバー付き関手〈fibred functor〉とは呼んでないようです。まったく別な意味のファイバー関手〈fiber functor〉があるからでしょう。ファイバー付き構造保存関手はデカルト関手〈cartesian functor〉と呼ばれることが多いですが、困ったことに、デカルト圏のあいだの構造保存関手もデカルト関手です。