複圏〈オペラッド〉はその下部構造に複グラフを持ちます。導出システム〈演繹系〉は、概念的には複グラフそのものです。複グラフを依存型理論で利用したいとき、複グラフにも依存性を導入する必要があります。この記事で、依存性を持つ複グラフを導入します。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
%\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\hyp}{\text{－} }
\newcommand{\In}{ \text{ in } }
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\Imp}{\Rightarrow }
`$
内容：
複グラフ
ここで使う用語法では、複圏とオペラッドは完全に同義です（区別しない）。複圏〈オペラッド〉から、結合〈composition〉と恒等〈identity〉を忘れた構造を複グラフ〈multigraph〉と呼びます。複グラフについては以下の過去記事で書いています。
導出システムと演繹系は完全に同義です。複グラフと導出システムも、分野が違うだけで同じ概念です。導出システム〈演繹系〉については以下の過去記事で書いています。
概念としては：
- 複圏 ＝ オペラッド
- 複グラフ ＝ 導出システム ＝ 演繹系
また、圏は特別な複圏とみなせます。しかし残念なことに、異なる分野で扱われるので、同じ概念に別な呼び名が付いています。以下の表のようです。（縦棒は「または」、疑問符は省略可能を意味します。）
| 圏 | 複圏〈オペラッド〉 | 複グラフ | 導出システム〈演繹系〉 |
|---|---|---|---|
| 対象 | 色、対象 | 頂点、ノード | 文 |
| {色 | 対象}リスト | {頂点 | ノード}リスト | 文リスト | |
| 射 | 複射、オペレーション、オペレーター | 複辺、辺 | 基本導出ステップ |
| 域 | ソース{リスト}? | 始点リスト、ソース{リスト}? | 仮説、前提 |
| 余域 | ターゲット{色 | 対象}? | 終点、ターゲット{頂点 | ノード}? | 結論 |
| 複パス、ツリー | 導出ツリー |
呼び名と書き方を決める
複グラフを話題にしたいのですが、複グラフは複圏〈オペラッド〉の下部構造として出現することが多いです。圏の下部構造であるグラフ〈有向グラフ〉は複グラフの特別なものとみなせます。複グラフと導出システム〈演繹系〉は同じ概念です。導出システムは型理論の文脈でも登場します。
複グラフというひとつの概念に対して、文脈や由来・習慣によって、様々な呼び名があり、呼び名にちなむ書き方〈記法〉もたくさんあります。
複グラフ $`X`$ の“頂点の集合”を表すために、次のような書き方があるでしょう。
- $`\mrm{Obj}(X)`$ （set of objects）
- $`\mrm{Color}(X)`$ （set of colors）
- $`\mrm{Vert}(X)`$ （set of vertices）
- $`\mrm{Node}(X)`$ （set of nodes）
- $`\mrm{Sen}(X)`$ （set of sentences）
- $`\mrm{Sort}(X)`$ （set of sorts）
- $`\mrm{Type}(X)`$ （set of types）
複グラフ $`X`$ の“辺の集合”を表すために、次のような書き方があるでしょう。
- $`\mrm{Mor}(X)`$ （set of morphisms）
- $`\mrm{Oper}(X)`$ （set of {operations | oprators}）
- $`\mrm{Edge}(X)`$ （set of edges）
- $`\mrm{Multiedge}(X)`$ （set of multiedges）
- $`\mrm{Step}(X)`$ （set of {primitive}? derivation steps）
- $`\mrm{Inference}(X)`$ （set of {primitive}? inference rules）
- $`\mrm{Function}(X)`$ （set of functions）
今ここでは次のように決めます。
- 複グラフ $`X`$ の“頂点の集合”を表すために、$`\mrm{Color}(X)`$ と書く。
- 複グラフ $`X`$ の“辺の集合”を表すために、$`\mrm{Oper}(X)`$ と書く。
つまり、オペラッド〈複圏〉の用語・記法を使います。
なお、$`\mrm{Sort}`$ は、$`\mrm{Color}`$ とは（似てるけど）少し違う意味で後で使います。
プロファイルと境界写像
$`X`$ は、圏、複圏〈オペラッド〉、複グラフ、導出システム〈演繹系〉のいずれかだとします。分野ごとの呼び名の違いを吸収するために、前節で決めた記法を使います。
- $`\mrm{Color}(X)`$ ： $`X`$ の{対象 | 色 | 頂点 | ノード | 文}の集合
- $`\mrm{Oper}(X)`$ ： $`X`$ の{射 | 複射 | オペレーション | オペレーター | 複辺 | 辺 | 導出ステップ | 推論規則}の集合
圏または複圏〈オペラッド〉または複グラフまたは導出システム〈演繹系〉 $`X`$ に対して、プロファイルの集合〈set of profiles〉 $`\mrm{Prof}(X)`$ を次のように定義します。
- $`X`$ が圏のとき：
$`\mrm{Prof}(X) := \mrm{Color}(X)\times \mrm{Color}(X) = \mrm{Obj}(X)\times \mrm{Obj}(X)`$ - $`X`$ が複圏または複グラフまたは導出システムのとき：
$`\mrm{Prof}(X) := \mrm{List}(\mrm{Color}(X))\times \mrm{Color}(X)`$
$`X`$ が圏であっても、複圏であっても、複グラフであっても、導出システムであっても、境界写像 $`\mrm{bdry}_X`$ を定義できます。サイズが小さい場合なら：
$`\quad \mrm{bdry}_X : \mrm{Oper}(X) \to \mrm{Prof}(X) \In \mbf{Set}`$
サイズが大きい場合なら（$`\mbf{SET}`$ は大きな集合達の集合圏）：
$`\quad \mrm{bdry}_X : \mrm{Oper}(X) \to \mrm{Prof}(X) \In \mbf{SET}`$
境界写像については、「複圏〈オペラッド〉とプレ準同型射の圏」を見てください。
「複圏〈オペラッド〉とプレ準同型射の圏」で導入したプレ準同型射〈pre-homomorphism〉とは、プロファイルのあいだの写像とオペレーションのあいだの写像のペア $`(F_\mrm{prof}, F_\mrm{oper})`$ で、境界写像を保存するもの（以下の可換図式）です。
$`\quad \xymatrix{
\mrm{Oper}(X) \ar[d]_{\mrm{bdry}_X} \ar[r]^{F_\mrm{oper}}
& \mrm{Oper}(Y) \ar[d]^{ \mrm{bdry}_Y }
\\
\mrm{Prof}(X) \ar[r]^{F_\mrm{prof}}
& \mrm{Prof}(Y)
}\\
\quad \text{commutative }\In \mbf{Set}
`$
$`\mrm{Prof}(X), \mrm{Oper}(X)`$ の由来も忘れてしまえば、プレ準同型射とは、バンドルのあいだのバンドル射に過ぎません。バンドル-ファミリー対応（「バンドル-ファミリー対応 再考」参照）により、バンドルからファミリーを作れます。そのファミリー〈集合族〉がホムセット〈homset〉です。
$`\quad \mrm{Hom}_X = {\mrm{bdry}_X}^{-1} : \mrm{Prof}(X) \to |\mbf{Set}|\In \mbf{SET}`$
依存複グラフ
複グラフ $`X`$ のプロファイルの集合は、$`\mrm{Color}(X)`$ を使って簡単に定義できました。
$`\quad \mrm{Prof}(X) := \mrm{List}(\mrm{Color}(X)) \times \mrm{Color}(X)`$
プロファイルとは、色リスト（$`\mrm{List}(\mrm{Color}(X))`$ の要素）と色（$`\mrm{Color}(X)`$ の要素）のペアです。プロファイルを具体的に書けば：
$`\quad ( (A_1, \cdots, A_n), B ) \\
\text{Where}\\
\quad (A_1, \cdots, A_n) \in \mrm{List}(\mrm{Color}(X))\\
\quad B \in \mrm{Color}(X)
`$
依存複グラフ〈dependent multigraph〉とは、プロファイルが依存性を持つかもしれないような複グラフです。今までの定義には依存性がありませんでした。依存複グラフのプロファイルにおいては、色リスト $`(A_1, \cdots, A_n)`$ の成分〈項目〉間に依存性があるかも知れず、色 $`B`$ も $`(A_1, \cdots, A_n)`$ に依存しているかも知れないのです。
依存性を定式化するには、色の集合の代わりに、色の集合族〈ファミリー〉を考えます。“インデックス付き集合のファミリー”を次のように書きます。
$`\quad \mrm{Sort}_X : \mrm{Ctx}(X) \to |\mbf{Set}| \In \mbf{SET}`$
呼び名は次のようです。
- $`\mrm{Ctx}(X)`$ ： 依存複グラフ $`X`$ のコンテキストの集合〈set of contexts〉
- $`\mrm{Sort}_X`$ ： 依存複グラフ $`X`$ のソートファミリー〈sort family〉
- $`\Gamma \in \mrm{Ctx}(X)`$ ： $`\Gamma`$ は、依存複グラフ $`X`$ のコンテキスト〈context〉
- $`A \in \mrm{Sort}_X(\Gamma)`$ ： $`A`$ は、依存複グラフ $`X`$ のコンテキスト $`\Gamma`$ 上のソート〈sort〉
呼び名〈用語〉は依存型理論に寄せています。
依存性がない複グラフ $`Y`$ を、依存複グラフの特別なものとみなすには、次のように定義します。
$`\quad \mrm{Ctx}(Y) := \mrm{List}(\mrm{Color}(Y))\\
\quad \mrm{Sort}_Y(\Gamma) := \mrm{Color}(Y)
`$
この場合、$`\mrm{Sort}_Y(\Gamma)`$ は $`\Gamma`$ に依存せず、常に一定値 $`\mrm{Color}(Y)`$ です。
さて、依存複グラフ $`X`$ のプロファイルの集合を定義しましょう。
$`\quad \mrm{Prof}(X) := {\displaystyle
\sum_{\Gamma \in \mrm{Ctx}(X)} \mrm{Sort}_X(\Gamma)
}`$
ここで、総和記号（シグマ）は、ファミリー〈インデックス付き集合族〉の成分〈値〉を直和で全部足し合わせた集合です。依存型理論で言えば、型ファミリーのパイ型です。
「依存型理論の道具を定義している最中に、依存型理論の概念を使うのか？」と不満や疑念をいだくかも知れませんが、よくあることです。循環論法で破綻しているわけではないので大丈夫です。
集合 $`\mrm{Prof}(X)`$ の要素は、次のようなペアですが、第一成分と第二成分のあいだに依存性があります。
$`\quad (\Gamma, B) \in \mrm{Prof}(X)\\
\text{Where}\\
\quad \Gamma \in \mrm{Ctx}(X)\\
\quad B \in \mrm{Sort}_X(\Gamma)
`$
依存複グラフでは、プロファイルの定義が複雑化していますが、プロファイルの集合 $`\mrm{Prof}(X)`$ さえ定義できれば、あとは通常の（依存性がない）複グラフと同じです。
依存複グラフの定義まとめ
依存複グラフ $`X`$ の構成素は次のものです。
- $`\mrm{Ctx}(X)`$ ： $`X`$ のコンテキストの集合
- $`\mrm{Sort}_X`$ ： $`X`$ のソートファミリー
- $`\mrm{Prof}(X)`$ ： $`X`$ のプロファイルの集合、コンテキストの集合とソートファミリーから定義する。
- $`\mrm{Oper}(X)`$ ： $`X`$ のオペレーションの集合
- $`\mrm{bdry}_X`$ ： $`X`$ の境界写像
境界写像は次の形になります。
$`\quad \mrm{Oper}(X) \ni \varphi \mapsto (\Gamma, B) \in {\displaystyle \sum_{\Gamma \in \mrm{Ctx}(X)} \mrm{Sort}_X(\Gamma)}
`$
$`\Gamma`$ を $`\varphi`$ のソースコンテキスト〈source context〉、$`B`$ を $`\varphi`$ のターゲットソート〈target sort〉と呼びます。もちろん、様々な分野、文脈、由来・習慣によって、たくさんの同義語があります。呼び名・書き方の違いは無視して、概念の同一性に注意を向けましょう。
依存型理論における依存複グラフの利用
前節で定義した依存複グラフを依存型理論に利用するときは、また若干の用語翻訳が必要です。
| 依存型理論 | 依存複グラフ |
|---|---|
| コンテキスト | コンテキスト |
| 型項〈型〉 | ソート |
| インスタンス項〈項〉 | オペレーション |
| ？ | ソースコンテキスト |
| ？ | ターゲットソート |
型理論では多くの場合、構文的対象物〈syntactic object〉である型項を単に「型」、インスタンス項を単に「項」と呼びます。それが習慣なのでしょうがないです。
さて、依存複グラフの場合も、圏・グラフと同様にホムセットを定義します。
$`\text{For }\alpha \in \mrm{Prof}(X)\\
\quad \mrm{Hom}_X(\alpha) = X(\alpha) :=
\{ \varphi \in \mrm{Oper}(X) \mid \mrm{bdry}_X(\varphi) = \alpha
\}
`$
依存型理論における型判断の形式
$`\quad \Gamma \vdash \varphi : B`$
は、依存複グラフ $`X`$ 内では次のように解釈されます。
$`\quad \varphi \in \mrm{Hom}_X( (\Gamma, B) )`$
ホムセットをもっと簡素に書けば：
$`\quad \varphi \in X( \Gamma, B )`$
今日定義した依存複グラフは、型判断形式の解釈に使えるだけですが、もっと構造を付け足すことにより、依存型理論の圏論的定式化であるC-システム（「カートメル／ヴォエヴォドスキー／パルムグレンの型理論」）に接近することが出来ます。
