Cartesian Cubical型理論の概説(1)

　Cubical型理論の覚書です。AIを使うことでここ1か月ほど急速にこの分野にキャッチアップすることに成功しつつあるのですが、いかんせんまともに資料がまとめられていないために、多数の混乱を自分はしました。おそらく今もまだ悩んでいる……が、アウトプットしない限りにはまったく頭が整理されない。

Cubical型理論

　Cubical Type Theoryですごく簡単に言うと「Martin-Löf依存型理論+区間$I$+面論理」とからなり、Homotopy Type TheoryのUnivalenceなどを計算的に実現する型理論です。
　Cubical Type Theoryには2種類の流儀があります。

• CCHM (Cohen, Coquand, Huber, Mörtberg, 2016)
• CCTT (Cartesian Cubical Type Theory, 2019)

いずれの流儀でも区間(Interval)$I$と面論理(Face Logic)を依存型理論に追加した構造となっています。

直観的な説明

　Cubical型理論では$0 : I$と$1 : I$という2つの端点からなる区間(Interval)$I$を導入して、Homotopy型理論におけるPath型のかわりに、項同士の間に区間を「貼り付ける」ことによって等号論理を形成します。
　Homotopy型理論でのPath型とは

• Formation: $A$が型ならば、型$A$の項$a$および$b$に対してPath型$a =_{A} b$は型である。
• Introduction: 型$A$の項$a$に対して$\mathrm{refl}(a)$はPath型$a =_{A} a$の項である。

このIntroductionルールでなぜ多様な等式が出るのか甚だ謎だと思うけれども、それは後になってHIT (Higher Inductive Type)まで行って代数的データ型に自由にPathを定義するようにすると、それを除去する目的で使えることがわかるという理解をすればいいと思う。

• Elimination: 第一にPath型$a =_{A} b$の要素$p$があったときに、要素$p$に応じた型を返す関数$P$をモチーブ(motive)と呼ぶ。これに、Path型の項$p$を除去するためには、道$p$に応じてケース分けするので、その端点$a$と使用する道$p$とから、除去結果を返す関数$r : A \rightarrow P(p)$を第二に必要とする。これらを得たときに$ind_{=_{A}}(P, r)$は$(a : A) \rightarrow (b : A) \rightarrow (p : a =_{A} b) \rightarrow P(p)$型の関数である。
• Computation: 帰納$ind_{=_{A}}(P, r)$は
  $$
  ind_{=_{A}}(P, r) (x, x, p) \equiv r(x)
  $$
  で計算する。

自分はこのPath型のEliminationにはとても納得していなくて、何度も考え直しては意味わからんとなっている。というのもHITで定義する道$p$を除去するには、左の端点$a$と右の端点$b$に依存して項を除去しなければならないので、除去本体である$r$は$a$と$b$を引数に取らないと、HITまでのPath帰納法には効かないのではないか？と直感では思ってしまう。要するに$ind_{=_{A}}(P, r) (x_{0}, x_{1}, p) \equiv r(x_{0}, x_{1})$のほうが正しくないか？と思うわけ。この問題は関数$r$が2変数になるのはいいとして、$r$が部分関数になって、すべての$x_{0}, x_{1}$に対して定義されない関数になるという問題はある。
The HoTT BookのPath型は後半の章でHITが出るだいぶ前で定義されてしまうから、この時点で$\mathrm{refl}(a)$だけでしか導入(Introduction)できない正型(Positive Type)であるPath型(2025年現在でいえばむしろPath型というよりId型な気もするが)ではこの定義でいいと思うが、後ろのHITにおけるPath導入まで一貫して説明できているとは思えない。ほとんどThe HoTT Bookという聖書に対して、ダーウィンの進化論的に間違った記述があると主張しているような、信徒でありながらThe HoTT Bookの批判をしているわけだが、いまだに納得できない。
いやでも、こう書いてみると、結局、このThe HoTT Bookの1章で定義するPath型は$\mathrm{refl}(a)$を送る先を指定さえできればいいのだから、現在の定義でもいいのでは？という気もしてくる。いずれにせよ、この後に説明するCartesian Cubical型理論では、そもそも型$A$を区間文脈$\Psi$で分割し、$A$の点要素(0次元)と線要素(1次元)と正方形要素(2次元)と立方体要素(3次元)などと分けるわけだから、聖典であるHoTTの悪しき定式化なんぞ、今更どうでもいいという気もしてくる。

の4つのルールから成る型でした。(The HoTT Bookを読むか、日本語の一部抜粋翻訳みたいな資料を読むかで確認にしてください)

このような等式型の導入は、あとでCubical型理論でのPath型と対比するとわかるように、型$A$に外側から等式型を追加する構造でした。私の理解では結局、このような外側からの等式の追加が、延いてはUnvialenceさえも公理として外側から追加する必要となる理由で会って、従って計算的な理論ではなくなった理由であると理解しています。

