大反省 (1)： 概念ベン図と木・林

具体例

$`\quad \xymatrix{
\text{バンドル} \ar@{=}[r]
&\text{写像}
}`$

$`\quad \xymatrix{
\text{バンドル} \ar@{=}[r]^{\sim}
&\text{ファミリー}
}`$

$`\quad \xymatrix{
\text{ファミリー} \ar@{=}[r]^{\sim}_{\text{グロタンディーク構成}\to}
&\text{バンドル}
}`$

$`\quad \xymatrix{
\text{ファミリー} \ar@{=}[r]^{\sim}
&\text{全射的関係}
}`$

$`\quad \xymatrix{
\text{ファミリー} \ar@{=}[r]^{\sim}_{\text{incl}\to}
&{\text{低木林}\subset \text{林}}
}`$

$`\quad \text{木}\subset \text{林}`$

$`\quad \xymatrix{
\text{林} \ar@{=}[r]^{\sim}_{\text{addRoot}\to}
&{\text{木}}
}`$ もともとの木は、ルートが新規追加される。$`T \mapsto T_\bot`$ となる。

$`\quad \text{無交差ファミリー} \subset {\text{ファミリー}}
`$

$`\quad \xymatrix{
\text{無交差ファミリー} \ar@{=}[r]^-{\sim}_{\leftarrow\text{tagging}}
&{\text{ファミリー}}
}`$ これは弱いEPペアだ。

$`\quad \xymatrix{
\text{無交差ファミリー} \ar@{=}[r]^-{\sim}_{\text{タギング無しグロタンディーク構成}\to}
&{\text{バンドル}}
}`$

$`\quad \xymatrix{
\text{グラフ} \ar@{=}[r]_-{\text{incl}\to}
&{\text{閉じた有向半グラフ} \subset \text{有向半グラフ}}
}`$

$`\quad \xymatrix{
{\text{有向半グラフ(例外ループ除外)}}
\ar@{=}[d]^{\sim}
\\
{ \text{頂点2色付きグラフ} \subset \text{頂点色付きグラフ} }
}`$

$`\quad \xymatrix{
\text{グラフ} \ar@{=}[r]^-{\sim}
&{\text{頂点色無しグラフ} \subset \text{頂点色付きグラフ}}
}`$

$`\quad \xymatrix{
\text{木} \ar@{=}[r]_-{\text{incl}\to}
&{\text{林}}\ar@{=}[r]_-{\text{roo-to-leaf}\to}
&{ \text{root-to-leaf 林グラフ} \subset \text{グラフ}}
}`$

新規ルートが追加される例や自然同値はもっと精密な記述が必要だ。

補足説明

高校の順列組み合わせで樹形図が出てくる。樹形図が場合の数え上げ〈列挙〉に使われる。「1つの場合←→ルートからのパス」と対応する。木〈ツリー〉または林〈フォレスト〉 $`A`$ のすべての「ルートからのパス」の集合を $`\mathrm{Data}(A)`$ と書く。これを 木または林のデータ集合と呼ぶ。

林（特別な場合として木を含む）のデータ集合の概念があれば、依存型理論はだいたいOK。次の概念は明確になる。

• リスト： 特殊な林のデータ集合の要素
• タプル： 多少特殊な林のデータ集合の要素
• レコード： タプルだがレベル識別子〈キー〉に名前を許す
• 依存ペア： 高さ1の林のデータ集合の要素
• 個体： 高さ0の林のデータ集合の要素
• 依存タプル： 一般的な林のデータ集合
• 依存レコード： 依存タプルだがレベル識別子〈キー〉に名前を許す

レベルのノード集合が、前レベルのノードごとに無交差コピーを使っているか、交差して共有するかの違いも重要。

「集合 → ファミリー → バンドル」あるいは「集合 → ファミリー → (無交差ファミリー → バンドル)」の繰り返しで林の全体を作っていく。そのプロセスは、“繰り返しグロタンディーク構成”になる。これは高さレベル（自然数）に沿った帰納的構成になる。

1. 高さ0の林がある。
2. 高さ0のノード集合（ルート集合と同じ）が空なら終わり。結果は空林。
3. 高さ0の林の高さ0のノード集合上のファミリーを考える。
4. ファミリーからのバンドル構成をする。
5. 高さ1のノード集合が空なら終わり。
6. 高さ1の林がある。
7. 高さ1の林の高さ1のノード集合上のファミリーを考える。
8. ファミリーからのバンドル構成をする。
9. 高さ2のノード集合が空なら終わり。
10. 高さ2の林がある。
11. 以下同様、繰り返し

特殊な林

1. 低木
2. 低木林
3. 二進木〈二分木〉
4. 竹
5. 竹林