　一方で、Cubical型理論ではPath型とは大まかに言えば「区間$I$から型$A$への関数」で、「端点の行き先が判断的(judgementally)に決まっている」型です。ただ、ここが初見殺しポイントで、CCHM流とCCTT流でPath型の扱いが違うのです。CCHM流に言えば、
$$
\mathrm{Path}(A, a, b) \equiv I \rightarrow A \quad \text{s.t.} \quad p : \mathrm{Path}(A, a, b),\quad p(0) := a,\quad p(1) := b
$$
CCTT流に言えば、
$$
\begin{align}
\Psi, i : I; \phi; \Gamma & \vdash A(i) \quad \text{type} \newline
\Psi, i : I; \phi;\Gamma & \vdash a : A(0) \newline
\Psi, i : I; \phi;\Gamma & \vdash b : A(1) \newline
\Psi, \phi;\Gamma & \vdash \mathrm{Path}_{<i> A(i)}(a, b) \quad \text{type} \newline
\end{align}
$$

ただし、ここでCCHMが型理論的で、CCTTが自然演繹風に記述しましたが、オリジナル文献がこういった記法をしているので、素人の自分はこのような形で書かないと正しく議論できないから、このように比較して書いているにすぎません。記法の問題ではなく、むしろ区間$I$がCCHMでは「型」として、CCTTでは「文脈」として登場することのほうがずっと重要です。

ここで区間$I$の扱いがどのように違うかというと、

• CCHM: 区間$I$はDe Morgan代数を満たす代数系を満たす型となっており、それ自体が代数レベルで直観的で幾何学的な区間となっている。$i, j : I$があれば、$i \land j$や$i \lor j$、$\neg i$が区間$I$の要素として認められる。従って、$i, j$に具体的に端点$0$や$1$を代入しなくても、区間内の点同士の大小比較$(i \land j) \lt (i \lor j)$とかは議論できてしまいます。加えて、すべての次元変数$i, j : I$が同一区間内で議論されるので、Principal化といって、$N$次元立方体(要するに$i, j, k \cdots$複数の次元があるとして)での議論を、Kan合成方向ではない$j, k, \cdots$についてぐちゃりと潰して、単一の次元変数$i$における$0 \rightarrow 1$の議論に純粋に落とし込んでしまうことができます。この結果、面論理は実のところ$\mathrm{isOne}$という、区間の要素$I$の要素を一つ取って「$i = 1$」という単一の方法のみを採用すればよいです。この$\mathrm{isOne}$で面を構成することで、すべての面を作れます。実際に、面論理「$i = 0$」は「$(\neg i) = 1$」ですし、面論理「$i = 1 \lor j = 1$」は「$(i \lor j) = 1$」です。

(オリジナルのCCHMではPricipal化による$\mathrm{isOne}$であらゆる面を作るのではなく、面論理側にも$\land$や$\lor$が入る設計になっています。しかしDe Morgan代数によって、面論理側の演算子は不要になると理解していいようです。一方で、面論理には$\neg$が出てこないのが特徴で、なぜなら面の否定をすると、そのほかの面全てを意味することになるためです。とAIに言われたのだが自分は納得していない。そもそも文脈って$x : A$というコンテキストはあっても「$x : A$ではない」って文脈をそもそもみないのと同じなのかなぁ)

• CCTT: 区間$I$では代数演算を認めません。したがって、純粋に区間$I$は$0$または$1$からなっており、型でさえなく、区間文脈$\Psi$(Interval Context)の記号でしかありません。その代わり、面論理では軸変数$i : I$に対して「$i = 1$」に加えてCCHMでは省略できた「$i = 0$」が必要です。さらに、面論理$\alpha, \beta$に対して「$\alpha \land \beta$」「$\alpha \lor \beta$」も面論理として認めます。区間$I$が豊かな幾何的な構造を持たない代わりに、面論理で豊かな幾何的な構造が実現されるのが特徴です。

という対比になっています。今回はCCHMについて詳しく記載しないですが、Kan合成がCCHMでは$0 \rightarrow 1$のみ用意すればいいのです。一方で、CCTTではKan合成は任意の$r \rightarrow r'$に用意しないといけないという差が生まれます。

CCHMはCCTT以上にプログラミング言語的にどのように実現したらいいかわからないという状況があります。次元変数とか軸変数同士の代数演算があるので、項の記述(要するにλ計算のあるパートの文法)でこれの計算を記述しないとだめなのですが、これがあるおかげで$I \rightarrow A$型というのと、端点が固定された$\mathrm{Path}(A, a, b)$の二種類が区間$I$を引数に取る関数型として採用する必要が出るのです。しかし、コンパイラ側である項$p$が区間$I$を引数に取る関数型であるとして、端点をそれぞれ$a$および$b$と計算をできてしまったら、$Path(A, a, b)$で推論するのか？という疑問が起きます。そして、そうなると$\mathrm{Path}(A, a, b)$は$I \rightarrow A$の部分型なのか？とか思うし、部分型は入れたくないぞ？とかいろいろな問題が波及するのです。

次回予告

次回はKan合成についてまとめます。