この記事は、連載シリーズ企画の第２回目です
Arend という定理証明支援系について、全７回にわたってお伝えしています。
初回は、Arend が ホモトピー型理論（HoTT, Homotopy Type Theory）を公理としてではなく、計算して確かめる対象として扱っていること。そして、そこから何が期待されるのかをお伝えしました。
連載２回目となるこの記事は、その続編です。
初回記事では、２つのことを述べたまま先へ進みました。
１つは、「等しさの根拠を区別できると、何ができるようになるのか」です。
- 移送
- 商型
- 関数外延性
この３つの名前を挙げただけで、中身には触れていません。
もう１つは、「Arend は正準性を持たない」ということです。
弱みであると述べ、Cubical Agda との違いは理論の複雑さにあるとだけ記しました。
この記事から次回の記事にわたって、この２つの論点を掘り下げます。
本記事のExecutive Summary
本記事を読むと、何が分かるのか
結論を先に述べます。
２つの対象の「等しさ」に複数の異なる根拠（理由）があるとき、２つの対象が「等しい」複数の理由（根拠） を 区別して扱うことができる のが、2000年代に登場した比較的新しい数学理論である HoTT（ホモトピー型理論） です。
なお、HoTT の全体をこの一文で定義できるわけではありません。
本連載シリーズでは、HoTT の 特徴の１つ として「等しさの根拠そのものを対象として扱える」点に注目します。
HoTTを取り扱える ２つの定理証明言語 ── Arend と Cubical Agda ── は、ある一点で、その設計判断が分かれました。
その判断が何であり、それぞれの言語が何を得て、何を失ったのか。
この記事は、これらの論点を主題に掲げます。
本記事をお読みいただくことで、定理証明言語の設計に「正解」がない ということにお気づきいただけると思います。
Arend と Cubical Agda の設計者は、それぞれ優先して手にすべきものと、その代償として失っても構わないもの選び取る決断をした からです。
本稿：３つの論点
以下の３つの論点の並び順（① → ② → ③）は、本記事の中で各論点が登場する順番に並べています。
| 論点 | 読者が受け取るもの | 本記事での扱い | |
|---|---|---|---|
| ① | 等しさの根拠を識別して扱えると、何ができるようになるのか | ３つの具体的な効能 | 概要のみ。詳細は次回 |
| ② | HoTT の主張を「そういうものだ」と宣言して済ませると、何が起きるのか | 証明が動かなくなる理由 | 概要のみ。詳細は次回 |
| ③ | Arend と Cubical Agda は、どこで分かれたのか | 設計判断の中身と、その代償 | 本記事の中心。詳しく扱います |
上記のうち、③が本稿の中心論点 です。
重要性の観点から、まず最初に論点③から解説致します。
本記事の読み方
本記事は長いため、関心に応じた入口を示しておきます。
| 関心 | どこから読むか |
|---|---|
| Arend と Cubical Agda の設計の違いだけ知りたい | 論点③から |
| 等しさの根拠を扱えると何ができるのかを知りたい | 論点①から |
| HoTT を公理として足すと何が起きるのかを知りたい | 論点②から |
コードで確認したい方は、論点③の「３つの場面」をご覧ください。
本記事（連載２回目）と次回（３回目）で扱う概念の積み上がり
本記事から次回の記事にかけて、概念を一段ずつ積み上げていきます。
青い枠が出発点、金色の枠がこの記事と次回記事の中心、緑の枠が到達点です。
本連載シリーズ ２回目から３回目の記事にかけての議論の流れ
本稿（連載第２回目）と次回（３回目）の記事の論旨の流れを１枚の図にまとめます。
青い枠が、出発点です。 HoTT が何を扱う理論なのか、というところから始まります。
金色の枠が、３つの論点です。 ①から③へ、順に降りていきます。
赤い枠が、証明が途中で止まる場合です。 公理として足した場合と、Arend の場合の２つがあります。
緑の枠が、２つの言語の選択です。 それぞれ別のものを優先しています。
そして最下段で、両者が合流します。 どちらが正しいという話ではない、という結論です。
論点③ ── Arend と Cubical Agda は、どこで分かれたのか
両言語は、何を得て、その代償に何を失ったのか
両言語が何を優先して手に入れ、その代償として何を失ったのか。
Cubical Agda が失ったものは、理論の単純さです。
Cubical Agda は、後で説明する「証明の計算を途中で止めにくくする仕組み」を得る代わりに、理論と実装上の扱いがより複雑になります。
具体的には、Cubical Agda のコードを書く際、プログラマが考慮すべきことが増えます。
たとえば、区間変数、面条件、境界の整合性、path 型と cubical identity type の使い分けです。（難しい言葉が並びましたが、本稿で後程、丁寧に説明いたします）
また、常に起きることではなく、プログラマがどのような問題を扱うのかによって変わるのですが、Cubical Agdaは、Arendよりもコードの行数が増える場合があります。
そのような場面では、Arend では消去原理で短く書ける証明に対し、Cubical Agda では面条件や区間変数を明示する必要があり、記述量も増えてしまうのです。
プログラマにこのような負担を負わせる代わりに、Cubical Agda は、Arend よりも証明の計算を先まで進められることができます。
Arend では、証明を走らせても途中で止まる式が残ります。
Cubical Agda では、Arend で途中に残ることがある式についても、
計算を進めて、より具体的な形まで到達できる場合があります。
つまり、Cubical Agda は、プログラマに負荷をかけるという代償を引き受けた上で、証明を計算したときに「途中で式が残る」場面を少なくすることを優先する言語設計思想を採用したのです。
このことをもう少し専門的な言葉を使って表現すると、以下のようになります。
- Arend では、証明を走らせても途中で簡約が止まる式が残ることがある
- Cubical Agda は、Arend よりも豊富な計算規則を備え、一価性や高次帰納的型を含む主要な構成について、より強い計算的性質を与えられている
ここで注意すべきは、両者の差は単に「コードが短いか長いか」ではない、ということです。
- Arend は、理論をできるだけ単純に保つことを選択した。
- Cubical Agda は、理論が複雑になることを引き受ける代わりに、証明を計算したときに途中で式が残る場面を減らすことを選んだ。
その設計選択が、利用者の判断負担や記述量、そして計算の振る舞いに現れるのです。
| Arend | Cubical Agda | |
|---|---|---|
| 証明を走らせたとき | 一部の式で計算が止まる | HoTT の主要な構成を計算的に扱える |
| 理論 | 単純 | より複雑 |
| プログラマの負担 | 比較的軽い | 比較的大きい |
より厳密に言うと、次のようになります。
| 体系 | HoTT 的構成の位置づけ | 計算上の性質 |
|---|---|---|
| Rocq 上の HoTT ライブラリ／通常の Agda に公理を追加 | 公理として追加 | 公理を通る計算は、一般に定義的には簡約しない |
| Arend | 計算規則を伴う形で多くの構成を提供 | 多くの式は計算するが、正準性は持たない |
| Cubical Agda | 一価性・高次帰納的型を計算的に扱う立方体型理論 | 閉じたデータ項の正準性を支える、より強い計算的性質を目指す |
なお、本記事で 「証明を最後まで走らせる力」 と述べるときは、Arend は計算の途中で式が残ることがあるのに対し、Cubical Agda はその計算を先へ進め、途中に式が残る場面を減らせることを指します。
（より専門的な言葉を使うならば、「証明を最後まで走らせる力」と述べるときは、Arendでは計算の途中で未簡約の式が残ることがある場面の一部について、Cubical Agda では計算をさらに進められることを指す、という表現になります）
Arend と Cubical Agda の 分かれ目 は、「等しさの根拠」を表すために使う 「区間」という部品の扱い方 の 違いに起因 します。
ここで、 「区間」 という言葉が キーワード になります。
区間とは何か
両端を持つ線分だとお考えください。
記号では $I$ と書きます。
左端を $\mathsf{i0}$、右端を $\mathsf{i1}$ と呼びます。
具体例
true と false は、どちらも Bool の値です。
「true と false は等しい」という主張を、どう表すか。
区間 $I$ から Bool への写像として表します。
$$p : I \to \mathrm{Bool}$$
$$p(\mathsf{i0}) = \mathrm{true}, \qquad p(\mathsf{i1}) = \mathrm{false}$$
線分の左端が true に、右端が false に送られます。
線分の上を左から右へ移動すると、true から false へ移り変わっていく。
そういう描像を思い浮かべてください。
この写像 $p$ が「道」です。
より一般的には
値 $a$ と $b$ が、同じ型 $X$ に属しているとします。
「$a$ と $b$ は等しい」の道は、区間 $I$ から $X$ への写像です。
$$p : I \to X, \qquad p(\mathsf{i0}) = a, \qquad p(\mathsf{i1}) = b$$
行き先の型 $X$ は、$a$ と $b$ が属している型そのものです。
補足 ── 具体例で確かめる
ここは、少しわかりづらい部分がありますので、対話形式で少し丁寧に解説します。
タロウくん：
先生、いまの説明を具体例で確かめさせてください。
以下の理解で、間違いないでしょうか？
２つの文字列型の値を比較したい場合
（例えば、等しくない "Taro" と "Kawaguchi" と、等しい "Taro" と "Taro"）
-
"Taro"と"Kawaguchi"の「等しさ」（が成立している場合に成り立つ道（経路））：区間 $I$（"Taro"と"Kawaguchi"の２点を結ぶ道・経路）から文字列型への写像
-
"Taro"と"Taro"の「等しさ」（が成立している場合に成り立つ道（経路））：区間 $I$（"Taro"と"Taro"の２点を結ぶ道・経路）から文字列型への写像
２つの整数型の値を比較したい場合
（例えば、等しくない 123 と 571 と、等しい 123 と 123）
-
123と571の「等しさ」（が成立している場合に成り立つ道（経路））：区間 $I$（123と571の２点を結ぶ道・経路）から整数型への写像
-
123と123の「等しさ」（が成立している場合に成り立つ道（経路））：区間 $I$（123と123の２点を結ぶ道・経路）から整数型への写像
専任講師：
よく整理しましたね。
ただ、残念ながら、２点、誤りがあります。
同時に、正しい部分もあります。
どこが間違っていて、どこが正しいのか、いまから見ていきましょう。
誤り① ── 区間 $I$ は、比べる対象によって変わりません
タロウくんの整理では、こうなっていました。
区間 I（"Taro" と "Kawaguchi" の２点を結ぶ道・経路）
区間 I（123 と 571 の２点を結ぶ道・経路）
区間 $I$ は、何を比べるかによらず、常に同じ１つの型です。
比べる対象ごとに、別の区間が用意されるわけではありません。
Arend で確かめてみましょう。
なお、以下では説明を簡単にするため、文字列型 Str を自然数のリストとして表します。
各自然数は文字コードを表すものとします。
ASCII および Unicode の基本ラテン文字では、T = 84、a = 97、r = 114、o = 111 です。したがって、文字列 "Taro" は [84, 97, 114, 111] と表せます。
\data List (A : \Type) | nil | cons A (List A)
-- 説明用の簡略化：Str は文字コードの並びとして表す
\func Str => List Nat
-- 比べる対象の型が整数でも文字列でも、区間は同じ I
\func forNat (a b : Nat) : \Type => I
\func forStr (a b : Str) : \Type => I
-- 一方、道の型は比べる対象ごとに変わる
\func pathNat (a b : Nat) : \Type => a = b
\func pathStr (a b : Str) : \Type => a = b
型検査は通ります。
$ java -jar Arend.jar S4.ard
--- Typechecking \default ---
[ ] src.S4
--- Done (133ms) ---
タロウくん：
forNat と forStr ・・・引数の型は違うのに、返している型はどちらも I ですね。
専任講師：
そこがポイントです。
整数を比べようが、文字列を比べようが、使う区間は同じ I です。
タロウくん：
その一方で、pathNat と pathStr は・・・。
専任講師：
こちらは a = b を返しています。
a と b が整数なら整数どうしの等しさ、
文字列なら文字列どうしの等しさ。
比べる対象ごとに、別の型になります。
タロウくん：
・・・区間は同じ。道の型は違う。
区間 $I$ は、実数の閉区間ではありません
タロウくん：
先生、ここで疑問があります。
区間 は、両端点の２つの数だけを持つのではなく、両端点の ２つの数の間の数も 含みうるのですか？
例えば、いま 3 と 5 を比べようとしていて、区間の両端点が 3 と 5 になります。
すると、この区間 は、両端点の 間の点の部分 に、 3.41 とか 4.74 とか、$3\sqrt{7}$ とか、つまり 3 と 5 を端点に持つ 実数空間の閉区間（端点を含む線分）になるのですか？
専任講師：
よい質問ですね。
質問に対する答えを言うと、ここでいう区間 $I$ は、実数の閉区間ではありません。
いま 3 と 5 を比べているからといって、区間の端点が数 3 と数 5 になるわけでもありません。
区間 $I$ の両端は、常に left と right です。
$$\mathsf{left} : I, \qquad \mathsf{right} : I$$
一方、3 と 5 は、自然数型 Nat の値です。
$$3 : \mathrm{Nat}, \qquad 5 : \mathrm{Nat}$$
この２つは、別の型に属しています。
タロウくん：
・・・left と 3 は、そもそも別の型の要素なのですね。
専任講師：
そうです。ここはしっかりと理解しておくべきポイントです。
両者は、道を作るときに初めて結びつきます。
$$p : I \to \mathrm{Nat}$$
このとき、次を満たす道を作れれば、3 = 5 の根拠になります。
$$p(\mathsf{left}) = 3, \qquad p(\mathsf{right}) = 5$$
タロウくん：
では、「3 と 5 を比べるとき、区間 $I$ の両端が 3 と 5 になる」のではない。
専任講師：
そのとおりです。
常に同じ left と right を持つ区間 $I$ を使い、left を 3 へ、right を 5 へ送る写像を作れるかを問います。
ただし Nat では、そのような道は作ることはできません。
\func p : 3 = {Nat} 5 => idp
型検査は通りません。
$ java -jar Arend.jar T4.ard
[ERROR] src.T4:1:26: Expressions are not equal
Left: 3
Right: 5
In: idp
3 = 5 という型は書くことはできます。
しかし、その型の要素、すなわち 3 と 5 が等しいことの根拠は作れません。
したがって、先ほどの式は「もしそのような道が作れれば」という仮定の形です。
タロウくん：
では、区間の中間点が 3.41 や 4.74、あるいは $3\sqrt{7}$ を表しているわけではないのですね？
専任講師：
そのとおりです。
3.41、4.74、$3\sqrt{7}$ は、実数の閉区間 $[3,5]$ に属する数です。
しかし、立方体型理論の区間 $I$ は、そのような実数の集合ではありません。
$$I \neq [3,5] \subseteq \mathbb{R}$$
left と right は、道を記述するための抽象的な両端です。
3 と 5 は、その道が行き着く先の型 Nat の値です。
$$\mathsf{left} \longmapsto 3, \qquad \mathsf{right} \longmapsto 5$$
左側と右側は、別の型に属しています。
$$\mathsf{left}, \mathsf{right} : I, \qquad 3, 5 : \mathrm{Nat}$$
タロウくん：
では、「区間の途中を左から右へ動く」という説明は、何を意味するのですか？
専任講師：
実数の値を１つずつ通る、という意味ではありません。
区間変数 i : I は、道の位置を表すための抽象的な変数です。
i が left のときに始点が得られ、
i が right のときに終点が得られます。
立方体型理論では、i を用いて、道・正方形・立方体の辺や面を記述します。
そのために、区間には最小演算 ∧、最大演算 ∨、反転 ~ などの演算が備わっています。
ただし、これは i を実数として計算するためではありません。
道や面の端点・境界がどのようにつながるかを、型検査器に記述するための演算です。
タロウくん：
つまり、区間 $I$ は「数 3 から数 5 までの線分」ではない 、そういうことですね？
専任講師：
そういうことです。
区間 $I$ は、どの道でも共通に使う抽象的な区間です。
道 $p$ のほうが、left を始点の値へ、right を終点の値へ送ります。
$$p : I \to X, \qquad p(\mathsf{left}) = a, \qquad p(\mathsf{right}) = b$$
ここで変わるのは、区間 $I$ ではありません。
比較する値 $a$、$b$、行き先の型 $X$、そして写像 $p$ です。
重要
立方体型理論の区間 $I$ は、実数の閉区間ではありません。
leftとrightは、比較する値そのものではなく、道を記述するための抽象的な端点です。
比較する値 $a$、$b$ は、道 $p : I \to X$ によってleftとrightの像として指定されます。
結論から言うと、Cubical Agda における立方体型理論の区間 I は、実数の閉区間 $[3,5]$ でも、3 と 5 の間に実数を詰め込んだ集合でもありません。
left と right は 3 や 5 そのものではなく、区間の抽象的な端点 です。
Cubical Agda の公式説明では、空の文脈における閉じた I の値は、端点 i0 と i1 の２つだけです。
その一方で、文脈に区間変数 i : I を置くと、i、i ∧ j、i ∨ j、~ i のような区間式を扱えます。
なお、Arend では端点を left と right、Cubical Agda では i0 と i1 と書きます。
いずれも、比較する値そのものではなく、道を記述するための区間の端点です。
区間の型と、道の型
タロウくん：
先生、ひとつ確かめさせてください。「区間」と「道の型」は、本質的に別のものなんですか？
つまり、「道の型」は、「区間の型」と言っては間違いですか？
専任講師：
間違いです。まったく別のものです。
タロウくん：
どう別なのでしょうか？
専任講師：
Arend のコードで並べてみましょう。
-- 区間そのもの
\func intervalType : \Type => I
-- 道の型は、区間とは別のもの
\func pathType (a b : Nat) : \Type => a = b
-- 道は、区間から型への写像として作られる
\func aPath : 3 = {Nat} 3 => path (\lam i => 3)
-- 区間の両端
\func leftEnd : I => left
\func rightEnd : I => right
型検査は通ります。
$ java -jar Arend.jar S6.ard
--- Typechecking \default ---
[ ] src.S6
--- Done (100ms) ---
タロウくん：
intervalType が I を返して、pathType が a = b を返していますね。
専任講師：
この２つは、別々の型です。
I には left と right という両端があります。
3 = 3 の要素は、道そのものです。
タロウくん：
・・・住んでいるものが違う。
専任講師：
では、どういう関係にあるのか、そのことを理解する必要があります。
aPath の定義をみてください。
\func aPath : 3 = {Nat} 3 => path (\lam i => 3)
\lam i とは何か
タロウくん：
先生、この \lam i というのは何ですか。
専任講師：
無名関数を作る記法です。
Haskell の \x -> ... にあたります。
タロウくん：
ラムダ式ですね。
専任講師：
そのとおりです。lam は、lambda を省略したものです。まず、普通の例をお見せします。
-- \lam は無名関数を作る記法
\func addOne : Nat -> Nat => \lam n => n Nat.+ 1
\func check : addOne 3 = 4 => idp
型検査は通ります。
\lam n => n Nat.+ 1 は、「n を受け取って n + 1 を返す関数」です。
タロウくん：
Haskell なら \n -> n + 1 ですね。
専任講師：
同じものです。
では、道の定義に戻りましょう。
\func aPath : 3 = {Nat} 3 => path (\lam i => 3)
\lam i => 3 は、「区間の値 i を受け取って、3 を返す関数」です。
タロウくん：
・・・i を受け取っているのに、i を使っていませんね。
専任講師：
そうです。定数関数だからです。
区間のどの位置にいても、常に 3 を返します。
タロウくん：
なぜ、定数でよいのですか？
専任講師：
3 = 3 の道を作りたいからです。
左端でも 3、右端でも 3。
両端が同じ値なので、途中も動かなくてよいのです。
タロウくん：
なるほど。では 3 = 5 の道を作りたい場合は。
専任講師：
Nat では作ることはできません。
3 = 5 という型は宣言できます。
しかし idp は、両端が計算して同じ形になるときにだけ使えます。
Nat は集合として振る舞う型なので、3 と 5 のように異なる標準形どうしを結ぶ等しさの根拠は作ることができないのです。
タロウくん：
・・・Nat では、道が引けない。
専任講師：
そこは、注意して覚えてください。
ただし、これは、すべての型について成り立つ一般則ではありません。
タロウくん：
えっ？どういうことですか？
専任講師：
商型や高次帰納的型では、見かけ上は異なる２つの値のあいだに、同一視を与える道を型の定義として追加できます。
次回の記事で扱う商型が、まさにその例です。
q a b と q (a * k) (b * k) は見かけが違いますが、same という道で結ばれます。
タロウくん：
・・・「等しくなさそうに見える２つの項には常に道がない」わけではない。
専任講師：
そのとおりです。
ここでの結論は、Nat のような集合として振る舞う型では、異なる標準的な数のあいだに道は存在しない、ということです。
path とは何か
タロウくん：
道の定義として示されていた以下のコードに戻らせてください。
\func aPath : 3 = {Nat} 3 => path (\lam i => 3)
このpath とは、なんでしょうか？
専任講師：
区間からの写像を、道に変換する操作 です。
\lam i => 3 -- これは、区間から Nat への写像
path (\lam i => 3) -- これを道にしたもの。型は 3 = 3
タロウくん：
・・・写像を包んで、道の型にしている！
専任講師：
そういう関係です。逆向きの操作もあります。
-- 左端と右端で値を取り出す
\func atLeft : Nat => aPath @ left
\func atRight : Nat => aPath @ right
\func c1 : atLeft = 3 => idp
\func c2 : atRight = 3 => idp
型検査は通ります。
@ が、道の指定した位置における値を取り出す操作です。
タロウくん：
aPath @ left で左端の値、
aPath @ right で右端の値。
専任講師：
そして、どちらも 3 になりました。
c1 と c2 が idp で示せたということは、処理系が実際に計算して 3 に到達したということです。
タロウくん：
・・・path で作って、@ で取り出す。
専任講師：
この２つが対になっています。
道に付ける名前は、自由に決められます
タロウくん：
先生、今回示していただいたコードでは、aPath という名前を与えていますが、
ここはプログラマが任意の名前を道に与えることはできますか？
例えば、studentNamePath とか、mathematicsExaminationResultScorePath とか。
専任講師：
できます。実際に書いてみましょう。
\data List (A : \Type) | nil | cons A (List A)
-- 説明用の簡略化：
-- Str は文字コードの並びとして表す
-- "Taro" = [84, 97, 114, 111]
\func Str => List Nat
\func taro : Str => cons 84 (cons 97 (cons 114 (cons 111 nil)))
-- 道の名前は、プログラマが自由に付けられる
\func studentNamePath : taro = {Str} taro => path (\lam i => taro)
\func mathematicsExaminationResultScorePath : 87 = {Nat} 87 => path (\lam i => 87)
-- 付けた名前で、あとから参照できる
\func check1 : studentNamePath @ left = taro => idp
\func check2 : mathematicsExaminationResultScorePath @ right = 87 => idp
型検査は通ります。
$ java -jar Arend.jar T2.ard
--- Typechecking \default ---
[ ] src.T2
--- Done (137ms) ---
タロウくん：
・・・普通の関数と同じように、名前を付けられるのですね。
専任講師：
そのとおりです。\func で名前を付けた普通の定義として扱えます。
タロウくん：
aPath という名前に、特別な意味はなかった。
専任講師：
ありません。私が説明のために付けただけです。
慣習 として、道を表すものには Path という語尾を付けることが多いです。
しかし、規則ではありません。
タロウくん：
studentNamePath は、文字列 "Taro" がそれ自身と等しいことの根拠。
専任講師：
そして mathematicsExaminationResultScorePath は、数学の試験の点数 87 が 87 と等しいことの根拠です。
タロウくん：
・・・何についての等しさなのかを、名前で表すことができる！
専任講師：
実際の開発では、そこが重要になります。
証明の中に道がいくつも現れるとき、名前が付いていなければ何の根拠なのか分からなくなるからです。
区間と道の関係
タロウくん：
整理すると、i は区間の値で、それを使って道を作る。
専任講師：
そうです。
整理すると、こうなります。
| 何であるか | 注目するもの | |
|---|---|---|
区間 I |
道を記述するための抽象的な区間 | 両端 left と right、および区間変数 i
|
道の型 a = b |
$a$ と $b$ の等しさの根拠を集めた型 | その要素は、端点が $a$、$b$ となる道 |
タロウくん：
理解できてきました。
結局、「道の型」を「区間の型」と呼ぶのは・・・。
専任講師：
入力と出力を取り違えることになります。
Haskell でいえば、Int -> String という関数の型を「Int の型」と呼ぶようなものです。
タロウくん：
・・・確かに、それはおかしいですね。
専任講師：
ここは大事なところなので、頭の中を整理しましょう。
| 何が変わるか | |
|---|---|
| 区間 $I$ | 変わらない。常に同じ区間 |
| 道 $p$ | 比べる対象ごとに変わる |
| 行き先 $X$ | 比べる対象が属する型 |
| 具体的には、こうなります。 | |
| 比べるもの | 行き先の型 $X$ |
| --- | --- |
"Taro" と "Taro"
|
文字列型 Str
|
123 と 123
|
整数型 Nat
|
誤り② ── Nat の異なる数どうしには、道を作れません
タロウくんの最初の質問には、こういう項目がありました。
"Taro" と "Kawaguchi" の「等しさ」：区間 I から文字列型への写像
123 と 571 の「等しさ」：区間 I から整数型への写像
今回扱っている Nat や、文字コードのリストとして表した文字列では、これらの写像は存在しません。
Arend で確かめてみましょう。
-- 等しい場合：道が存在する
\func p1 : 123 = {Nat} 123 => idp
-- 等しくない場合：道は存在しない
\func p2 : 123 = {Nat} 571 => idp
最後の一行で、型検査が通りません。
$ java -jar Arend.jar S1.ard
[ERROR] src.S1:5:31: Expressions are not equal
Left: 123
Right: 571
In: idp
タロウくん：
・・・123 = 571 という式は、書けているのですね。
専任講師：
書けます。型としては存在します。
しかし、その型の要素が存在しません。
タロウくん：
型はあるけれど、中身がない。
専任講師：
そういうことです。
123 と 571 は異なる自然数です。
そのため、123 = 571 という型は書けますが、その要素、すなわち等しさの根拠を作ることはできません。
ただし、これはすべての型について成り立つ一般則ではありません。
たとえば商型や高次帰納的型では、見かけ上は異なる２つの値のあいだに、同一視を与える道を型の定義として追加できます。
| 比べるもの | 道は存在するか |
|---|---|
"Taro" と "Taro"
|
存在する |
"Taro" と "Kawaguchi"
|
存在しない |
123 と 123
|
存在する |
123 と 571
|
存在しない |
この表は、Nat と、文字コードのリストとして表した文字列についてのものです。 |
タロウくん：
先生、いま見てきたことを振り返ると、123 = 571 という型は書けますが、その要素、すなわち等しさの根拠を作ることはできませんでした。
つまり、型はあるけれど、中身がありませんでした。
カリー＝ハワード同型対応では、定理証明支援言語における「型」が、検証して、証明（または反証すべき）すべき論理命題（証明式）であり、その「型」のインスタンス（具体的な値）を見つける（構成する）ことができた場合は、その論理命題（証明式）は成立している正しいものとして、証明される。
でも、その「型」のインスタンス（具体的な値）を構成できなかった場合は、その論理命題（証明式）は成立していない、つまり、反証されるのでしたね？
今回のケースでは、『"Taro" と "Kawaguchi" は等しい』という論理命題と、『123 と 571 は等しい』という論理命題は、どちらも、成立していない、つまり、正しくないものであることが証明された（反証された）、という理解であっていますね？
専任講師：
前半は正しいのですが、後半に誤りがあります。
タロウくん：
えっ？後半は間違っていましたか？
専任講師：
「インスタンスを構成できなかった」ことと、「反証された」ことは、別のことです。
タロウくん：
・・・また、同じ形の誤りをしてしまいましたか。
専任講師：
残念ですが、そのようですね。先ほどの idp の話と、同じ構造です。
idp が通らないことは「等しくない」の証明ではありませんでした。
同じように、インスタンスを構成できないことは「反証」ではありません。
タロウくん：
では、反証するにはどうするのですか？
専任講師：
「その命題が成り立つと矛盾する」ことを示す関数を、実際に構成する必要があります。
$$\neg P ;\equiv; P \to \bot$$
「$P$ を仮定すると矛盾が導ける」という関数を、実際に書くのです。
タロウくん：
・・・「作れなかった」ではなく、「矛盾を導く関数を作った」。
専任講師：
そこが違いです。実際にやってみましょう。
\data Empty
\data Unit | unit
\func Not (A : \Type) => A -> Empty
-- 3 と 5 を区別する述語
\func diff (n : Nat) : \Type
| 3 => Unit
| _ => Empty
-- 3 = 5 の否定を構成する
\func ne : Not (3 = {Nat} 5) => \lam p => coe (\lam i => diff (p @ i)) unit right
型検査は通ります。
$ java -jar Arend.jar U3.ard
--- Typechecking \default ---
[ ] src.U3
--- Done (127ms) ---
タロウくん：
Empty というのは。
専任講師：
定義をご覧ください。
\data Empty
構成子が１つも書かれていません。
タロウくん：
・・・Haskell の data でいえば、| の右に何もない。
専任講師：
そのとおりです。要素を作る手段が、存在しません。
Bool なら true と false を書きます。Unit なら unit を書きます。
Empty には、それがありません。
タロウくん：
だから、要素を持たない。
専任講師：
論理でいえば、偽にあたります。
「証明が存在しない命題」です。
タロウくん：
そして Not A は A -> Empty ・・・。
専任講師：
「A の証明を渡されたら、偽の証明を返す関数」です。
そんな関数が書けるということは、A の証明があると矛盾する、ということです。
タロウくん：
diff は、何をしているのですか。
専任講師：
3 のときだけ Unit、それ以外は Empty を返す述語です。
実際に確かめられます。
\func c1 : diff 3 = Unit => idp
\func c2 : diff 5 = Empty => idp
型検査は通ります。
タロウくん：
そして coe というのは。
専任講師：
道に沿って、値を運ぶ操作です。
型 $X$ と型 $Y$ が等しいと示せたとき、$X$ の値を $Y$ へ持っていく。
この操作を、移送（transport）と呼びます。
タロウくん：
・・・その coe を、ここで使っている。
専任講師：
では、順を追いましょう。
まず、3 = 5 の道 p があると仮定します。
タロウくん：
はい。
専任講師：
この p は、3 から 5 へ至る道です。
そして diff を通せば、diff 3 から diff 5 へ至る道が得られます。
タロウくん：
diff 3 は Unit、diff 5 は Empty でした。
専任講師：
つまり、Unit から Empty への道です。
タロウくん：
・・・２つの型が、等しいことになってしまう。
専任講師：
そして、道があれば coe で値を運べます。
出発点に unit を置きます。Unit の要素です。
タロウくん：
それを運ぶと。
専任講師：
到着点で、Empty の要素が得られます。
タロウくん：
・・・あっ。
専任講師：
気づかれましたか。
タロウくん：
Empty には、要素を作る手段がないはずでした。
構成子が１つも書かれていないのですから。
専任講師：
そのとおりです。
要素を持たないはずの型に、要素が現れた。これが矛盾です。
タロウくん：
・・・仮定した 3 = 5 の道が、おかしかった。
専任講師：
だから、そんな道は存在しないと結論できます。
これが反証です。
タロウくん：
型検査が通らなかったこととは、まったく別の作業 なのですね！
専任講師：
そのとおりです。
「証明できなかった」は、まだ何も分かっていない状態です。
「反証した」は、存在しないことを積極的に示した状態です。
タロウくん：
・・・今回、私たちは前者しかやっていなかった。
専任講師：
そこを区別しておいてください。
正しかった部分
タロウくん：
では、私の整理で正しかったのは、どこですか？
専任講師：
行き先の型を、正しく捉えていました。
文字列どうしを比べるなら文字列型へ。
整数どうしを比べるなら整数型へ。
タロウくん：
比べる値が属している型が、そのまま行き先になる。
専任講師：
そこは、そのとおりです。
さらに、「等しさが成立している場合に成り立つ道」という言い方も、方向としては正しいものでした。
今回扱っている Nat のような型では、等しければ道があり、異なる標準形の値のあいだには道がありません。
その対応を捉えていたからです。
タロウくん：
・・・区間そのものが道だと思い込んでいたところが、間違いだった のですね。
専任講師：
区間は、道を描くための入力側です。
そして 道は、区間から型への写像 であって、両端が比べる２つの値になるもの。
この２つを分けて捉えてください。
証明を最後まで走らせるには、２つの操作が要ります
１つは、道に沿って値を運ぶ操作です。
Agda では transp と書きます。
型 $X$ と型 $Y$ が等しいと示せたとき、$X$ の値を $Y$ へ持っていく。
この操作がなければ、証明を書いても何も起きません。
もう１つは、描きかけの道の隙間を埋める操作です。
Agda では hcomp と書きます。
道が途中までしか引けていないとき、残りを補う。
この操作がなければ、複雑な証明が途中で行き止まりになります。
この２つが、どんな型についても定義されていれば、証明は途中で止まりません。
立方体型理論では、通常の型について２つの操作が使えるよう設計されています
ここが、２つの言語の分かれ目を理解する鍵になります。
まず、立方体型理論という語を説明します。
等しさを「道」として扱う型理論の総称です。
道と道のあいだの関係を、正方形や立方体の形に載せて計算することから、この名が付きました。
まず、立方体型理論という語を説明します。
等しさを「道」として扱う型理論の総称です。
道と道のあいだの関係を、正方形や立方体の形に載せて計算することから、この名が付きました。
２点の間の道は、２点をつなぐ線分（経路、道、等しさの根拠）。
p
a ─────────── b
← １次元（線分）
２点の間の道は、２点をつなぐ線分（経路、道、等しさの根拠）が２本ある場合、その道と道をつなぐ、新しい（より抽象度、メタレベルの高い）道を引ける。線を引くと、図の次元も１次元（横方向に伸びる道だけ）から２次元（横方向に加えて、縦方向に伸びる道が追加される）になる。
p
a -------------- b
| |
idp | α | idp ← 左辺・右辺は、その場に留まる道
| |
a -------------- b
q
← ２次元（正方形）。α が、道 p と道 q をつなぐ
さらに、さきほどの新しい（より抽象度、メタレベルの高い）道が２本あった場合、その２つの道を結ぶ新しい（より抽象度、メタレベルの高い）道を引ける。図の次元は３次元になる。
手前の面 奥の面
p p
a --------- b a --------- b
| α | | β |
a --------- b a --------- b
q q
↓ θ が、面 α と面 β をつなぐ
← ３次元（立方体）。２枚の正方形を、奥行き方向に結ぶ
この２枚を奥行き方向に重ねると、立方体になります。
p
a ─────────── b
╱│ ╱│
╱ │ ╱ │
╱ │ β ╱ │ ← 奥の面が β
╱ │ ╱ │
a ─────────── b │
│ a ───────┼─── b
│ ╱ q │ ╱
idp │ ╱ │ ╱ idp
│ ╱ α │ ╱ ← 手前の面が α
│╱ │╱
a ─────────── b
q
θ は、この立方体の内部にあたる。
手前の面 α と、奥の面 β を結ぶ。
この立方体では、８つの頂点がすべて a または b です。
左側の４頂点が a、右側の４頂点が b になります。
そして、辺は次のように対応します。
| 辺の向き | 何を表すか |
|---|---|
| 横方向 | 道 p と道 q
|
| 縦方向 |
idp（その場に留まる道） |
| 奥行き方向 |
idp（その場に留まる道） |
面と内部は、こう対応します。
| 何を表すか | |
|---|---|
| 手前の面 |
α（p と q をつなぐ道） |
| 奥の面 |
β（p と q をつなぐ、もう１つの道） |
| 立方体の内部 |
θ（α と β をつなぐ道） |
階層の対応
実機で確認した対応です。
\data Bool | true | false
-- １次元：a から b への道
\func p1 : true = {Bool} true => idp
\func p2 : true = {Bool} true => idp
-- ２次元：道と道のあいだの道
\func alpha : p1 = p2 => idp
\func beta : p1 = p2 => idp
-- ３次元：面と面のあいだの道
\func theta : alpha = beta => idp
型検査は通ります。
$ java -jar Arend.jar X1.ard
--- Typechecking \default ---
[ ] src.X1
--- Done (128ms) ---
| 次元 | 何をつなぐか | 型の例 |
|---|---|---|
| １ | 点と点 | p1 : true = true |
| ２ | 道と道 | alpha : p1 = p2 |
| ３ | 面と面 | theta : alpha = beta |
この階層は、どこまでも続きます。
Arend も Cubical Agda も、この立方体型理論の一種を実装しています。
そして立方体型理論では、通常の型について、道に沿って値を運ぶ操作（transp）と、描きかけの道の隙間を埋める操作（hcomp）の２つが利用できるように設計されています。
Nat も Bool も、組の型も関数の型も、すべて対象に含まれます。
だからこそ、「どんな型についても２つの操作が使える」と言えるのです。
しかし、区間 $I$ は、通常の型とは異なる立場に置かれています。
区間の上には、欠けた部分を埋める操作を定義できないからです。
理由について、詳細はこの記事の第7部で解説させて頂きますが、ここでは先取して、概略だけ述べさせていただきます。
理由は、２つあります。
第１に、型検査の問題があります。
区間 を 通常の型 として扱うと、たとえば
$f : \mathbb{N} \to \mathbb{I}$
のような関数が書けてしまいます。
そうした自由を許すと、型検査が有限時間で終わる保証を失いかねません。
第２に、区間には、通常の型に必要な構造を定義できないからです。
ここで比較している Cubical Agda では、区間 $I$ は通常の Type の要素ではありません。
立方体型理論では、区間を通常の型とは別のものとして導入します。
型の仲間ではなく、道を書くための部品として、最初から分けて扱われるのです。
なぜ、この違いが２つの操作の有無につながるのか。
通常の型には、作り方ごとに決まった規則があるからです。
$A \times B$ は、型 $A$ と型 $B$ から作ります。$A \to B$ も同じです。List A も、型 $A$ から作ります。
そして、作り方ごとに、２つの操作の規則を与えられます。
組の型なら、成分ごとに値を運ぶ。関数の型なら、引数と返り値について規則を与える。作り方が決まっているから、操作の規則も決められるのです。
一方、区間は、そのような型構成子から作られた通常の型ではありません。
他の型から作られたのではなく、立方体型理論の土台として最初から置かれる部品です。
そのため、「型の作り方に沿って操作を定義する」という手が使えません。
では、直接定義すればよいのでしょうか。
試みると、うまくいきません。
区間には、端点を入れ替える ~ i のような区間式はあります。
しかし、通常の型に対して必要な意味で、どの欠けた面についても残りを埋める操作を、区間そのものに与えることはできません。
つまり、区間には Kan 型として必要な「隙間を埋める構造」を定義できないのです。
「Kan」とは何か
人名です。 代数トポロジーの数学者、Daniel M. Kan に由来します。
もとは、図形についての条件でした。
三角形を思い浮かべてください。３辺のうち、２辺だけが描かれている状態があるとします。
残りの１辺を、必ず補えるか。
補えるなら、その図形は Kan 条件を満たします。欠けた部分を、いつでも埋められるということです。
立方体型理論では、この条件が２つの操作として現れます。
道が途中までしか引けていないとき、残りを補う。それが、欠けた部分を埋める操作にあたります。
そして、通常の型はこの条件を満たすように設計されています。
区間だけが、その例外なのです。
なお、Kan 条件の厳密な内容と、２つの操作との対応関係については、本連載の次回であらためて扱います。
この２つの理由について、一次資料を引きながら詳しく扱うのも、次回の記事です。
Arend は、区間を普通の型として扱いました
$I$ は、Nat や Bool と同じ場所に置かれています。
しかし、条件を満たさないものを、同じ場所に置いたということです。
その結果、こうなります。
Nat、Bool、組の型、関数の型 |
区間 $I$ | |
|---|---|---|
| 同じ場所にあるか | ある | ある |
| ２つの操作を持つか | 持つ | 持たない |
「この場所にあるものについては、すべて２つの操作を利用できる」とは、言えません。
区間だけが、条件を満たさないまま同居しているからです。
そして、条件を満たさないものが混じっていると、そこに行き当たった計算が止まります。
「どんな型でも値を運べる」という前提で書かれた式が、区間に出会ったところで進めなくなるのです。
これが、この記事で説明している「Arend で証明が途中で止まる」現象の背景です。
理論は単純に保たれます。 置き場所をひとつに保てるからです。
Cubical Agda は、区間を型の外に置きました
「型の外」とは、こういうことです。
Agda では、通常の型は Type という場所に集められています。
$$\mathrm{Nat} : \mathrm{Type}, \qquad \mathrm{Bool} : \mathrm{Type}$$
区間 $I$ だけは、通常の Type とは区別し、特別なソートに置きます。
$$I : \mathrm{IUniv}$$
IUniv は、区間 $I$ を通常の型とは別に置くための特別なソートです。
ソートとは、簡単にいえば「型や型に似たものが、どの階層に属しているかを表す分類」です。
普通の値が Nat や Bool という型に属するように、型そのものも「どこに属するのか」を持っています。 Nat は Type のような宇宙に属します。
普通の値 → 型 → 宇宙
↑
通常の階層
区間 I → IUniv
↑
特別なソート
ここでいう「別の場所」とは、単にプログラム上の別の名前空間という意味ではありません。
型理論の規則によって、通常の型とは異なる扱いを受ける場所という意味 です。
（原文引用）
The key idea of Cubical Type Theory is to add an interval type
I : IUniv(the reason this is in a special sortIUnivis because it doesn't support thetranspandhcompoperations).
（筆者による日本語訳）
立方体型理論の要となる発想は、区間型
I : IUnivを加えることである。これが特別なソートIUnivに置かれている理由は、transpとhcompの操作をサポートしないためである。
出典：
Cubical, Agda Documentation
引用文が、まさにその判断を述べています。
区間は２つの操作をサポートしない。
だから、通常の型とは別の場所に置いた。
その結果、こうなります。
Type にあるもの |
IUniv にある区間 $I$ |
|
|---|---|---|
| ２つの操作を持つか | すべて持つ | 持たない |
「Type にある通常の型については、２つの操作を利用できるように設計されている」と、例外なく言えます。
区間はそこにいないので、そもそも例外になりようがありません。
条件を満たさないものが混じっていないので、計算が止まりません。
そのぶん、理論が複雑になります
型の置き場所が、Type と IUniv の２つに増えました。
そして、その２つを行き来する規則が必要になります。
より厳密に言うと、こうなります。
通常の型の宇宙 と 区間用のソート を 区別する ため、区間変数を含む式、面条件、型構成子の適用可能性について、通常の型だけを前提にした体系より多くの整合条件が必要になります。
ここで、「面条件」 という言葉が出てきました。
道と道のあいだの関係を示すとき、正方形や立方体の形が現れます。
その各辺、各面が、どういう値で埋まっているかを指定するもの が面条件です。
具体例は、このあとの場面２でお見せします。
タロウくん：
先生、具体的には、Cubical Agda のプログラマは、Arend では必要ない、どんな整合条件の確認作業が必要になるのですか？
具体的な場面を、いくつか挙げて教えてください。
そして、その結果、コーディングすべき記述も増えるのかどうか も知りたいです。
取り上げた場面ごとに教えてください。
専任講師：
分かりました。
３つの場面を見ていきます
Cubical Agda が引き受けた理論の複雑さは、プログラマの負担として現れます。
しかし、その代わりに、計算を（後述する比較対象に比べて）より先まで進めることができるというメリットも享受します。
タロウくん：
比較対象は何ですか？
専任講師：
２つあります。
比較対象１ ── Rocq の HoTT ライブラリ
HoTT を公理としてだけ受け取る方式です。
HoTT を検証すべき定理として扱わないため、HoTT の計算規則そのものを備えていません。
タロウくん：
「公理として受け取る」というのは、具体的にどういうことですか。
専任講師：
HoTT の中心にある主張を、証明せずに「正しいものとする」と宣言することです。
HoTT の中心にある主張とは、「一対一に対応し、構造を保つ対応がある２つの型は、等しいものとして扱ってよい」というものです。
タロウくん：
「同じ構造を持つ２つの型」というのが、まだ分かりません。具体例を挙げていただけますか。
専任講師：
４つ挙げましょう。
第１に、名前だけが違う型です
data Bool = True | False
data Answer = Yes | No
構成子の名前が違うだけで、True と Yes、False と No が一対一に対応します。
第２に、数の表し方が違う型です
片方は、0 から始めて「１を足す」を必要な回数だけ重ねる方法です。
0 → 0
1 → 0 に「１を足す」を１回
2 → 0 に「１を足す」を２回
3 → 0 に「１を足す」を３回
もう片方は、0 と 1 の並びで表す方法です。
0 → 0
1 → 1
2 → 10
3 → 11
4 → 100
後者は、いわゆる二進数です。
タロウくん：
前者は、3 を表すのに「１を足す」を３回。1000 なら1000回ですか。
専任講師：
そうなります。
一方、二進数で 1000 を表すと 1111101000 となり、10桁で表せます。
「１を足す」を1000回重ねるのと、10個の記号を並べるのと。 同じ数を表すのに、必要な量がまったく違います。
タロウくん：
・・・100分の１ですね。
専任講師：
表し方はまったく違いますが、表している数は同じです。
1000 を表す方法が２通りある、というだけのことなのです。
第３に、要素が２つの群です
２つの群を並べます。
| 要素 | 演算 | |
|---|---|---|
| 群Ａ | $0$ と $1$ | 足し算 |
| 群Ｂ | $1$ と $-1$ | 掛け算 |
要素も演算も違いますが、構造が同じです。
まず、群Ａから見ます。
タロウくん：
0 と 1 しかないのに、足し算ができるのですか。1 + 1 は 2 になってしまいます。
専任講師：
2 は、この世界には存在しません。
要素は 0 と 1 の２つだけです。そこで、2 になったら 0 に戻す、という決まりにします。
タロウくん：
・・・その決まりは、勝手に決めてよいのですか。
専任講師：
実は、決める余地がありません。
タロウくん：
といいますと。
専任講師：
群には、満たすべき決まりがあります。そのうちの１つが「逆元の存在」です。
タロウくん：
逆元、ですか。
専任講師：
「足すと単位元になる相手」のことです。
群Ａの単位元は $0$ です。何に足しても、相手を変えないからです。
$$0 + 0 = 0, \qquad 0 + 1 = 1$$
タロウくん：
・・・足しても何も起きない要素。
専任講師：
そして群の決まりでは、どの要素にも逆元がなければなりません。
$1$ の逆元は何でしょうか。
タロウくん：
$1$ に足して $0$ になる相手・・・。
専任講師：
候補は $0$ か $1$ の２つだけです。
$$1 + 0 = 1$$
これは $0$ になりません。 したがって、$0$ は $1$ の逆元ではありません。
タロウくん：
・・・残るのは $1$ だけですね。
専任講師：
そのとおりです。$1$ の逆元は、$1$ 自身になります。
つまり、
$$1 + 1 = 0$$
これ以外にありえません。
タロウくん：
決まりを追加したのではなく、そうならざるをえなかった。
専任講師：
そういうことです。
タロウくん：
時計のようですね。
専任講師：
発想は同じです。 時計は 12 の次が 1 に戻ります。
こちらは、2 になったら 0 に戻ります。
$$0 + 0 = 0, \qquad 0 + 1 = 1, \qquad 1 + 0 = 1, \qquad \mathbf{1 + 1 = 0}$$
タロウくん：
偶数と奇数の話に似ていますね。
専任講師：
まさにそれです。
0 を偶数、1 を奇数と読んでください。奇数と奇数を足すと、偶数になります。
$$3 + 5 = 8$$
奇数＋奇数＝偶数。 つまり $1 + 1 = 0$ です。
タロウくん：
先生、0 と 1 しかない世界というと、体の話でも似たものを見た気がします。
専任講師：
２元体のことですね。
${0, 1}$ に、足し算と掛け算の両方を入れたものです。
そして、その足し算の部分だけを取り出すと、群Ａになります。
| 演算の数 | 名称 | |
|---|---|---|
| 群Ａ | 足し算のみ | 群 |
| ２元体 | 足し算と掛け算 | 体 |
足し算の表は、まったく同じです。 $1 + 1 = 0$ になります。
タロウくん：
・・・同じものを、別の角度から見ていた。
専任講師：
本記事で扱うのは、足し算だけの群Ａです。
次に、群Ｂを見ます。
要素は 1 と -1 の２つ。演算は掛け算です。
$$1 \times 1 = 1, \qquad 1 \times (-1) = -1, \qquad (-1) \times 1 = -1, \qquad \mathbf{(-1) \times (-1) = 1}$$
マイナスとマイナスを掛けると、プラスになります。
タロウくん：
・・・こちらも、２つの中で閉じていますね。
専任講師：
では、群Ａと群Ｂを対応させてみましょう。
$$0 \leftrightarrow 1, \qquad 1 \leftrightarrow -1$$
すべての計算が、ぴたりと重なります。
| 群Ａ（足し算） | 群Ｂ（掛け算） |
|---|---|
| $0 + 0 = 0$ | $1 \times 1 = 1$ |
| $0 + 1 = 1$ | $1 \times (-1) = -1$ |
| $1 + 0 = 1$ | $(-1) \times 1 = -1$ |
| $1 + 1 = 0$ | $(-1) \times (-1) = 1$ |
「偶数と奇数」と「プラスとマイナス」。 見た目はまったく違いますが、振る舞いが同じです。
第４に、平面上の矢印と、２つの実数の組です
原点から出る矢印を $(x, y)$ で表せば、そのまま対応します。
矢印どうしの足し算は成分ごとの足し算になり、矢印を２倍にすることは成分を２倍にすることになります。
４つに共通すること
タロウくん：
・・・どれも、一対一に対応していますね。
専任講師：
そして、その対応が構造を保っています。
| 例 | 保たれる構造 |
|---|---|
Bool と Answer
|
要素の対応 |
| 単進数と二進数 | 数としての値 |
| 群Ａと群Ｂ | 演算の結果 |
| 平面の矢印と数の組 | 足し算と定数倍 |
この状況を「同じ構造を持つ」といいます。
タロウくん：
・・・当たり前のことのようですが。
専任講師：
当たり前に思えるからこそ、証明が難しいのです。
「同じ構造を持つなら、等しいものとして扱ってよい」。この主張には名前が付いています。一価性公理（univalence axiom）といいます。
なお、群やベクトル空間のように構造が載ったものについては、一価性公理から導かれる別の原理が働きます。 そちらは本連載の後の回で扱います。
タロウくん：
一価性公理を、証明せずに認めてしまう。
専任講師：
Rocq の HoTT ライブラリでは、そうします。
「一価性公理は正しいものとする」と宣言し、その上に議論を積み上げていく。証明そのものは記述できるのですが、走らせたところで計算は進みません。
タロウくん：
なぜ、進まないのですか。
専任講師：
「正しいものとする」としか書いていないからです。
正しいと宣言しただけで、一価性公理を使った式をどう計算するかは、何も定めていません。
タロウくん：
・・・計算の手順がないから、そこで止まる。
専任講師：
そういうことです。
比較対象２ ── Arend
HoTT を検証すべき定理として扱う方式です。
そのため、HoTT の計算規則を備えています。
タロウくん：
「HoTT の計算規則」って、具体的にはどういうものですか？
Arend と Cubical Agda それぞれで、「HoTT の計算規則」はどう定義（コーディング）されていますか？
専任講師：
「等しいという根拠を使って、値を実際に動かす規則」です。
Arend で見てみましょう。
\data Bool | true | false
-- 何も変えない関数
\func boolId (b : Bool) : Bool => b
\func boolIdId (b : Bool) : boolId (boolId b) = b => idp
-- true と false を入れ替える関数
\func boolNeg (b : Bool) : Bool \elim b
| true => false
| false => true
\func boolNegNeg (b : Bool) : boolNeg (boolNeg b) = b \elim b
| true => idp
| false => idp
-- 「Bool と Bool は等しい」という根拠を、２通り作る
\func idPath : Bool = Bool => path (iso boolId boolId boolIdId boolIdId)
\func negPath : Bool = Bool => path (iso boolNeg boolNeg boolNegNeg boolNegNeg)
-- それぞれの根拠に沿って true を運ぶ
\func movedId : Bool => coe (\lam i => idPath @ i) true right
\func movedNeg : Bool => coe (\lam i => negPath @ i) true right
-- 運んだ結果を確かめる
\func check1 : movedId = true => idp
\func check2 : movedNeg = false => idp
記号を説明します。
| 記号 | 意味 |
|---|---|
\data |
データ型を定義する。Haskell の data
|
\func |
関数や値を定義する |
=> |
定義の本体を書き始める。Haskell の =
|
\elim b |
引数 b について場合分けする。Haskell の case b of
|
| |
場合分けの各行を区切る |
iso |
２つの型が一対一に対応することから、等しさの根拠を作る |
path |
区間からの写像を、等しさの根拠に変換する |
coe |
等しさの根拠に沿って、値を運ぶ |
idp |
両辺が計算して同じ形になることを示す証拠 |
タロウくん：
boolId と boolNeg という名前は、先生が付けたのですか。
専任講師：
そうです。関数の名前は、プログラマが自由に決められます。
flip でも invert でも、動くコードとしては何ら変わりません。
タロウくん：
neg のほうが短くて済みそうですが。
専任講師：
そこは、あえて避けました。
Arend には、neg という組み込みの関数があるからです。 整数の符号を反転するものです。
\func t : Int => neg 3
\func t2 : neg 3 = -3 => idp
型検査を通過します。 neg 3 が -3 になっています。
タロウくん：
・・・同じ名前を使うと、どうなりますか。
専任講師：
自分で定義したほうが優先され、組み込みのほうが隠れます。
neg という名前で Bool 用の関数を定義すると、こうなります。
\func neg (b : Bool) : Bool \elim b
| true => false
| false => true
\func t : Int => neg 3
最後の行で、型検査が通りません。
[ERROR] Type mismatch
Expected type: Bool
Actual type: Nat
In: 3
私が定義した neg が Bool を期待しているため、整数の 3 を渡せなくなったのです。
タロウくん：
・・・組み込みのほうが、使えなくなってしまう。
専任講師：
だから boolNeg という名前にしました。
Bool 用の否定である、という意味です。組み込みの neg とは、名前の上でも区別できます。
タロウくん：
neg は negative の略ですか。
専任講師：
組み込みのほうは、負の数を作る関数ですから、そう読めます。
ただし、Arend の公式マニュアルには略語の元が書かれていません。
私が定義した boolNeg のほうは、negation（否定）のつもりで名付けました。 true と false を入れ替えるので、論理の否定にあたります。
iso、coe、idp について
タロウくん：
先生、iso、coe、idp という名前も、何かの略ですか。
専任講師：
Arend の公式マニュアルには、略語の元が書かれていません。
一般には isomorphism、coercion、identity path の略と理解されていますが、筆者が調べた範囲では、公式の記述を確認できませんでした。
代わりに、公式マニュアルがそれぞれをどう説明しているかをお見せします。
idp について。
（原文引用）
The constructor idp is not a correct definition since it is not allowed to use lambdas in constructors. This constructor can be used to replace the J operator with pattern matching.
（筆者による日本語訳）
構成子
idpは、正しい定義ではない。構成子のなかでラムダを使うことが許されていないからである。この構成子は、J演算子をパターン照合で置き換えるために使える。
出典：Prelude — Arend Theorem Prover
タロウくん：
「正しい定義ではない」・・・？
専任講師：
Prelude に置かれた定義は、通常の文法では記述できないものだという意味です。
処理系に組み込まれた特別なものだ、ということです。
coe について。
（原文引用）
Function coe is an eliminator for the interval type. For every type over the interval, it allows one to transport elements from the fiber over left to the fiber over an arbitrary point.
（筆者による日本語訳）
関数
coeは、区間型の除去子である。区間上の任意の型について、leftの上にあるファイバーから、任意の点の上にあるファイバーへ要素を輸送することを可能にする。
出典：同上
タロウくん：
「除去子」「ファイバー」という語が出てきました。
専任講師：
除去子は、その型の値を使って何かをするための道具です。
Haskell でいえば、case にあたるものだとお考えください。
ファイバーは、区間の各点に対応する型のことです。
区間の左端に１つ、右端に１つ、型が対応している。coe は、左端の型の値を、右端の型へ運びます。
iso について。
（原文引用）
The definition of iso is not correct since it uses pattern matching on the interval. This definition implies the univalence axiom.
（筆者による日本語訳）
isoの定義は、区間についてのパターン照合を使うため、正しい定義ではない。この定義は、一価性公理を含意する。
出典：同上
タロウくん：
「一価性公理を含意する」・・・先ほどの主張ですね。
専任講師：
そうです。「同じ構造を持つなら等しい」という主張です。
iso を備えることで、Arend はその主張を体系のなかに取り込んでいます。
２通りの根拠を作りました
専任講師：
コードの中ほどに注目してください。
\func idPath : Bool = Bool => path (iso boolId boolId boolIdId boolIdId)
\func negPath : Bool = Bool => path (iso boolNeg boolNeg boolNegNeg boolNegNeg)
どちらも型は Bool = Bool です。 つまり「Bool と Bool は等しい」という主張です。
しかし、中身が違います。
| 使った関数 | どういう対応か | |
|---|---|---|
idPath |
boolId |
true を true に、false を false に |
negPath |
boolNeg |
true を false に、false を true に |
タロウくん：
・・・同じ主張なのに、根拠が２つある。
専任講師：
そこが、HoTT の特徴です。
「等しい」という主張は同じでも、「どう対応させて等しいと見なすか」が違います。
根拠が違えば、運ばれる値が違う
専任講師：
それぞれの根拠に沿って、true を運んでみます。
\func movedId : Bool => coe (\lam i => idPath @ i) true right
\func movedNeg : Bool => coe (\lam i => negPath @ i) true right
\func check1 : movedId = true => idp
\func check2 : movedNeg = false => idp
両方とも、型検査を通過します。
$ java -jar Arend.jar BN2.ard
--- Typechecking \default ---
[ ] src.BN2
--- Done (177ms) ---
タロウくん：
idPath で運ぶと true、negPath で運ぶと false ・・・。
専任講師：
行き先の型は、どちらも Bool です。
変わったのは、運ばれた値のほうです。
タロウくん：
・・・根拠を区別できるから、結果も違う。
専任講師：
idp は、両辺が計算して同じ形になるときにだけ記述できます。
check1 と check2 が通ったということは、処理系が実際に計算し、true と false にそれぞれ到達したということです。
タロウくん：
・・・「等しい」という根拠が、値を動かした。
専任講師：
それが、HoTT の計算規則です。
Arend では、iso で根拠を作り、coe で値を運ぶ。この２つの組み合わせが規則の実体です。
Cubical Agda では、どうなるか
タロウくん：
Cubical Agda では、どうなりますか。
専任講師：
名前が違うだけで、やっていることは同じです。
-- 「等しい」という根拠を作る
ua : A ≃ B → A ≡ B
-- その根拠に沿って値を運ぶ
transport : A ≡ B → A → B
-- 運んだ結果が計算される
_ : transport (ua not≃) false ≡ true
_ = refl
記号を説明します。
| 記号 | 意味 | Arend でいえば |
|---|---|---|
≃ |
一対一に対応する | ── |
≡ |
等しい | = |
ua |
対応から等しさの根拠を作る |
iso ＋ path
|
transport |
根拠に沿って値を運ぶ | coe |
refl |
両辺が計算して同じ形になる証拠 | idp |
_ |
名前を付けずに定義する | ── |
出典：Internalizing Representation Independence with Univalence, arXiv:2009.05547
タロウくん：
・・・ua が Arend の iso、transport が coe にあたるのですね。
専任講師：
そういう対応です。
タロウくん：
ua と refl も、何かの略ですか。
専任講師：
refl については、公式ドキュメントに説明があります。
（原文引用）
For example, this is the definition of the constant path (or proof of reflexivity)
（筆者による日本語訳）
たとえば、これが定数の道（あるいは反射性の証明）の定義である。
出典：Cubical — Agda Documentation
reflexivity（反射性）の略です。
タロウくん：
反射性、というのは。
専任講師：
「$a$ は $a$ に等しい」という、当たり前の性質です。
Arend の idp にあたります。
タロウくん：
ua のほうは。
専任講師：
公式ドキュメントに略語の元は書かれていません。
ただし、ua が現れる文脈から読み取れます。
（原文引用）
Transporting along the path that we get from applying ua to an equivalence is hence the same as applying the equivalence. This is what makes it possible to use the univalence axiom computationally in Cubical Agda.
（筆者による日本語訳）
同値に
uaを適用して得られる道に沿って輸送することは、その同値を適用することと同じである。これが、Cubical Agda において一価性公理を計算的に使うことを可能にしている。
出典：同上
univalence axiom（一価性公理）の略と読めます。
タロウくん：
・・・略語の元が明記されているのは、refl だけなのですね。
専任講師：
ua、iso、coe、idp については、文脈から読み取るほかありません。
タロウくん：
先ほどの Rocq の HoTT ライブラリでは、これがどうなるのですか。
専任講師：
ua にあたるものが、公理として宣言されているだけです。
対応から根拠を作る手順が記述されていないため、transport に渡しても計算が進みません。
refl で示そうとしても、そこで止まります。
タロウくん：
・・・３つの言語で、道具の名前は違っても、やろうとしていることは同じ。
専任講師：
違うのは、その道具に計算の手順が備わっているかどうかです。
ただし Arend は区間 I を、普通の型である文字列型や整数型と同じように扱う。そのぶん、区間 I を計算に使う場面では、計算が途中で止まる状況が出てきます。
そして Cubical Agda
HoTT を検証すべき定理として扱い、かつ区間 I を普通の型とは別の場所に置きます。
理論はそのぶん複雑になり、プログラマの負担も大きくなる。
その代わりに、計算はより先まで進むのです。
タロウくん：
・・・３つを並べると、こうなりますか？
| 言語 | HoTT の扱い | この比較で見ている計算 |
|---|---|---|
| Rocq の HoTT ライブラリ | 公理として受け取る | 公理を使ったところで、定義的な計算は進まない |
| Arend | 計算規則を持つ。区間は普通の型 | 一部の HoTT 的構成を計算できる |
| Cubical Agda | 計算規則を持つ。区間は別の場所 | より広い範囲を計算的に扱える |
専任講師：
そうなりますね。
この記事で取り上げる ３つの場面 だけを見ると、
プログラマにかかる負担は、それとは逆の順番 になります。
| 言語 | ３つの場面での負担 |
|---|---|
| Rocq の HoTT ライブラリ | 最も小さい |
| Arend | 中間 |
| Cubical Agda | 最も大きい |
言語全体としての負担を比べたものではありません。
タロウくん：
・・・計算が進むほど、負担も増える。
専任講師：
そこがトレードオフです。
では、その負担が具体的にどういう場面で生じるのか。３つの場面を取り上げます。
先に、全体像をお見せしましょう。
| 場面 | どういうときに出てくるか | |
|---|---|---|
| １ | 区間を普通の型の材料にできるかどうか | データ構造を組み立てるとき |
| ２ | 面条件を自分で書き並べる | 道と道の関係を証明するとき |
| ３ |
J 規則を自分で組み立てる |
等しさについて場合分けしたいとき |
タロウくん：
・・・どれも、まだ何のことか分かりません。
専任講師：
それで構いません。いまは、３つあるということだけ掴んでください。
もう少しだけ、それぞれの中身を述べておきます。
場面１ ── データ構造を組み立てるとき
リストや組といった、普通のデータ構造を定義する場面です。
ここでは、型構成子（type former）という言葉がキーワードになるので、まずはこの言葉から説明します。
型構成子とは、型宣言で使う部品のことです。
Haskell で書けば、次の List や (,) や -> がそれにあたります。
List Int -- List が型構成子。Int を渡して「Int のリスト」を作る
(Int, String) -- (,) が型構成子。２つの型を渡して「組」を作る
Int -> String -- -> が型構成子。２つの型を渡して「関数の型」を作る
型を受け取って、新しい型を作る仕組みです。
タロウくん：
・・・型を組み立てる部品ですね。
専任講師：
そして、区間 I を型構成子に渡せるかどうかが、この場面の主題です。
Arend では、型構成子に、区間 I を渡すことができます。その理由は、Arend が区間 I を普通の型と同じに扱うからです。
文字列型や整数型と、まったく同じ場所に置かれています。だから、文字列型や整数型を渡せる場所には、区間も渡せます。
List I -- 区間を要素に持つリスト
Nat -> I -- 自然数から区間への関数
\Sigma I I -- 区間２つの組
タロウくん：
Cubical Agda では、どうなりますか。
専任講師：
Cubical Agda では、型構成子に区間 I を渡すことができません。その理由は、Cubical Agda が区間 I を普通の型とは別物として扱うからです。
普通の型が置かれる場所と、区間が置かれる場所が分かれています。そのため、普通の型を渡す場所に区間を渡せません。
タロウくん：
・・・置き場所が違うから、渡せない。
専任講師：
そういうことです。
この場面で増えるのは、記述量ではありません。
「この位置に区間を記述してよいか」という判断の手間が増えます。
場面２ ── 道と道の関係を証明するとき
「２つの道が同じである」ことを示す場面です。
まず、道と道の関係を図で示します。
２点をつなぐ線分が、道です。
p
a ─────────── b
← １次元（線分）
同じ２点をつなぐ道が２本ある場合、その２本をつなぐ道を引けます。
p
a ─────────── b
│ │
idp │ α │ idp ← 左辺・右辺は、その場に留まる道
│ │
a ─────────── b
q
← ２次元（正方形）。α が、道 p と道 q をつなぐ
タロウくん：
・・・正方形になりました。
専任講師：
道は線分です。線分と線分の関係を描くには、縦横２つの方向が要ります。
上の辺が道 p、下の辺が道 q です。
左辺と右辺は、a と b の位置に留まったままの道です。
タロウくん：
正方形の内側が、α ですか。
専任講師：
そのとおりです。α が、道 p と道 q をつないでいます。
タロウくん：
先生、ひとつ確かめさせてください。
α は、面なのですか。つまり、正方形の内側の２次元の領域ですか。
それとも、２つの線分を縦方向に結ぶ、縦向きの線分なのですか。
専任講師：
どちらの見方も正しいのです。
タロウくん：
両方、ですか。
専任講師：
まず、α は２つの区間変数を受け取ります。
Arend で確かめてみましょう。
\data Bool | true | false
\func p1 : true = {Bool} true => idp
\func p2 : true = {Bool} true => idp
-- α は、道と道のあいだの道
\func alpha : p1 = p2 => idp
-- α の位置 i における値を取り出すと、道が得られる
\func atI (i : I) : true = {Bool} true => alpha @ i
-- さらに、その道の位置 j における値を取り出すと、点が得られる
\func atIJ (i j : I) : Bool => (alpha @ i) @ j
型検査を通過します。
$ java -jar Arend.jar ALPHA.ard
--- Typechecking \default ---
[ ] src.ALPHA
--- Done (178ms) ---
タロウくん：
@ を２回使うと、点が取り出せるのですね。
専任講師：
i と j の２つを与えると、点が決まる。つまり α は、２次元の領域を描いています。
タロウくん：
では、縦向きの線分という見方は。
専任講師：
i を１つ固定してみてください。
\func atI (i : I) : true = {Bool} true => alpha @ i
alpha @ i の型は true = true、つまり道です。
タロウくん：
・・・i を決めると、道が１本出てくる。
専任講師：
その道が、縦向きの線分にあたります。
p
a ─────────── b
│ │ │ │ │
│ │ │ │ │ ← i を固定するごとに、縦の線分が１本
│ │ │ │ │
a ─────────── b
q
i = i0 のとき ─── p の位置
i = i1 のとき ─── q の位置
タロウくん：
・・・その線分が、隙間なく並んでいる。
専任講師：
並んだ線分の全体が、正方形を埋めています。
| 見方 | どう捉えるか |
|---|---|
| 全体として | 正方形という２次元の領域 |
i を固定すると |
縦向きの線分が１本 |
どちらも、同じものを別の角度から見ているのです。
面条件とは何か
専任講師：
この正方形のうち、どの辺がどういう値で埋まっているか。それを指定するものが、面条件です。
p ← 上辺：道 p
a ─────────── b
│ │
idp │ ？ │ idp ← 左辺・右辺：面条件で指定する
│ │
a ─────────── b
q ← 下辺：道 q
？の部分を埋めるのが、道と道をつなぐ操作
タロウくん：
・・・周りが決まっていて、中を埋める。
専任講師：
Arend では、この作業を処理系が引き受けます。
道について場合分けすれば、残りは処理系が埋めてくれます。２行で記述できます。
Cubical Agda では、証明を書く側が指定します。
左辺は何、右辺は何。そうやって、各辺を書き並べることになるのです。
この場面では、記述量がはっきり増えます。
場面３ ── 等しさについて場合分けしたいとき
「$a$ と $b$ が等しい」という前提から、何かを導く場面です。
ここでは、J という言葉がキーワードになるので、まずはこの言葉から説明します。
J は、帰納的な定義の発想を、等しさに適用したものです。
タロウくん：
帰納的な定義、といいますと。
専任講師：
自然数の定義を思い出してください。
data Nat = Zero | Suc Nat
自然数は、Zero と Suc の２つだけで作られます。
だから、自然数について何かを示したいとき、Zero の場合と Suc の場合を示せば足ります。
タロウくん：
・・・数学的帰納法ですね。
専任講師：
同じ発想を、等しさに適用します。
「$a$ と $b$ が等しい」という根拠は、どこから来たのか。
もとをたどれば、「$a$ は $a$ に等しい」という当たり前の根拠にたどり着きます。
タロウくん：
自然数でいう Zero にあたるもの。
専任講師：
自然数の帰納法では、Zero の場合を示すことが出発点でした。
等しさについては、idp の場合を示すことが出発点になります。
だから、等しさについて何かを示したいとき、「$a$ は $a$ に等しい」場合だけを示せば足ります。
この原理を、J といいます。
タロウくん：
先生、いまの説明で確かめたいことがあります。
自然数の例では、Zero と Suc の２つがありました。そして a = a が Zero に対応するとのことでした。
では、Suc に対応するものは何ですか。
専任講師：
存在しません。
タロウくん：
えっ。
専任講師：
そこが、自然数との決定的な違いです。
自然数を作る方法は２つあります。
data Nat = Zero | Suc Nat
Zero から始めるか、すでにある自然数に Suc をかぶせるか。
タロウくん：
はい。
専任講師：
一方、等しさの根拠を作る方法は１つしかありません。
a = a という当たり前の根拠。それだけです。
タロウくん：
・・・Suc にあたるものが、ない。
専任講師：
Arend で確かめてみましょう。
自然数の帰納法を書くと、場合が２つ出てきます。
\func natInd (P : Nat -> \Type) (base : P 0)
(step : \Pi (n : Nat) -> P n -> P (suc n)) (n : Nat) : P n \elim n
| 0 => base
| suc m => step m (natInd P base step m)
| 0 => と | suc m => の２行です。
一方、J を書くと、場合は１つだけです。
\func J {A : \Type} {a : A} (B : \Pi (a' : A) -> a = a' -> \Type)
(b : B a idp) {a' : A} (p : a = a') : B a' p \elim p
| idp => b
| idp => の１行しかありません。
型検査は、どちらも通過します。
$ java -jar Arend.jar JIND.ard
--- Typechecking \default ---
[ ] src.JIND
--- Done (276ms) ---
タロウくん：
・・・本当に、１行だけですね。
専任講師：
別の構成子で場合分けしようとすると、弾かれます。
\func f {A : \Type} {a a' : A} (p : a = a') : Nat \elim p
| idp => 0
| suc _ => 1
型検査は通りません。
[ERROR] 'Nat.suc' is not a constructor of data type Path
In: suc _
「suc は Path という型の構成子ではない」 と述べられています。
タロウくん：
・・・等しさの型には、idp という構成子しかない。
専任講師：
だから、idp の場合だけを示せば足りるのです。
自然数のように、「次の場合へ進む」という段取りが要りません。
タロウくん：
帰納法 というより、「唯一の場合を確かめる」 に近いですね。
専任講師：
そのとおりです。
| 構成子 | 示すべき場合 | |
|---|---|---|
| 自然数 |
Zero と Suc
|
２つ |
| 等しさ |
idp のみ |
１つ |
「帰納法」 という言葉は使いますが、自然数の帰納法とは形が違います 。
タロウくん：
なぜ J という名前なのですか。
専任講師：
マーティン＝レーフが最初にこの規則を示したときから、この名前が使われています。
由来については、筆者が調べた範囲では、信頼できる説明を見つけられませんでした。
タロウくん：
アルファベットの J に、意味はないのかもしれませんね。
専任講師：
そう考えるほかありません。
両言語で、J の書き方が違います
専任講師：
Arend では、J を場合分けとして記述できます。
Haskell の case のように、| idp => ... と記述するだけで済むのです。
Cubical Agda では、その書き方が許されていません。
代わりに、J という道具を引数を指定しながら自分で組み立てることになります。
タロウくん：
・・・同じことをするのに、手数が違う。
専任講師：
この場面でも、記述量が増えます。
３つを並べると
| 場面 | 判断の手間 | 記述量 |
|---|---|---|
| １. データ構造を組み立てるとき | 増える | 増えない |
| ２. 道と道の関係を証明するとき | 増える | 増える |
| ３. 等しさについて場合分けしたいとき | 増える | 増える |
タロウくん：
・・・場面１だけ、記述量は増えないのですね。
専任講師：
記述できないものを記述しないだけですから。
では、場面１から順に見ていきましょう。
場面１ ── 区間を型構成子に渡せるかどうか
専任講師：
場面１の状況設定は、区間を他の型を作る材料として使えるかどうかです。
コードがこれです。
Arend のコードと Cubical Agda のコードを並べて比較して行きましょう。
＜Arend のコード＞
\data List (A : \Type) | nil | cons A (List A)
\func xs : List I => cons left (cons right nil)
\func g (n : Nat) : I => left
\func p : \Sigma I I => (left, right)
\func h (i : I) : Nat => 0
＜Cubical Agda のコード＞
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
data List (A : Set) : Set where
nil : List A
cons : A → List A → List A
xs : List I -- 記述できない
g : ℕ → I -- 記述できない
p : Σ I (λ _ → I) -- 記述できない
h : I → ℕ -- 記述できる
タロウくん：
うわぁ。どちらの言語のコードも、ほぼコードの意味がわからないです。
わたしは Haskell の文法と考え方を学び始めたばかりで、Arend も、Cubical Agda も、文法や記号の意味をまだなにも知らないんです。
この第２回記事のなかの対話では、面条件とか、立方体型理論について教えていただくなかで、少しずつ理論面の理解を積み上げ始めるスタート地点にようやく立ったばかりなんです。
でも、面条件や立方体型理論についても、まだ理解が浅すぎるので、ましてやそれらの難しい概念が、まだ文法や記号の意味すら学んでいない Arend のコードと Cubical Agda のコードに、どう実装されているのかをコードリーディングして読み解いていく基礎体力が準備できていません。
専任講師：
了解。
まずは Arend のコード解説から始めます。
文法・記号の解説から、丁寧に進めましょう。
その後で、Cubical Agda のコード解説に移ります。
Arend のコード解説
Arend の記号 ── Haskell との対応
Arend の記号は、\ で始まるものが多くあります。
| Arend | 意味 | Haskell でいえば |
|---|---|---|
\data |
データ型を定義する | data |
\func |
関数や値を定義する | 関数定義（f x = ...） |
=> |
定義の本体を書き始める | = |
\Type |
型が置かれる場所 |
Type（*） |
\Sigma |
組の型を作る | (,) |
-> |
関数の型を作る | -> |
| |
データ型の選択肢を区切る | | |
: |
「〜の型を持つ」 | :: |
left / right
|
区間の両端 | ── |
Arend の公式マニュアルは、次のページにあります。
- 言語リファレンス：https://arend-lang.github.io/documentation/language-reference/
- 入門用のチュートリアル：https://arend-lang.github.io/documentation/tutorial/
タロウくん：
\ で始まるのは、Haskell のラムダ式と紛らわしいですね。
専任講師：
Arend では、\ はキーワードの目印です。
Haskell の \x -> ... にあたるものは、Arend では \lam x => ... と記述します。\lam で１つのキーワードです。
１行目 ── リストの定義
＜Arend のコード＞
\data List (A : \Type) | nil | cons A (List A)
＜Haskell で書けば＞
data List a = Nil | Cons a (List a)
１つずつ対応させます。
| Arend | Haskell | 意味 |
|---|---|---|
\data List |
data List |
List という型を定義する |
(A : \Type) |
a |
型引数。A は型である |
| nil |
= Nil |
選択肢その１。空リスト |
| cons A (List A) |
| Cons a (List a) |
選択肢その２。先頭と残り |
タロウくん：
(A : \Type) の書き方が Haskell と違いますね。
専任講師：
Arend では、型引数にも型を明示します。
A : \Type は、「A は \Type に属する」という意味です。
ここが、この場面の要点につながります。
\Type とは何か
タロウくん：
\Type というのが、その「型が置かれる場所」ですか。
専任講師：
そうです。Arend には、型を集めた場所があります。
何が属しているのか、実際に確かめてみましょう。
＜Arend のコード＞
\func t1 : \Type => Nat
\func t2 : \Type => I
\func t3 : \Type => \Sigma Nat Nat
\func t4 : \Type => Nat -> Nat
\func t5 : \Type => I -> Nat
\func t6 : \Type => Nat -> I
＜Arend の型検査結果＞
$ java -jar Arend.jar S1B.ard
--- Typechecking \default ---
[ ] src.S1B
--- Done (87ms) ---
タロウくん：
Nat も I も、組の型も関数の型も・・・全部通っていますね。
専任講師：
I が２行目にあることに注目してください。
区間は、Nat とまったく同じ資格で \Type に属しています。
タロウくん：
Nat -> I も通っていますね。返り値が区間の関数。
専任講師：
Arend では、これも普通の型です。
この事実が、以下のコードすべての土台になります。
２行目 ── 区間を要素に持つリスト
＜Arend のコード＞
\func xs : List I => cons left (cons right nil)
＜Haskell で書けば＞
xs :: List I
xs = Cons left (Cons right Nil)
１つずつ見ます。
| 部分 | 意味 |
|---|---|
\func xs |
xs という名前で定義する |
: List I |
その型は List I
|
=> |
ここから本体 |
cons left (cons right nil) |
left と right を要素に持つリスト |
タロウくん：
cons left (cons right nil) の括弧は、必要なのですか。
専任講師：
必要です。外すと別の意味になります。
関数適用は、左から順に結合します。Haskell と同じ規則です。
括弧を外して cons left cons right nil と記述すると、cons に４つの引数を渡そうとしていることになり、型検査で弾かれます。
タロウくん：
List I の I が、型引数として渡されている。
専任講師：
List は \Type の要素を型引数として受け取ります。I は \Type の要素ですから、渡せるのです。
ここからが深掘りです ── 渡したあと、何ができるのか
タロウくん：
先生、List I が作れるとして、そのリストで何ができるのですか。
専任講師：
普通のリストとして扱えます。
長さを数える関数を書いてみましょう。
＜Arend のコード＞
\func length {A : \Type} (l : List A) : Nat \elim l
| nil => 0
| cons _ rest => suc (length rest)
\func lenXs : length xs = 2 => idp
タロウくん：
{A : \Type} の波括弧は。
専任講師：
暗黙の引数です。呼び出すときに書かなくても、処理系が推論してくれます。
Haskell の型変数 a にあたるものだとお考えください。
タロウくん：
length xs = 2 が idp で示せた・・・処理系が実際に数えたのですね。
専任講師：
xs は要素が２つのリストですから、長さは 2 です。
区間を要素にしていても、リストとしての振る舞いは変わりません。
タロウくん：
中身を取り出すこともできますか。
専任講師：
できます。
＜Arend のコード＞
\func head {A : \Type} (d : A) (l : List A) : A \elim l
| nil => d
| cons x _ => x
\func firstOfXs : I => head left xs
＜Arend の型検査結果＞
$ java -jar Arend.jar S1DEEP.ard
--- Typechecking \default ---
[ ] src.S1DEEP
--- Done (174ms) ---
firstOfXs の型が I になっている点に注目してください。
タロウくん：
・・・リストから取り出したものが、区間の値。
専任講師：
区間は、他の型と完全に同じ扱いを受けています。
リストに入れられる。長さを数えられる。取り出せる。どこにも特別扱いがありません。
ただし、区間には１つだけ制約があります
タロウくん：
では、区間は完全に普通の型なのですか。
専任講師：
１点だけ違います。
取り出した区間の値で、場合分けができません。
＜Arend のコード＞
\data Bool | true | false
\func f (i : I) : Bool \elim i
| left => true
| right => false
＜Arend の型検査結果＞
[ERROR] Pattern matching on the interval is not allowed here
In: f
タロウくん：
「区間についてのパターン照合は、ここでは許されていない」・・・。
専任講師：
この制約は、Cubical Agda にもあります。両言語で共通です。
Arend の公式マニュアルが、理由を述べています。
（原文引用）
The definition of the interval type \data I | left | right looks like the definition of the set with two elements, but this is not true actually. One way to think about this data type is that it has one more constructor, which connects left and right and which cannot be accessed explicitly. This means that it is forbidden to define a function on I by pattern matching.
（筆者による日本語訳）
区間型
\data I | left | rightの定義は、要素が２つの集合の定義のように見えるが、実際にはそうではない。このデータ型には、leftとrightを結ぶ構成子がもう１つあり、それは明示的にアクセスできない、と考えるとよい。このため、I上の関数をパターン照合で定義することは禁じられている。
出典：Prelude — Arend Theorem Prover
タロウくん：
「left と right を結ぶ構成子がもう１つある」・・・？
専任講師：
区間は、２つの点だけでできているのではありません。
left と right のあいだが、つながっているのです。
left ●━━━━━━━━━━━● right
↑
ここが「もう１つの構成子」
明示的には触れない
タロウくん：
・・・線分そのもの、ということですか。
専任講師：
そういうイメージで考えると分かりやすいです。ただし、数学的には実数の線分ではありません。
２つの点ではなく、切れ目のないひとつながりのものだとお考えください。
だから、「左端ならこちら、右端ならあちら」と結果を切り替える関数を許すと、線分が途中で切れてしまいます。
タロウくん：
それで、場合分けが禁じられている。
専任講師：
両言語に共通の制約です。ここは違いではありません。
３行目 ── 自然数から区間への関数
＜Arend のコード＞
\func g (n : Nat) : I => left
＜Haskell で書けば＞
g :: Nat -> I
g n = left
| 部分 | 意味 |
|---|---|
\func g |
g という関数を定義する |
(n : Nat) |
引数 n は Nat
|
: I |
返り値の型は I
|
=> left |
常に left を返す |
タロウくん：
n を受け取っているのに、使っていませんね。
専任講師：
使わなくても構いません。定数関数です。
ここで確かめたいのは、「返り値の型に I を記述できるかどうか」 だけですから。
タロウくん：
なぜ、そこが問題になるのですか。
専任講師：
この形が、Cubical Agda では記述できないからです。
先ほどの \Type の確認で、Nat -> I が通っていたことを思い出してください。
４行目 ── 区間を成分に持つ組
＜Arend のコード＞
\func p : \Sigma I I => (left, right)
＜Haskell で書けば＞
p :: (I, I)
p = (left, right)
\Sigma I I が、「I と I の組」 を表します。
タロウくん：
\Sigma が Haskell のタプルにあたるのですね。
専任講師：
ここでは、依存型ではない単純な組として使っているので、Haskell のタプルに近いものとして考えてください。
ただし Arend の \Sigma は、依存型も記述できます。
第１成分の値によって、第２成分の型が変わる。
そういう組をつくることもできます。
今回は、その機能は使いません。
５行目 ── 区間から自然数への関数
＜Arend のコード＞
\func h (i : I) : Nat => 0
引数の型が I、返り値の型が Nat。先ほどの g と、向きが逆です。
タロウくん：
これも、Arend では書けるのですね。
専任講師：
この形だけは、Cubical Agda でも記述できます。
そこが、あとで効いてきます。
Arend 側をまとめます
＜Arend の型検査結果＞
$ java -jar Arend.jar B2.ard
--- Typechecking \default ---
[ ] src.B2
--- Done (117ms) ---
エラーが出ませんでした。すべて正しく記述できています。
タロウくん：
[ ] src.B2 というのは。
専任講師：
「このファイルを型検査した」という印です。角括弧の中にエラーの印が出ていなければ、通ったということです。
専任講師：
５行すべてで、区間を型構成子に渡しています。
＜Arend のコード＞
\data List (A : \Type) | nil | cons A (List A)
-- 型構成子 List に、区間 I を渡している
\func xs : List I => cons left (cons right nil)
-- 型構成子 -> に、Nat と I を渡している
\func g (n : Nat) : I => left
-- 型構成子 \Sigma に、区間 I を２つ渡している
\func p : \Sigma I I => (left, right)
-- 型構成子 -> に、I と Nat を渡している
\func h (i : I) : Nat => 0
渡せる理由は、区間が \Type に属しているからです。
＜Arend のコード＞
\func t2 : \Type => I
この一行が、すべての土台になっています。
Cubical Agda のコード解説
専任講師：
では、Cubical Agda に移ります。
はじめにお断りしておきます。筆者の執筆環境には Cubical Agda を用意できませんでした。
そのため以下は、Agda 公式ドキュメントおよび Agda の課題管理システムの記載に基づく説明です。実行結果は掲載しません。
Cubical Agda の記号 ── Haskell との対応
| Cubical Agda | 意味 | Haskell でいえば | Arend でいえば |
|---|---|---|---|
data ... where |
データ型を定義する | data |
\data |
: |
「〜の型を持つ」 | :: |
: |
→ |
関数の型を作る | -> |
-> |
Set |
型が置かれる場所 | Type |
\Type |
Σ |
組の型を作る | (,) |
\Sigma |
ℕ |
自然数 | 自然数型 | Nat |
I |
区間 | ── | I |
i0 / i1
|
区間の両端 | ── |
left / right
|
{-# OPTIONS --cubical #-} |
立方体モードを有効にする | ── | ── |
Agda の公式ドキュメントは、次のページにあります。
タロウくん：
Arend の left と right が、Cubical Agda では i0 と i1 なのですね。
専任講師：
名前は違いますが、ここでは「区間の両端」という同じ役割を持つものとして対応させて考えてください。
なお、両者の理論的な違いについては、記事末尾の発展篇コラムで述べます。
１行目 ── モードの指定
＜Cubical Agda のコード＞
{-# OPTIONS --cubical #-}
タロウくん：
これは何ですか。
専任講師：
立方体型理論の機能を有効にする指定です。
Agda は、この指定がなければ普通の型理論として動きます。区間 I も使えません。
タロウくん：
Arend には、こういう指定がありませんでした。
専任講師：
Arend は、最初から立方体型理論を土台にしているからです。
Agda は、もともと普通の型理論の処理系でした。立方体型理論は、あとから加えられた機能です。
２行目以降 ── ライブラリの読み込み
＜Cubical Agda のコード＞
open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import は、ライブラリを読み込む記述です。
Haskell の import にあたります。
タロウくん：
Cubical.Foundations.Prelude というのは。
専任講師：
区間 I や i0、i1 が、ここに入っています。
Arend では Prelude が自動で読み込まれますが、Cubical Agda では明示的に読み込みます。
リストの定義
＜Cubical Agda のコード＞
data List (A : Set) : Set where
nil : List A
cons : A → List A → List A
＜Arend で書けば＞
\data List (A : \Type) | nil | cons A (List A)
書き方の違いを並べます。
| Cubical Agda | Arend | |
|---|---|---|
| キーワード | data ... where |
\data |
| 型引数 | (A : Set) |
(A : \Type) |
| 型が置かれる場所 | Set |
\Type |
| 構成子の書き方 | 各行に型を明記 |
| で区切る |
タロウくん：
Cubical Agda では、構成子ごとに型を書くのですね。
専任講師：
nil : List A、cons : A → List A → List A。それぞれの型を明示します。
Arend の | cons A (List A) と、同じことを述べています。
ここからが、この場面の要点です
専任講師：
List の型引数は Set の要素でなければなりません。
定義の (A : Set) が、そう述べています。
タロウくん：
では、List I と書くと。
専任講師：
記述できません。区間 I が Set に属していないからです。
Agda 公式ドキュメントが、区間の置き場所を述べています。
（原文引用）
The interval I belongs to its own sort, IUniv. Types in this sort do not support composition and transport (unlike Set), but function types from types in this sort to types in Set do (unlike SSet).
（筆者による日本語訳）
区間
Iは、それ自身のソートIUnivに属する。このソートの型は、（Setとは異なり）合成と輸送をサポートしない。しかし、このソートの型からSetの型への関数型は、（SSetとは異なり）サポートする。
出典：Cubical — Agda Documentation
タロウくん：
IUniv という別の場所にある、と。
専任講師：
Arend との対比が、はっきりします。
区間 I の置き場所 |
普通の型の置き場所 | |
|---|---|---|
| Arend | \Type |
\Type |
| Cubical Agda | IUniv |
Set |
Arend では同じ、Cubical Agda では別々です。
４つの記述を、順に確かめます
＜Cubical Agda のコード＞
xs : List I -- 記述できない
List の型引数は Set の要素でなければならず、I は IUniv に属するためです。
＜Cubical Agda のコード＞
g : ℕ → I -- 記述できない
関数の終域が IUniv に属することになるためです。
この点について、立方体型理論の正規形を扱った論文が理由を述べています。
（原文引用）
One is that the interval should not participate in any type formers, so for example we cannot have functions $f: \mathbb{N} \to \mathbb{I}$ which easily make type-checking undecidable.
（筆者による日本語訳）
１つは、区間が型構成子に一切関与すべきでないということである。たとえば $f : \mathbb{N} \to \mathbb{I}$ のような関数を許すと、型検査の決定可能性を容易に失いうる。
出典："Normal forms in cubical type theory", arXiv:2603.24923
タロウくん：
引用文の $f : \mathbb{N} \to \mathbb{I}$ が、Arend で書いた g そのものですね。
専任講師：
Arend では記述できます。Cubical Agda では記述できません。
＜Cubical Agda のコード＞
p : Σ I (λ _ → I) -- 記述できない
Σ の第１引数も Set の要素でなければならないため、同じ理由で記述できません。
タロウくん：
λ _ → I というのは。
専任講師：
Cubical Agda の Σ は、依存型を前提とした書き方をします。
第２成分の型を、第１成分の値から決める関数として渡すのです。ここでは値を使わないので _ で受け流し、常に I を返しています。
Arend の \Sigma I I と、同じことを述べています。
ただし、１つだけ記述できます
＜Cubical Agda のコード＞
h : I → ℕ -- 記述できる
タロウくん：
これは通るのですか。
専任講師：
通ります。先ほどの引用の後半が、その根拠です。
しかし、このソートの型から
Setの型への関数型は、サポートする。
I は IUniv、ℕ は Set。「IUniv から Set へ向かう関数型」にあたります。
Agda の課題管理システムにも、同じ趣旨の記述があります。
（原文引用）
_ : Set_ = I → ?this is a hard type error, butI → Nat(e.g.) has type Set.
（筆者による日本語訳）
_ : Setに対する_ = I → ?は、確かな型エラーである。しかしI → Nat（たとえば）はSetの型を持つ。
出典：piSort/funSort of IUniv should be blocked on the codomain, agda/agda Issue #6074
タロウくん：
なぜ、この向きだけ許されるのですか。
専任講師：
道 $p : I \to A$ が、まさにこの形だからです。
区間から型への写像。それが道でした。
タロウくん：
・・・道を書くことだけは、許されている。
専任講師：
区間は、そのために置かれた部品ですから。
そして、それ以外の用途は塞がれています。結果として、普通の型についての２つの操作が保たれている、という形になっています。
場面１のまとめ
| 記述 | Arend | Cubical Agda | 理由 |
|---|---|---|---|
List I |
記述できる | 記述できない |
List の引数は Set の要素。I は IUniv
|
Nat -> I |
記述できる | 記述できない | 関数の終域が IUniv になる |
\Sigma I I |
記述できる | 記述できない |
Σ の引数は Set の要素 |
I -> Nat |
記述できる | 記述できる |
IUniv から Set への関数型は許される |
| 区間の場合分け | 記述できない | 記述できない | 両言語で共通の制約 |
タロウくん：
・・・Arend では４つとも記述でき、Cubical Agda では１つだけ。
専任講師：
Cubical Agda でプログラムを書く人は、「この位置に区間を記述してよいか」を常に判断することになります。
Arend では、その判断が要りません。区間を、他の型と同じように扱えるからです。
タロウくん：
記述量としては、どうなりますか。
専任講師：
この場面に限れば、Cubical Agda のコードの行数は、Arend と比べて増えません。
List I を記述しようとすれば、型検査で弾かれます。
記述できないものを記述しないだけです。
増えるのは、プログラマがコーディングする際に判断すべき事柄が増えることから生じる心理的負担感です。
タロウくん：
・・・では、記述量が増える場面もあるのですか。
専任講師：
あります。このあとお見せする場面２と場面３が、それにあたります。
場面２では、道と道の関係を示すために、立方体の面をひとつずつ指定することになります。
場面３では、J という除去規則の引数を、自分で組み立てることになります。
どちらも、Arend では２行で書けるものです。
タロウくん：
・・・行数が、はっきり増える。
専任講師：
そういう場面が出てきます。
場面２ ── 面条件を自分で書き並べる
専任講師：
場面２の状況設定は、道と道の関係を証明する場面です。で、コードがこれです。
＜Arend のコード＞
\func concat {A : \Type} {a b c : A} (p : a = b) (q : b = c) : a = c \elim q
| idp => p
\func concat-idp {A : \Type} {a b : A} (p : a = b) : concat p idp = p => idp
\func assoc {A : \Type} {a b c d : A} (p : a = b) (q : b = c) (r : c = d)
: concat (concat p q) r = concat p (concat q r) \elim r
| idp => idp
＜Cubical Agda のコード＞
compPathRefl : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → compPath p refl ≡ p
compPathRefl {x = x} {y = y} p j i =
hfill (λ _ → λ { (i = i0) → x ; (i = i1) → y }) (inS (p i)) (~ j)
タロウくん：
Arend のほうは短いですね。Cubical Agda のほうは、記号が多くて読めません。
専任講師：
まずは Arend のコード解説から始めます。
その後で、Cubical Agda のコード解説に移ります。
Arend のコード解説
この場面で新しく出てくる記号
場面１で説明した記号に加えて、次のものが出てきます。
| Arend | 意味 |
|---|---|
{A : \Type} |
暗黙の引数。呼び出し時に書かなくてよい |
a = b |
a と b が等しいことを表す型 |
idp |
「両辺が計算して同じ形になる」ことを示す証拠 |
\elim q |
引数 q について場合分けする |
１つ目 ── 道をつなぐ関数
＜Arend のコード＞
\func concat {A : \Type} {a b c : A} (p : a = b) (q : b = c) : a = c \elim q
| idp => p
型の部分を、順に読みます。
| 部分 | 意味 |
|---|---|
{A : \Type} |
型 A を暗黙に受け取る |
{a b c : A} |
A の値を３つ、暗黙に受け取る |
(p : a = b) |
a から b への道 |
(q : b = c) |
b から c への道 |
: a = c |
返すのは、a から c への道 |
タロウくん：
・・・２本の道を受け取って、１本の道を返す。
専任講師：
図にすると、こうなります。
p q
a ───────→ b ───────→ c
↓ concat
a ───────→ c
タロウくん：
本体の | idp => p が、まだ分かりません。
専任講師：
\elim q が、引数 q について場合分けしています。
q は b = c という道です。そして、道の作り方は idp の場合だけを考えれば足りました。
タロウくん：
場面３で説明された、J の話ですね。
専任講師：
そうです。q が idp の場合、b と c は同じものになります。
そのとき、求める道 a = c は a = b と同じです。つまり、p をそのまま返せばよいのです。
タロウくん：
・・・だから | idp => p の１行で済む。
専任講師：
実際に動かしてみましょう。
＜Arend のコード＞
\data Bool | true | false
\func p1 : true = {Bool} true => idp
\func joined : true = {Bool} true => concat p1 p1
\func check : joined = idp => idp
＜Arend の型検査結果＞
$ java -jar Arend.jar S2B.ard
--- Typechecking \default ---
[ ] src.S2B
--- Done (146ms) ---
タロウくん：
joined = idp が idp で示せた。処理系が計算したのですね。
専任講師：
idp どうしをつないだ結果が、idp になっています。
２つ目 ── 道に idp をつないでも変わらない
＜Arend のコード＞
\func concat-idp {A : \Type} {a b : A} (p : a = b) : concat p idp = p => idp
型が述べている主張を読み解きます。
$$\mathrm{concat}(p, \mathrm{idp}) = p$$
「道 p に idp をつないでも、p のまま」 ということです。
タロウくん：
\elim がありませんね。
専任講師：
場合分けが要らないからです。
concat の定義を見てください。第２引数が idp のとき、p をそのまま返しています。
＜Arend のコード＞
\func concat {A : \Type} {a b c : A} (p : a = b) (q : b = c) : a = c \elim q
| idp => p
concat p idp は、定義に従って計算すると p になります。
タロウくん：
・・・計算するだけで、同じ形になる。
専任講師：
だから idp で示せます。本体は => idp の一語です。
３つ目 ── 結合律
＜Arend のコード＞
\func assoc {A : \Type} {a b c d : A} (p : a = b) (q : b = c) (r : c = d)
: concat (concat p q) r = concat p (concat q r) \elim r
| idp => idp
型が述べている主張を読み解きます。
$$\mathrm{concat}(\mathrm{concat}(p, q), r) = \mathrm{concat}(p, \mathrm{concat}(q, r))$$
左辺は、前の２本を先につないでから、３本目をつなぐ。
右辺は、後ろの２本を先につないでから、１本目をつなぐ。
タロウくん：
・・・つなぐ順序が違う。
専任講師：
図にすると、こうなります。
p q r
a ──────→ b ──────→ c ──────→ d
左辺：(p と q) を先につないでから、r をつなぐ
右辺：(q と r) を先につないでから、p をつなぐ
どちらでも同じ結果になる。それを証明します。
タロウくん：
本体は、また | idp => idp の１行ですね。
専任講師：
\elim r が、３本目の道 r について場合分けしています。
r が idp のとき、c と d は同じものになります。そのとき、左辺と右辺はどちらも concat p q に計算されます。
タロウくん：
・・・同じ形になるから、idp で示せる。
専任講師：
Arend では、場合分けと計算だけで済みます。
Arend 側をまとめます
＜Arend の型検査結果＞
$ java -jar Arend.jar S2A.ard
--- Typechecking \default ---
[ ] src.S2A
--- Done (242ms) ---
３つとも、型検査を通過しました。
| 関数 | 本体の行数 |
|---|---|
concat |
１行（| idp => p） |
concat-idp |
本体は idp の一語 |
assoc |
１行（| idp => idp） |
証明を書く側が指定するのは、場合分けの１行だけです。
残りは、処理系が計算で埋めます。
Cubical Agda のコード解説
専任講師：
では、Cubical Agda に移ります。
先ほどと同じく、筆者の執筆環境には Cubical Agda を用意できませんでした。以下は Agda 公式ドキュメントの記載に基づく説明です。
取り上げるのは、Arend の concat-idp にあたる主張です。
「道 p に refl をつないでも、p のまま」。先ほど Arend では、本体が idp の一語で済みました。
＜Cubical Agda のコード＞
compPathRefl : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → compPath p refl ≡ p
compPathRefl {x = x} {y = y} p j i =
hfill (λ _ → λ { (i = i0) → x ; (i = i1) → y }) (inS (p i)) (~ j)
出典：Cubical — Agda Documentation
タロウくん：
・・・３行ありますね。
専任講師：
１行ずつ読み解きましょう。まず、この場面で新しく出てくる記号です。
この場面で新しく出てくる記号
| Cubical Agda | 意味 | Arend でいえば |
|---|---|---|
∀ {ℓ} |
宇宙のレベルを暗黙に受け取る | ── |
Set ℓ |
レベル ℓ の型が置かれる場所 |
\Type |
≡ |
等しいことを表す型 | = |
refl |
反射性の証拠 | idp |
compPath |
道をつなぐ操作 | concat |
λ { ... } |
場合分けを含む無名関数 | ── |
(i = i0) |
区間変数 i が左端のとき |
── |
~ j |
区間の反転 | ── |
hfill |
開いた箱の内部を埋める操作 | ── |
inS |
底面として渡すための操作 | ── |
１行目 ── 型の宣言
＜Cubical Agda のコード＞
compPathRefl : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → compPath p refl ≡ p
＜Arend で書けば＞
\func concat-idp {A : \Type} {a b : A} (p : a = b) : concat p idp = p
並べて比較します。
| Cubical Agda | Arend | 意味 |
|---|---|---|
∀ {ℓ} |
── | 宇宙のレベルを受け取る |
{A : Set ℓ} |
{A : \Type} |
型 A を暗黙に受け取る |
{x y : A} |
{a b : A} |
A の値を２つ、暗黙に受け取る |
(p : x ≡ y) |
(p : a = b) |
x から y への道 |
→ compPath p refl ≡ p |
: concat p idp = p |
示したい主張 |
タロウくん：
∀ {ℓ} だけ、Arend にありませんね。
専任講師：
Agda では、宇宙のレベルを明示的に受け取ります。
Arend では、処理系が推論してくれる部分です。
タロウくん：
・・・型の部分は、ほぼ同じですね。
専任講師：
問題は、次の行からです。
２行目 ── 引数の受け取り
＜Cubical Agda のコード＞
compPathRefl {x = x} {y = y} p j i =
タロウくん：
{x = x} というのは。
専任講師：
暗黙の引数に、名前を付けて受け取る記法です。
{x = x} は、「暗黙の引数 x を、x という名前で使う」という意味です。
タロウくん：
そして p j i の３つが並んでいます。
専任講師：
p は道です。そして j と i が、区間変数です。
タロウくん：
なぜ、区間変数が２つ要るのですか。
専任講師：
示したい主張が、道と道の等しさだからです。
$$\mathrm{compPath}(p, \mathrm{refl}) \equiv p$$
左辺も右辺も、道です。道と道の関係を描くには、縦横２つの方向が要りました。
p
a ─────────── b
│ │
idp │ ？ │ idp
│ │
a ─────────── b
compPath p refl
i が横方向、j が縦方向にあたります。
タロウくん：
・・・Arend では、区間変数を１つも書きませんでした。
専任講師：
そこが、この場面の分かれ目です。
Arend では、道について場合分けすれば済みました。Cubical Agda では、区間変数を導入して正方形を直接記述します。
３行目 ── 面条件と底面の指定
＜Cubical Agda のコード＞
hfill (λ _ → λ { (i = i0) → x ; (i = i1) → y }) (inS (p i)) (~ j)
３つの部分に分けて読みます。
hfill (λ _ → λ { (i = i0) → x ; (i = i1) → y }) (inS (p i)) (~ j)
+---------------------------------------+ +---------+ +---+
第１引数：面条件 底面 向き
第１引数 ── 面条件
＜Cubical Agda のコード＞
λ _ → λ { (i = i0) → x ; (i = i1) → y }
内側の λ { ... } が、面条件です。
| 記述 | 意味 |
|---|---|
(i = i0) → x |
横方向の変数 i が左端のとき、値は x
|
(i = i1) → y |
横方向の変数 i が右端のとき、値は y
|
図で示すとこうなります。
p
a ─────────── b
│ │
x │ ？ │ y ← ここを指定している
│ │
a ─────────── b
compPath p refl
(i = i0) → x 左辺
(i = i1) → y 右辺
タロウくん：
・・・正方形の左辺と右辺を、自分で書いている。
専任講師：
それが面条件です。
Arend では、処理系が場合分けから埋めてくれた部分です。
タロウくん：
外側の λ _ → は？
専任講師：
充填を進める方向の変数を受け取る部分です。
ここでは使わないので _ で受け流しています。
第２引数 ── 底面
＜Cubical Agda のコード＞
inS (p i)
p i は、道 p の位置 i における値です。
Arend でいえば p @ i にあたります。
タロウくん：
inS というのは？
専任講師：
底面として渡すための操作です。
図でいうと、ここです。
p
a ─────────── b
│ │
x │ │ y
│ │
a ─────────── b ← 底面。inS (p i) が指定する
compPath p refl
第３引数 ── 向き
＜Cubical Agda のコード＞
(~ j)
~ は、区間の反転演算です。
j の値 |
~ j の値 |
|---|---|
i0 |
i1 |
i1 |
i0 |
縦方向を、逆向きに辿っています。
タロウくん：
なぜ、逆向きにするのですか。
専任講師：
hfill が埋める向きと、示したい主張の向きが逆だからです。
hfill の第３引数が i0 のとき底面、i1 のとき蓋になります。
一方、示したい主張は compPath p refl ≡ p です。j が i0 のとき compPath p refl、i1 のとき p でなければなりません。
そこで、~ で向きを反転させています。
hfill とは何か
タロウくん：
そもそも hfill は、何をする操作ですか。
専任講師：
Agda 公式ドキュメントが、こう述べています。
（原文引用）
When i is i0 this is u0 and when i is i1 this is hcomp u u0. This can hence be seen as giving us the interior of an open box.
（筆者による日本語訳）
iがi0のときこれはu0であり、iがi1のときこれはhcomp u u0である。したがってこれは、開いた箱の内部を与えるものと見ることができる。
出典：Cubical — Agda Documentation
タロウくん：
「開いた箱の内部」・・・。
専任講師：
蓋のない箱を思い浮かべてください。
側面と底が決まっている。そこから、内部を埋めていく操作です。
？ ← 蓋（まだない）
┌───┐
x │ │ y ← 側面（面条件で指定）
└───┘
↑
底面（inS で指定）
タロウくん：
・・・側面と底を指定して、中を埋める。
専任講師：
hfill は、その途中経過も扱えます。
hcomp は、埋め終わった結果の蓋にあたります。
両言語を並べます
＜Arend のコード＞
\func concat-idp {A : \Type} {a b : A} (p : a = b) : concat p idp = p => idp
＜Cubical Agda のコード＞
compPathRefl : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → compPath p refl ≡ p
compPathRefl {x = x} {y = y} p j i =
hfill (λ _ → λ { (i = i0) → x ; (i = i1) → y }) (inS (p i)) (~ j)
| Arend | Cubical Agda | |
|---|---|---|
| 区間変数 | 導入しない |
i と j の２つを導入 |
| 面条件 | 書かない | 左辺と右辺を明示 |
| 底面 | 書かない |
inS (p i) で指定 |
| 向き | 書かない |
~ j で指定 |
| 本体 | idp の一語 |
hfill の呼び出し |
タロウくん：
・・・Arend では、証明の中身が一語だけ。
専任講師：
定義に従って計算すれば、同じ形になるからです。
Cubical Agda では、正方形の各辺と底面と向きを、証明を書く側が並べます。
タロウくん：
記述量が、はっきり違いますね。
専任講師：
そして、これは最も単純な主張です。
先ほど Arend で書いた結合律は、さらに複雑な図形を扱います。
この作業は、繰り返し必要になります
専任講師：
こうした定型的な作業が、何度も出てきます。
（原文引用）
We have curated a small benchmarking suite of boundary problems, many of which are from the agda/cubical library. The problems are common proof obligations, such as associativity of path concatenation, rearrangements of sides of cubes, etc.
（筆者による日本語訳）
我々は、境界問題からなる小規模なベンチマーク集を整備した。その多くは agda/cubical ライブラリから採ったものである。これらの問題は、道の結合の結合律や、立方体の面の並べ替えといった、よくある証明義務である。
出典：Maximilian Doré, Evan Cavallo, Anders Mörtberg, "Automating Boundary Filling in Cubical Type Theories", arXiv:2402.12169
タロウくん：
「よくある証明義務」・・・。
専任講師：
そして、この作業が煩雑なため、専用のソルバーが研究として開発されています。
タロウくん：
・・・自動化しようとするほど、手間がかかる。
専任講師：
紙の数学では省略されやすい境界の整合性を、Cubical Agda では明示的な項として与える場面があるのです。
場面２のまとめ
| Arend | Cubical Agda | |
|---|---|---|
| 証明の方法 | 道について場合分け | 正方形を直接記述 |
| 区間変数 | 不要 | ２つ導入 |
| 面条件 | 不要 | 各辺を明示 |
| 記述量 | 本体は１行 | ３行 |
タロウくん：
・・・この場面では、記述量がはっきり増えるのですね。
専任講師：
そのとおりです。
場面３ ── J 規則を自分で組み立てる
専任講師：
最後の場面３では、等しさについて場合分けしたい場面を取り上げます。コードはこちらです。
＜Arend のコード＞
\func sym {A : \Type} {a b : A} (p : a = b) : b = a \elim p
| idp => idp
\func subst {A : \Type} (B : A -> \Type) {x y : A} (p : x = y) (b : B x) : B y \elim p
| idp => b
\func J {A : \Type} {x : A} (P : \Pi (y : A) -> x = y -> \Type)
(d : P x idp) {y : A} (p : x = y) : P y p \elim y, p
| _, idp => d
＜Cubical Agda のコード＞
J : ∀ {ℓ} {A : Set ℓ} {x : A} (P : ∀ y → x ≡ y → Set ℓ)
(d : P x refl) {y : A} (p : x ≡ y) → P y p
J P d p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d
タロウくん：
Arend のほうは、どれも | idp => の１行ですね。
Cubical Agda のほうは、右辺がまったく違います。
専任講師：
まずは Arend のコード解説から始めます。
その後で、Cubical Agda のコード解説に移ります。
Arend のコード解説
この場面で新しく出てくる記号
場面１・場面２で説明した記号に加えて、次のものが出てきます。
| Arend | 意味 |
|---|---|
\Pi (y : A) -> ... |
依存関数の型。引数の値によって返り値の型が変わる |
\elim y, p |
２つの引数について同時に場合分けする |
_ |
場合分けの中で、値を使わないときの受け皿 |
A -> \Type |
A の値を受け取って、型を返す関数 |
１つ目 ── 対称性
＜Arend のコード＞
\func sym {A : \Type} {a b : A} (p : a = b) : b = a \elim p
| idp => idp
型の部分を、順に読みます。
| 部分 | 意味 |
|---|---|
{A : \Type} |
型 A を暗黙に受け取る |
{a b : A} |
A の値を２つ、暗黙に受け取る |
(p : a = b) |
a から b への道 |
: b = a |
返すのは、b から a への道 |
タロウくん：
・・・向きを逆にする関数ですね。
専任講師：
「$a$ と $b$ が等しいなら、$b$ と $a$ も等しい」 ということです。
本体の | idp => idp を読み解きます。
\elim p が、道 p について場合分けしています。p が idp の場合、a と b は同じものになります。
タロウくん：
そのとき、b = a は a = a と同じ。
専任講師：
だから idp を返せばよいのです。
動かしてみましょう。
＜Arend のコード＞
\data Bool | true | false
\func p1 : true = {Bool} true => idp
\func chk1 : sym p1 = idp => idp
型検査を通過します。
２つ目 ── 代入
＜Arend のコード＞
\func subst {A : \Type} (B : A -> \Type) {x y : A} (p : x = y) (b : B x) : B y \elim p
| idp => b
型の部分を、順に読みます。
| 部分 | 意味 |
|---|---|
(B : A -> \Type) |
A の値を受け取って型を返す関数 |
{x y : A} |
A の値を２つ、暗黙に受け取る |
(p : x = y) |
x から y への道 |
(b : B x) |
B x という型の値 |
: B y |
返すのは、B y という型の値 |
タロウくん：
B : A -> \Type が、まだ分かりません。
専任講師：
「値を受け取って、型を返す関数」です。
実例を作ってみましょう。
＜Arend のコード＞
\func Pred (b : Bool) : \Set0 \elim b
| true => Nat
| false => Bool
Pred true は Nat、Pred false は Bool になります。
タロウくん：
・・・引数の値によって、返る型が変わる。
専任講師：
Haskell には、この形に対応するものがありません。
タロウくん：
それで、subst は何をするのですか。
専任講師：
「$x$ と $y$ が等しいなら、$B x$ の値を $B y$ へ運べる」 ということです。
動かしてみましょう。
＜Arend のコード＞
\func chk2 : subst Pred p1 5 = 5 => idp
＜Arend の型検査結果＞
$ java -jar Arend.jar S3X.ard
--- Typechecking \default ---
[ ] src.S3X
--- Done (144ms) ---
p1 は true = true の道です。Pred true は Nat ですから、5 を渡せます。
そして運んだ結果も 5 になりました。
タロウくん：
・・・| idp => b の１行で、これができる。
３つ目 ── J そのもの
＜Arend のコード＞
\func J {A : \Type} {x : A} (P : \Pi (y : A) -> x = y -> \Type)
(d : P x idp) {y : A} (p : x = y) : P y p \elim y, p
| _, idp => d
タロウくん：
\Pi というのが出てきました。
専任講師：
依存関数の型を作る記号です。
\Pi (y : A) -> x = y -> \Type は、**「A の値 y と、x から y への道を受け取って、型を返す関数」**を表します。
タロウくん：
・・・subst の B より、受け取るものが多いですね。
専任講師：
道そのものも受け取っています。
subst では、B が受け取るのは値だけでした。J では、道も受け取ります。
そのぶん、J のほうが強力です。
型の部分を、順に読みます。
| 部分 | 意味 |
|---|---|
(P : \Pi (y : A) -> x = y -> \Type) |
値と道を受け取って、型を返す関数 |
(d : P x idp) |
x と idp を渡したときの値 |
(p : x = y) |
x から y への道 |
: P y p |
返すのは、y と p を渡したときの値 |
タロウくん：
\elim y, p は、２つを同時に場合分けしているのですね。
専任講師：
そうです。そして本体は | _, idp => d の１行です。
p が idp のとき、y は x と同じものになります。そのため y の値は使わず、_ で受け流しています。
タロウくん：
・・・d をそのまま返している。
専任講師：
p が idp なら、求める P y p は P x idp と同じです。
d は、まさにその型の値でした。
J は、計算されます
専任講師：
J を idp に適用すると、その場で計算されます。
＜Arend のコード＞
\func J-computes {A : \Type} {x : A} (P : \Pi (y : A) -> x = y -> \Type) (d : P x idp)
: J P d idp = d => idp
＜Arend の型検査結果＞
$ java -jar Arend.jar S3A.ard
--- Typechecking \default ---
[ ] src.S3A
--- Done (175ms) ---
タロウくん：
J P d idp = d が idp で示せた。
専任講師：
定義に従って計算すると、d になるからです。
| _, idp => d という定義が、そのまま働いています。
タロウくん：
・・・当たり前のことのようですが。
専任講師：
この当たり前が、Cubical Agda では成り立ちません。
そこが、この場面の要点です。
Arend 側をまとめます
| 関数 | 本体 |
|---|---|
sym |
１行（| idp => idp） |
subst |
１行（| idp => b） |
J |
１行（| _, idp => d） |
J-computes |
idp の一語 |
どれも、道について場合分けするだけです。
なぜ場合分けだけで済むのか。等しさの型には idp という構成子しかないからです。
Cubical Agda のコード解説
専任講師：
では、Cubical Agda に移ります。
先ほどと同じく、筆者の執筆環境には Cubical Agda を用意できませんでした。以下は Agda 公式ドキュメントの記載に基づく説明です。
まず、決定的な違いを述べます
Cubical Agda の道の型では、refl へのパターン照合による場合分けができません。
タロウくん：
Arend では、| idp => と書くだけでした。
専任講師：
Cubical Agda では、その書き方が許されていません。
Agda の課題管理システムに、機能要望が立っています。
（原文引用）
It would be very nice to have cubical Agda to internally translate pattern matching on refl (with --without-K) to path induction. This would not only make proofs more readable, but also would allow existing Agda developments to migrate seamlessly to cubical Agda.
Because my codebase has 30k lines, it is not an option to just manually convert all uses of pattern matching on refl to uses of J.
（筆者による日本語訳）
cubical Agda が、
reflについてのパターン照合を内部的に道の帰納法へ翻訳してくれると、非常にありがたい。そうなれば証明が読みやすくなるだけでなく、既存の Agda の開発を cubical Agda へ滑らかに移行できるようにもなる。私のコード資産は３万行あるため、
reflについてのパターン照合をすべて手作業でJの使用へ変換するというのは、選択肢になりえない。
出典：Feature request: pattern matching on identity path in cubical Agda, agda/agda Issue #3551, 2019年2月8日
タロウくん：
「３万行あるため、手作業での変換は選択肢になりえない」・・・。
専任講師：
移行の障壁になっているということです。
タロウくん：
この要望は、もう反映されたのですか。
専任講師：
2026年8月末の時点でも、Open のままです。
そして、マイルストーンが icebox に設定されています。
タロウくん：
icebox というのは。
専任講師：
GitHub で、課題をグループにまとめる仕組みです。「次のリリースで対応するもの」といった単位で使われます。
icebox は Agda の開発チームが独自に付けた名前で、期日は設定されていません。
タロウくん：
・・・いつ対応するかは決まっていない。
専任講師：
そう読めます。ただし、Agda 開発チームがこの区分をどういう基準で使っているかまでは、筆者は確認していません。
事実として言えるのは、2019年に立てられた課題が2026年8月末の時点でも Open のままである、という点です。
では、どう記述するのか
専任講師：
J を、自分で組み立てることになります。
公式ドキュメントに、その定義が載っています。
＜Cubical Agda のコード＞
J : ∀ {ℓ} {A : Set ℓ} {x : A} (P : ∀ y → x ≡ y → Set ℓ)
(d : P x refl) {y : A} (p : x ≡ y) → P y p
J P d p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d
出典：Cubical — Agda Documentation
この場面で新しく出てくる記号
| Cubical Agda | 意味 | Arend でいえば |
|---|---|---|
∀ y → ... |
依存関数の型 | \Pi (y : A) -> ... |
transport |
道に沿って値を運ぶ | coe |
p i |
道 p の位置 i における値 |
p @ i |
i ∧ j |
区間の最小演算 | ── |
１行目・２行目 ── 型の宣言
＜Cubical Agda のコード＞
J : ∀ {ℓ} {A : Set ℓ} {x : A} (P : ∀ y → x ≡ y → Set ℓ)
(d : P x refl) {y : A} (p : x ≡ y) → P y p
＜Arend で書けば＞
\func J {A : \Type} {x : A} (P : \Pi (y : A) -> x = y -> \Type)
(d : P x idp) {y : A} (p : x = y) : P y p
並べて比較します。
| Cubical Agda | Arend | 意味 |
|---|---|---|
∀ {ℓ} |
── | 宇宙のレベルを受け取る |
{A : Set ℓ} |
{A : \Type} |
型 A を暗黙に受け取る |
(P : ∀ y → x ≡ y → Set ℓ) |
(P : \Pi (y : A) -> x = y -> \Type) |
値と道を受け取って型を返す関数 |
(d : P x refl) |
(d : P x idp) |
基点での値 |
(p : x ≡ y) |
(p : x = y) |
x から y への道 |
→ P y p |
: P y p |
返り値の型 |
タロウくん：
・・・型の部分は、ほぼ同じですね。
専任講師：
問題は、３行目です。
３行目 ── 本体
＜Cubical Agda のコード＞
J P d p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d
＜Arend で書けば＞
\elim y, p
| _, idp => d
タロウくん：
・・・まったく違いますね。
専任講師：
３つの部分に分けて読みます。
transport (λ i → P (p i) (λ j → p (i ∧ j))) d
└─運ぶ操作┘ └────── 道の指定 ──────┘ └出発点┘
transport とは何か
専任講師：
道に沿って、値を運ぶ操作です。
Arend の coe にあたります。
タロウくん：
場面１の説明で出てきた、あの操作ですね。
専任講師：
型 $X$ と型 $Y$ が等しいと示せたとき、$X$ の値を $Y$ へ持っていく。
ここでは、P x refl の値である d を、P y p へ運んでいます。
道の指定 ── 外側の λ i →
＜Cubical Agda のコード＞
λ i → P (p i) (λ j → p (i ∧ j))
i が、区間変数です。
i を左端から右端へ動かすと、P x refl から P y p へ移り変わっていきます。
タロウくん：
P (p i) の p i は。
専任講師：
道 p の位置 i における値です。
Arend の p @ i にあたります。
i の値 |
p i の値 |
|---|---|
i0 |
x |
i1 |
y |
タロウくん：
・・・i を動かすと、x から y へ移る。
道の指定 ── 内側の λ j →
専任講師：
ここが、この場面で最も込み入った部分です。
＜Cubical Agda のコード＞
λ j → p (i ∧ j)
タロウくん：
また区間変数が出てきました。今度は j ですね。
専任講師：
P の第２引数を作っています。
P の型を思い出してください。
＜Cubical Agda のコード＞
P : ∀ y → x ≡ y → Set ℓ
第１引数は値、第２引数は「x からその値への道」です。
タロウくん：
第１引数に p i を渡したのだから、第２引数は「x から p i への道」・・・。
専任講師：
そのとおりです。そして、それを作らなければなりません。
タロウくん：
p そのものではだめなのですか。
専任講師：
p は x から y への道です。x から p i への道ではありません。
必要なのは、p を途中で切り取った道です。
i ∧ j が、切り取りを行います
専任講師：
∧ は、区間の最小演算です。
i と j のうち、小さいほうを取ります。
タロウくん：
・・・それで、どう切り取れるのですか。
専任講師：
j を左端から右端へ動かしてみてください。
j の値 |
i ∧ j の値 |
p (i ∧ j) |
|---|---|---|
i0（左端） |
i0 |
x |
i1（右端） |
i |
p i |
j が左端のとき x、右端のとき p i。
タロウくん：
・・・x から p i への道になっている。
専任講師：
それが λ j → p (i ∧ j) の中身です。
図で示すと、こうなります。
p
x ------------> y
| |
+--------+
λ j → p (i ∧ j)
x から p i までの部分
i = i0 のとき --- 一点 x
i = i1 のとき --- p 全体
タロウくん：
・・・i の位置に応じて、切り取る長さが変わる。
専任講師：
それが ∧ の働きです。
ド・モルガン代数について
タロウくん：
先生、∧ という記号が使えるのは、なぜですか。
専任講師：
Cubical Agda の区間には、代数の構造が備わっているからです。
| 演算 | 意味 |
|---|---|
∧ |
最小 |
∨ |
最大 |
~ |
反転 |
この構造を、ド・モルガン代数といいます。
タロウくん：
Arend には、これがないのですね。
専任講師：
Arend の区間には、これらの演算がありません。
代わりに squeeze と squeezeR という補助関数が用意されています。
タロウくん：
・・・同じ「区間」でも、備わっているものが違う。
専任講師：
そのため、記述の仕方も変わってきます。
J の計算規則が、成り立ちません
専任講師：
もう１つ、重要な違いがあります。
Arend では、J を idp に適用すると、その場で計算されました。
＜Arend のコード＞
\func J-computes {A : \Type} {x : A} (P : \Pi (y : A) -> x = y -> \Type) (d : P x idp)
: J P d idp = d => idp
型検査を通過します。
Cubical Agda では、そうなりません。
（原文引用）
One subtle difference between paths and the propositional equality type of Agda is that the computation rule for J does not hold definitionally. If J is defined using pattern-matching as in the Agda standard library then this holds, however as the path types are not inductively defined this does not hold for the above definition of J.
（筆者による日本語訳）
道の型と、Agda の命題的等値型とのあいだにある微妙な違いの１つは、
Jの計算規則が定義的には成り立たないことである。Agda の標準ライブラリのようにパターン照合を用いてJを定義すればこれは成り立つが、道の型は帰納的に定義されていないため、上で挙げたJの定義については成り立たない。
出典：Cubical — Agda Documentation
タロウくん：
「道の型は帰納的に定義されていないため」・・・。
専任講師：
場合分けができない理由と、同じところに行き着きます。
タロウくん：
では、どうするのですか。
専任講師：
別の型を導入して解決しています。
（原文引用）
As mentioned above the computation rule for J does not hold definitionally for path types. Cubical Agda solves this by introducing a cubical identity type.
（筆者による日本語訳）
前述のとおり、
Jの計算規則は、道の型については定義的には成り立たない。Cubical Agda は、立方体的な同一視型を導入することでこれを解決している。
出典：同上
タロウくん：
「立方体的な同一視型」というのは。
専任講師：
等しさを表す型が、もう１種類あるということです。
| 型 | 特徴 |
|---|---|
道の型（≡） |
記法が扱いやすい。多くの定義的等値が成り立つ |
| 立方体的な同一視型 |
J が refl について計算される |
用途に応じて、使い分けることになります。
タロウくん：
・・・２種類を使い分ける。
専任講師：
Arend では、そういう使い分けがありません。
両言語を並べます
＜Arend のコード＞
\func J {A : \Type} {x : A} (P : \Pi (y : A) -> x = y -> \Type)
(d : P x idp) {y : A} (p : x = y) : P y p \elim y, p
| _, idp => d
＜Cubical Agda のコード＞
J : ∀ {ℓ} {A : Set ℓ} {x : A} (P : ∀ y → x ≡ y → Set ℓ)
(d : P x refl) {y : A} (p : x ≡ y) → P y p
J P d p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d
| Arend | Cubical Agda | |
|---|---|---|
| 道の場合分け | \elim y, p でできる |
できない |
| 本体 | | _, idp => d の１行 |
transport を組み立てる |
| 区間変数 | 導入しない |
i と j の２つを導入 |
| 区間の演算 | 使わない |
∧ を使う |
J の計算規則 |
成り立つ | 道の型では成り立たない |
| 等しさの型 | １種類 | ２種類を使い分ける |
タロウくん：
・・・すべての行で、Arend のほうが短い。
専任講師：
Arend では、場合分けの１行で済みます。
Cubical Agda では、区間変数を導入し、道を切り取り、それを transport に渡す。 その組み立てを、証明を書く側が行います。
既存のコードを移行するときの負担
専任講師：
そして、この違いは移行の負担にもなります。
先ほどの Issue #3551 で、**「３万行のコード資産について、手作業での変換は選択肢になりえない」**と述べられていたとおりです。
タロウくん：
・・・| idp => を、すべて J の呼び出しに書き換える。
専任講師：
それが、実務上の障壁になっています。
場面３のまとめ
| Arend | Cubical Agda | |
|---|---|---|
| 道の場合分け | できる | できない |
J の記述 |
場合分けで定義 |
transport で組み立て |
J の計算規則 |
成り立つ | 道の型では成り立たない |
| 記述量 | １行 | 引数の組み立てが必要 |
タロウくん：
・・・この場面でも、記述量が増えるのですね。
専任講師：
そして、判断の手間も増えます。
道の型と立方体的な同一視型。どちらを使うかを、選ばなければなりません。
３つの場面をまとめると
| 場面 | 確認作業の中身 | 記述量 |
|---|---|---|
| １. 区間を型の材料にできない | この位置に区間を書いてよいかを判断する | 増えない（判断の手間が増える） |
| ２. 面条件を書き並べる | どの面がどの値で埋まっているかを指定する | 増える（面の数だけ行が増える） |
| ３. 道の場合分けができない |
J の引数を自分で組み立てる |
増える（引数の指定が要る） |
タロウくん：
・・・２と３は、書く量そのものが増えるのですね。
専任講師：
そうです。そして１は、書く量ではなく、判断の負担です。
タロウくん：
どちらも、Arend では生じない負担。
専任講師：
その代わり、Arend は正準性を持ちません。
タロウくん：
・・・そこが、トレードオフですね。
Arend 公式論文は、こうした体系を two-level theories と呼んでいます。
（原文引用）
More advanced, fully computational cubical type theories have since evolved, in which univalence is derivable. However, these approaches are considerably more complex, featuring two-level theories where the interval
Iis not a type.
（筆者による日本語訳）
より進んだ、完全に計算可能な立方体型理論はその後発展し、そこでは一価性が導出可能である。しかしこれらの手法はかなり複雑で、区間
Iが型ではない two-level theories を特徴とする。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
本記事では、two-level theory を「二層理論」と仮に訳します。 訳語を選んだ根拠は、本節の末尾に記しました。
さらに、$I$ が普通の型でなくなったことで、$I$ に対してできることが減ります。
とりわけ、$I$ を通常の型構成に組み込むことができません。
たとえば、$f : \mathbb{N} \to \mathbb{I}$ のような関数を持つことはできません。
（原文引用）
There are multiple reasons for this distinction. One is that the interval should not participate in any type formers, so for example we cannot have functions $f: \mathbb{N} \to \mathbb{I}$ which easily make type-checking undecidable.
（筆者による日本語訳）
この区別には、複数の理由がある。１つは、区間が型構成子に一切関与すべきでないということである。たとえば $f : \mathbb{N} \to \mathbb{I}$ のような関数を持つことはできない。そうした関数は、型検査を容易に決定不能にしてしまう。
出典："Normal forms in cubical type theory", arXiv:2603.24923
この制約は、証明を書く人の負担として現れます。
なお、区間の値による場合分けが禁じられている点は、Arend でも Cubical Agda でも共通です。 両者の違いではありません。この点については、本記事の場面１であらためて扱います。
引き受けた複雑さは、作業量として現れます
Cubical Agda では、道と道のあいだの関係を示すときに、立方体の面を埋める作業が繰り返し必要になります。
どういう作業なのかを説明します。
道が２本あるとします。$a$ から $b$ への道と、$b$ から $c$ への道です。この２本をつなげば、$a$ から $c$ への道が得られます。
では、道が３本ある場合はどうでしょうか。
$a \to b$、$b \to c$、$c \to d$。つなぐ順序が２通りあります。
前の２本を先につないでから３本目をつなぐ。あるいは、後ろの２本を先につないでから１本目をつなぐ。
どちらでも同じ結果になる。 これが、道の結合における結合律です。
Cubical Agda では、この主張を証明するために、正方形の面を埋めます。
４辺のうち３辺が決まっていて、残りの１辺を埋める。その作業を、hcomp で行います。
そして、こうした定型的な作業が、何度も出てきます。
この作業が煩雑なため、専用のソルバーが研究として開発されているほどです。
（原文引用）
We have curated a small benchmarking suite of boundary problems, many of which are from the agda/cubical library. The problems are common proof obligations, such as associativity of path concatenation, rearrangements of sides of cubes, etc.
（筆者による日本語訳）
我々は、境界問題からなる小規模なベンチマーク集を整備した。その多くは agda/cubical ライブラリから採ったものである。これらの問題は、道の結合の結合律や、立方体の面の並べ替えといった、よくある証明義務である。
「よくある証明義務」と述べられています。
紙の数学では省略されやすい境界の整合性を、Cubical Agda では明示的な項として与える場面があるのです。
なお、本記事の執筆環境では Cubical Agda を実行できなかったため、Cubical Agda のコード例は掲載していません。 上記は、公式ドキュメントおよび査読論文の記載に基づくものです。
どちらの定理証明言語が正しいという話ではありません
Arend は、理論の単純さを取りました。
Cubical Agda は、証明を最後まで走らせる力を取りました。
そして、それぞれ別のものを諦めています。
もっとも、この負担は固定されたものではありません。 ライブラリ、補助記法、境界充填の自動化が発達すれば、利用者が直接負う負担は変わりえます。
先ほど触れた専用ソルバーの研究も、その方向の試みです。
定理証明言語の設計とは、そういうものです。
なお、HoTT がどこから生まれたのかについては、次回の記事で扱います。 2006年に、専門も所属も異なる２組の研究者が、独立に同じ着想へ至りました。
以下では、論点①と②についても、あらかじめ触れておきます。
論点① ── 等しさの根拠を識別して扱えると、何ができるのか
HoTT は、等しさの根拠を「値」として扱います。
値として扱うとは、変数に入れたり、関数に渡したりできる、という意味です。
そこから、３つのことができるようになります。
第１に、ある型について書いた証明を、別の型へ運べます。
２つの型が等しいと示せたとき、一方について証明したことを、他方へ持ち込めます。 同じ証明を２度書かずに済みます。
第２に、「これとこれは同じ数だ」という取り決めを、型の定義に書き込めます。
$1/2$ と $2/4$ は、書き方が違うだけで同じ数です。その取り決めを、プログラムの型として表現できます。
第３に、「どんな入力にも同じ値を返す２つの関数は、等しい」と言えるようになります。
素のマーティン＝レーフ型理論では、この主張を証明できません。
論点② ── HoTT の主張を「そういうものだ」で済ませると、何が起きるのか
この３つを、定理証明言語にどう組み込むか。
Rocq の HoTT ライブラリや、通常の Agda に HoTT の公理を追加したものは、「そういうものだ」と宣言して済ませました。
証明は書けます。しかし、その証明を実際に走らせても、途中で止まって具体的な値が出てきません。
Arend と Cubical Agda は、計算の規則そのものを言語に組み込みました。
その組み込み方の違いが、論点③で述べた分岐につながります。
訳語について ── two-level theory を「二層理論」と訳す根拠
まず、注意を述べます。
ここでの「二層」は、Cubical Agda において通常の型の宇宙と区間専用の特別なソートが区別される、という本記事の説明上の呼び方です。
文献でいう two-level type theory（2LTT）は、内側・外側の型理論や複数の等号を含む、より特定の理論体系を指すことがあります。本記事では両者を完全に同一視しません。
そのうえで、訳語の判断根拠を記します。
two-level theory について、日本語の数学用語・計算機科学用語として定まった訳語は存在しません。
筆者が調べた範囲では、確立された訳語を確認できませんでした。そこで本記事では、仮置きで「二層理論」と訳します。
「二水準理論」ではなく「二層理論」を選んだ根拠を、３点記します。
根拠① ── 原語の構造に近い
2LTT は、内側と外側という２つの型理論を重ねたものです。
Annenkov らの論文は、次のように定義しています。
（原文引用）
We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the inner and the outer type theory.
（筆者による日本語訳）
我々は、two-level type theory（2LTT）を定義し、展開する。これは、２つの異なる型理論を組み合わせたマーティン＝レーフ型理論の一種である。我々はそれらを、内側の型理論と外側の型理論と呼ぶ。
内と外に重なっている構造です。
「層」は、重なりを表す語です。 一方「水準」は、高低や程度を表します。
重なりを表すなら、「層」が適します。
根拠② ── 本記事の説明と噛み合う
本記事では、次のように説明しました。
「型の置き場所が２つに分かれ、その２つを行き来する規則が必要になる」
「行き来する」のは、層のあいだです。
「２つの水準を行き来する」では、日本語として不自然になります。
根拠③ ── 既存の用語との衝突を避けられる
HoTT には、すでに「ホモトピーレベル」という語があります。
上村太一氏の日本語版教科書でも、「ホモトピーレベル」と片仮名で訳されています。
「二水準理論」とすると、読者が「ホモトピーレベルの話か」と誤解する恐れがあります。
「層」であれば、別の概念だと分かります。
注記
「層」は layer の訳語でもあります。 そのため本記事では、原語を必ず併記します。
本記事では説明の便宜上、通常の型が置かれる側と、区間専用の特別なソートが置かれる側を「２つの層」と呼びます。
ただし、この区別だけが文献上の two-level type theory（2LTT）を定義するわけではありません。
なお、数学における層（sheaf）とは無関係です。
３つの体系を、並べて振り返ります
専任講師：
ここまで、３つの場面を見てきました。最後に、全体を整理しておきましょう。
タロウくん：
お願いします。
専任講師：
本記事では、HoTT を扱う３つの方式を取り上げました。
| 方式 | 代表例 |
|---|---|
| HoTT を公理としてだけ受け取る | Rocq の HoTT ライブラリ |
| HoTT の計算規則を持ち、区間を普通の型として扱う | Arend |
| HoTT の計算規則を持ち、区間を普通の型とは別に置く | Cubical Agda |
計算がどこまで進むか
専任講師：
証明を走らせたとき、どこまで計算が進むか。その順に並べます。
タロウくん：
Rocq の HoTT ライブラリが、最も早く止まるのでしたね。
専任講師：
一価性公理を、証明せずに「正しいものとする」と宣言しているだけだからです。
正しいと宣言しただけで、それを使った式をどう計算するかは、何も定めていません。
タロウくん：
・・・計算の手順がないから、そこで止まる。
専任講師：
Arend では、計算規則を備えています。
iso で等しさの根拠を作り、coe でその根拠に沿って値を運ぶ。その手順が、体系のなかに定められています。
＜Arend のコード＞
\func movedNeg : Bool => coe (\lam i => negPath @ i) true right
\func check2 : movedNeg = false => idp
型検査を通過します。true を運んだ結果が false になりました。
タロウくん：
Rocq では、ここで止まってしまう。
専任講師：
そのとおりです。しかし Arend にも限界があります。
区間 I を普通の型として扱っているため、区間変数を含んだままの式では、計算が止まります。
タロウくん：
・・・それが、記事の前半で見た例ですね。
専任講師：
Cubical Agda は、そこをさらに先へ進めます。
区間を普通の型とは別の場所に置いたことで、普通の型についての２つの操作を保証しているからです。
３つを並べると
本記事で見てきた HoTT 的構成について、計算がどこまで進むかを並べます。
| 方式 | HoTT の扱い | この比較で見ている計算 |
|---|---|---|
| Rocq の HoTT ライブラリ | 公理として受け取る | 公理を使ったところで、定義的な計算は進まない |
| Arend | 計算規則を持つ。区間は普通の型 | 一部の HoTT 的構成を計算できる |
| Cubical Agda | 計算規則を持つ。区間は別の場所 | より広い範囲を計算的に扱える |
あらゆる計算について、この順で強いという意味ではありません。
タロウくん：
・・・左から右へ、計算が先まで進む。
プログラマの負担は、逆順になります
専任講師：
そして、本記事で取り上げた３つの場面だけを見ると、負担の大きさは逆になります。
| 方式 | ３つの場面での負担 |
|---|---|
| Rocq の HoTT ライブラリ | 最も小さい |
| Arend | 中間 |
| Cubical Agda | 最も大きい |
言語全体としての負担を比べたものではありません。
タロウくん：
３つの場面で見たとおりですね。
専任講師：
場面ごとに、もう一度整理します。
| 場面 | Arend | Cubical Agda |
|---|---|---|
| １. 区間を型構成子に渡す | 記述できる | 記述できない |
| ２. 道と道の関係を証明する | 本体は１行 | 面条件・底面・向きを指定 |
| ３. 等しさについて場合分けする | 本体は１行 |
J を組み立てる |
タロウくん：
・・・どの場面でも、Arend のほうが短い。
専任講師：
その代わり、Arend は正準性を持ちません。
タロウくん：
先生、「正準性」という言葉が、まだ分かりません。
専任講師：
まだ説明していませんでしたね。ここで解説します。
正準性とは、閉じた項が必ず正準形へ評価されるという性質です。
タロウくん：
・・・「閉じた項」「正準形」。どちらも分かりません。
専任講師：
順に説明します。
「閉じた項」とは何か
専任講師：
自由な変数を含まない式のことです。
| 式 | 閉じているか |
|---|---|
n + 3 |
閉じていない（変数 n を含む） |
2 + 3 |
閉じている |
タロウくん：
外から値を渡してもらう必要がない式、ということですね。
専任講師：
そのとおりです。
「正準形」とは何か
専任講師：
その型の値として、最も基本的な形のことです。
自然数でいえば、zero と「１を足す」だけで作られた形です。
0 → zero
1 → suc zero
2 → suc (suc zero)
タロウくん：
2 + 3 を計算すると 5 になる。その 5 が正準形ですか。
専任講師：
そうです。suc (suc (suc (suc (suc zero)))) という形です。
正準性とは
専任講師：
閉じた項は、必ず正準形へたどり着く。それが正準性です。
自然数について正確に述べると、こうなります。
「自然数の型に属する閉じた項は、すべて zero と「１を足す」だけを使って構成されたものと同一である」
タロウくん：
・・・計算すれば、必ず具体的な数になる。
専任講師：
Arend は、この性質を持ちません。
開発者自身が、公開時にこう答えています。
（原文引用）
Does Arend have the canonicity property, i.e. does it evaluate closed expressions to their canonical forms? No, but it computes more terms than ordinary homotopy type theory, which makes it more convenient in many aspects.
（筆者による日本語訳）
Arend は正準性を持つか、すなわち閉じた式を正準形へ評価するか。いいえ。しかし通常のホモトピー型理論より多くの項を計算するため、多くの面でより便利になっている。
出典：New theorem prover Arend is released, Homotopy Type Theory mailing list, 2019年8月6日
タロウくん：
「いいえ」と、はっきり答えていますね。
専任講師：
そのうえで、「通常のホモトピー型理論より多くの項を計算する」と続けています。
計算しきれるわけではない。しかし、公理として足す方式よりは進む。
タロウくん：
・・・記事の前半で見た、３つの並びですね。
専任講師：
そこに戻ってきます。
計算が進むほど、負担も増える。それが、この記事の主題でした。
Arend と Cubical Agda、どちらを採用すべきか
タロウくん：
先生、実務的な質問をさせてください。
Cubical Agda と Arend のどちらを採用すべきかの選定基準は、どう考えたらいいですか？
専任講師：
答えを先に述べます。何を優先するかによって決まります。
タロウくん：
・・・状況によって違う、ということですか。
専任講師：
そうです。整理しましょう。
Cubical Agda が向いている場面
専任講師：
面条件や J の組み立てを、プログラマが自分で記述することを厭わない。
そして、とにかく計算をできるだけ先まで進めることを最優先に掲げる。
そういう方針であれば、Cubical Agda です。
タロウくん：
手間をかけてでも、計算しきりたい場合。
専任講師：
証明した内容を、実際に走らせて値を得たい。そういう場面では、計算が進むことが決定的に重要になります。
Arend が向いている場面
専任講師：
面条件や J の組み立てを、プログラマが都度記述することは避けたい。
そして、できる範囲で計算が進めばよい。
そういう方針であれば、Arend が現実的です。
タロウくん：
・・・証明を書くこと自体が目的の場合。
専任講師：
数学の定理を形式化して、正しさを機械に確かめてもらう。
その目的であれば、証明が書きやすいことのほうが重要になります。
証明の検査と、証明の実行は別のことです
タロウくん：
ちょっとまってください。
数学の定理を形式化して、正しさを機械に確かめてもらう場合こそ、区間 I が登場する箇所で計算が止まってしまう可能性がある Arend よりも、Cubical Agda のほうが向いているのではないですか？
専任講師：
そこは、区別が必要です。
「証明を検査すること」と「証明を走らせて値を得ること」は、別のことなのです。
タロウくん：
・・・別、ですか。
専任講師：
実際に確かめてみましょう。
＜Arend のコード＞
\data Bool | true | false
\func boolNeg (b : Bool) : Bool \elim b
| true => false
| false => true
\func boolNegNeg (b : Bool) : boolNeg (boolNeg b) = b \elim b
| true => idp
| false => idp
\func negPath : Bool = Bool => path (iso boolNeg boolNeg boolNegNeg boolNegNeg)
-- 区間変数を含んだまま、道に沿って true を運ぶ
\func theorem (i : I) : negPath @ i => coe (\lam j => negPath @ j) true i
-- 定理を組み合わせることもできる
\func theorem2 : negPath @ left = negPath @ left => idp
＜Arend の型検査結果＞
$ java -jar Arend.jar PROOF.ard
--- Typechecking \default ---
[ ] src.PROOF
--- Done (178ms) ---
タロウくん：
・・・通っていますね。区間変数を含んでいるのに。
専任講師：
そうです。証明としては、何の問題もありません。
型検査が通ったということは、機械が正しさを確かめたということです。
タロウくん：
では、何が止まるのですか。
専任講師：
そこから具体的な値を取り出そうとしたときです。
＜Arend のコード＞
-- 具体的な Bool の値を求めようとする
\func getValue (i : I) : Bool => theorem i
＜Arend の型検査結果＞
[ERROR] Type mismatch
Expected type: Bool
Actual type: iso {Bool} {Bool} boolNeg boolNeg boolNegNeg boolNegNeg i
In: theorem i
タロウくん：
・・・Bool を期待したのに、iso がそのまま残っている。
専任講師：
そこが、計算の止まる場面です。
i が left か right に定まっていれば、iso は簡約されて Bool になります。しかし i が区間変数のままでは、簡約できません。
タロウくん：
では、２つを整理すると。
専任講師：
こうなります。
| やりたいこと | 何が要るか | Arend で困るか |
|---|---|---|
| 定理を形式化し、正しさを機械に確かめてもらう | 型検査が通ること | 困らない |
| 証明から具体的な値を取り出す | 計算が最後まで進むこと | 困る場面がある |
タロウくん：
・・・数学の形式化は、前者。
専任講師：
定理が正しいかどうかを確かめるだけなら、値を取り出す必要がありません。
「この命題は成り立つ」と機械が判定してくれれば、目的は達成されています。
タロウくん：
では、後者はどういう場面ですか。
専任講師：
証明した内容を、プログラムとして実行したい場面です。
記事の前半で挙げた例を思い出してください。単進数と二進数の型が等しいと示し、単進法で書いた証明を二進法へ運ぶ。
タロウくん：
証明は前者で書き、実行は後者で行う・・・。
専任講師：
そのとき、運んだ結果が具体的な値になってくれなければ困ります。
そこが、計算が最後まで進むことの意味です。
タロウくん：
・・・数学の形式化と、プログラムの実行。目的が違うのですね。
専任講師：
Arend の開発チームが「実践的な経験は、そのような強化の必要性を大きくは示していない」と述べたのも、そういう文脈です。
数学の形式化を主な用途とするなら、証明が書きやすいことのほうが効いてきます。
タロウくん：
・・・私は、そこを混同していました。
専任講師：
混同しやすいところです。
「計算が止まる」と聞くと、証明そのものが失敗するように思えます。
しかし、止まるのは値を取り出す段階です。証明の検査は、そこまで進まなくても完了します。
Arend開発チームの認識
専任講師：
Arend の開発チームも、同じ趣旨のことを述べています。
（原文引用）
The type theory of Arend could potentially be adjusted to enhance its computational aspects, but practical experiences in formalization have not demonstrated a significant need for such enhancements.
（筆者による日本語訳）
Arend の型理論は、その計算的側面を高めるように調整できる可能性がある。しかし形式化における実践的な経験は、そのような強化の必要性を大きくは示していない。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", https://arend-lang.github.io/assets/lang-paper.pdf
タロウくん：
「実際に形式化をしてみると、そこまでの計算可能性は必要なかった」・・・。
専任講師：
同じ論文には、こうも書かれています。
（原文引用）
However, these approaches are considerably more complex, featuring two-level theories where the interval I is not a type. While the development of such fully computational theories is of theoretical interest, the complexity of two-level frameworks do not currently justify their use in practical applications.
（筆者による日本語訳）
しかしこれらの手法はかなり複雑で、区間
Iが型ではない二層理論を特徴とする。そのような完全に計算可能な理論の発展は理論的な関心の対象であるが、二層の枠組みの複雑さは、現状では実用上その採用を正当化しない。
出典：同上
タロウくん：
・・・理論としての関心は認めたうえで、実用上は割に合わないと。
専任講師：
現時点での判断です。
選定基準を、表にまとめます
| 優先するもの | 選ぶべき言語 |
|---|---|
| 計算をできるだけ先まで進めたい | Cubical Agda |
| 証明を書く手間を抑えたい | Arend |
| 既存の Agda の資産を活かしたい | Agda 系（ただし移行の負担がある） |
| 理論の単純さを重視したい | Arend |
タロウくん：
・・・目的が決まれば、選ぶべきものも決まる。
ただし、負担は固定されたものではありません
専任講師：
最後に、１点お断りしておきます。
プログラマの負担は、固定されたものではありません。
タロウくん：
といいますと。
専任講師：
ライブラリ、補助記法、境界充填の自動化が発達すれば、利用者が直接負う負担は変わりえます。
場面２で触れた専用ソルバーの研究も、その方向の試みです。
タロウくん：
・・・いまの比較が、そのまま続くとは限らない。
専任講師：
そのとおりです。
どちらが正しいという話ではありません
専任講師：
Arend は、理論の単純さを取りました。
Cubical Agda は、証明を最後まで走らせる力を取りました。
そして、それぞれ別のものを諦めています。
タロウくん：
・・・何を優先したかの違い。
専任講師：
定理証明言語の設計とは、そういうものです。
タロウくん：
先生、最後にひとつだけ。
専任講師：
どうぞ。
タロウくん：
Arend の判断は、**「これまで形式化してきた範囲では困らなかった」**という経験に基づくものですよね。
今後、扱う対象が広がったときに、困る場面が出てくる可能性は。
専任講師：
あります。公式論文も「調整できる可能性がある」と述べていました。
タロウくん：
・・・確定した結論ではない。
専任講師：
現時点での判断です。
それが、設計というものです。
次回の予告
【Arend Theorem Prover 連載（３回目）】では、本記事で名前だけを挙げたものを、順に掘り下げます。
第１部 ── ホモトピー型理論は、どこから来たのか
2006年、専門も所属も異なる２組の研究者が、独立に同じ着想へ至りました。
論理学と圏論の側から進んだ Awodey と Warren。代数幾何でフィールズ賞を受賞した Voevodsky。
その出発点となった「グルーポイド解釈」から説き起こします。
第２部 ── 移送とは何か
本記事では、coe という操作を何度か使いました。
等しさの根拠に沿って、値を運ぶ操作です。
それが実際に何の役に立つのか。単進法と二進法の使い分けを例に、詳しく扱います。
第３部 ── 商型とは何か
$1/2$ と $2/4$ は、書き方こそ違いますが同じ数です。
しかし、組として書けば (1,2) と (2,4) であり、別の値になります。
「これとこれは同じものとみなす」という取り決めを、型の定義に書き込む。 その仕組みを扱います。
第４部 ── 関数外延性とは何か
どんな入力を与えても同じ値を返す。そのとき、２つの関数は等しいと言ってよいでしょうか。
数学では、言ってよいことになっています。
しかし、素のマーティン＝レーフ型理論では証明できません。 なぜそうなるのかを扱います。
第５部以降
HoTT を公理として足したときに何が起きるのか。Lean 4 での事情も含めて扱います。
そして、Arend の宇宙に付いている２つの添字についても、入門者向けに平易に解説します。
連載リンク
出典一覧
Arend
- Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
https://arend-lang.github.io/assets/lang-paper.pdf - Prelude, Arend Documentation
https://arend-lang.github.io/documentation/language-reference/prelude.html - Language Reference, Arend Documentation
https://arend-lang.github.io/documentation/language-reference/ - Tutorial, Arend Documentation
https://arend-lang.github.io/documentation/tutorial/ - New theorem prover Arend is released, Homotopy Type Theory mailing list, 2019年8月6日
https://groups.google.com/g/homotopytypetheory/c/rf6YJB5Omj0
Cubical Agda
- Cubical, Agda Documentation
https://agda.readthedocs.io/en/latest/language/cubical.html - Feature request: pattern matching on identity path in cubical Agda, agda/agda Issue #3551, 2019年2月8日
https://github.com/agda/agda/issues/3551 -
piSort/funSortofIUnivshould be blocked on the codomain, agda/agda Issue #6074
https://github.com/agda/agda/issues/6074
立方体型理論
-
"Normal forms in cubical type theory", arXiv:2603.24923
https://arxiv.org/abs/2603.24923 - Maximilian Doré, Evan Cavallo, Anders Mörtberg, "Automating Boundary Filling in Cubical Type Theories", arXiv:2402.12169
https://arxiv.org/abs/2402.12169 -
"Internalizing Representation Independence with Univalence", arXiv:2009.05547
https://arxiv.org/abs/2009.05547
二層理論（two-level type theory）
- Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler, "Two-Level Type Theory and Applications", Mathematical Structures in Computer Science, vol. 33, no. 8, 2023, pp. 688–743, doi:10.1017/S0960129523000130
https://arxiv.org/abs/1705.03307
検証環境
本記事に掲載した Arend のコードは、すべて実機で検証しました。
- Arend 1.10（Java 21）
型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。
一方、Cubical Agda については、執筆環境に処理系を用意できませんでした。
同言語に関する記述は、Agda 公式ドキュメント、Agda の課題管理システム、および査読論文の記載に基づくものです。
【発展篇】コラム ── ４つの例のうち３つを、Arend のコードで確かめる
【発展篇】コラム ── ４つの例のうち３つを、Arend のコードで確かめる
本文で挙げた４つの例のうち、３つを Arend のコードで確かめます。
第２の例である単進数と二進数は、完全な対応の証明が長くなるため、割愛します。
まず、Arend の記号を説明します。
Arend の記号 ── Haskell との対応
| Arend | 意味 | Haskell でいえば |
|---|---|---|
\data |
データ型を定義する | data |
\func |
関数や値を定義する | 関数定義（f x = ...） |
=> |
定義の本体を書き始める | = |
| |
データ型の選択肢を区切る | | |
\elim |
引数について場合分けする | case ... of |
: |
「〜の型を持つ」 | :: |
\Sigma |
組の型を作る | (,) |
Int |
整数 | Int |
Arend の公式マニュアルは、次のページにあります。
- 言語リファレンス：https://arend-lang.github.io/documentation/language-reference/
- 入門用のチュートリアル：https://arend-lang.github.io/documentation/tutorial/
例① ── 名前だけが違う型
第１段階 ── ２つの型を定義する
\data Bool | true | false
\data Answer | yes | no
Haskell で書けば、こうなります。
data Bool = True | False
data Answer = Yes | No
| Arend | Haskell | 意味 |
|---|---|---|
\data Bool |
data Bool |
Bool という型を定義する |
| true |
= True |
選択肢その１ |
| false |
| False |
選択肢その２ |
Arend では、最初の選択肢にも | を付けます。
第２段階 ── 一方から他方への関数を定義する
\func toAnswer (b : Bool) : Answer \elim b
| true => yes
| false => no
Haskell で書けば、こうなります。
toAnswer :: Bool -> Answer
toAnswer True = Yes
toAnswer False = No
一行ずつ見ます。
| 部分 | 意味 |
|---|---|
\func toAnswer |
toAnswer という関数を定義する |
(b : Bool) |
引数 b は Bool の値 |
: Answer |
返り値の型は Answer
|
\elim b |
引数 b について場合分けする |
| true => yes |
b が true のとき yes を返す |
| false => no |
b が false のとき no を返す |
\elim b が、Haskell の case b of にあたります。
逆向きの関数も、同じように定義します。
\func toBool (a : Answer) : Bool \elim a
| yes => true
| no => false
第３段階 ── 往復すると元に戻ることを示す
「一対一に対応する」を確かめるには、往復して元に戻ることを示します。
\func bool-rt1 (b : Bool) : toBool (toAnswer b) = b \elim b
| true => idp
| false => idp
型に記述されている toBool (toAnswer b) = b が、示したい主張です。
b を toAnswer で Answer に変え、toBool で Bool に戻す。それが元の b と等しい、と述べています。
idp というのが出てきました。
idp は、「両辺が計算して同じ形になる」ことを示す証拠です。
b が true のとき、左辺は次のように計算されます。
toBool (toAnswer true)
→ toBool yes
→ true
右辺も true です。同じ形になりました。 だから idp で示せます。
逆向きも同様です。
\func bool-rt2 (a : Answer) : toAnswer (toBool a) = a \elim a
| yes => idp
| no => idp
第４段階 ── ２つの型が等しいことを示す
\func boolIsAnswer : Bool = Answer => path (iso toAnswer toBool bool-rt1 bool-rt2)
iso という道具を使います。
iso は、次の４つを受け取ります。
| 引数 | 何を渡すか |
|---|---|
| 第１ | 一方から他方への関数 |
| 第２ | 逆向きの関数 |
| 第３ | 往復して元に戻ることの証拠 |
| 第４ | 逆向きに往復して元に戻ることの証拠 |
そして path が、それを等しさの証拠に変換します。
最後の行の型に注目してください。
$$\mathrm{Bool} = \mathrm{Answer}$$
別々に定義した２つの型が、等しいと示されました。
例③ ── 要素が２つの群
第１段階 ── ２つの群を定義する
群Ａは、0 と 1 に足し算を入れたものです。
\data Add2 | zero2 | one2
\func add (x y : Add2) : Add2 \elim x, y
| zero2, y => y
| one2, zero2 => one2
| one2, one2 => zero2
\elim x, y は、２つの引数について同時に場合分けする書き方です。
| 行 | 意味 |
|---|---|
| zero2, y => y |
x が zero2 なら、y をそのまま返す |
| one2, zero2 => one2 |
1 + 0 = 1 |
| one2, one2 => zero2 |
1 + 1 = 0 |
群Ｂは、1 と -1 に掛け算を入れたものです。
\data Mul2 | plus1 | minus1
\func mul (x y : Mul2) : Mul2 \elim x, y
| plus1, y => y
| minus1, plus1 => minus1
| minus1, minus1 => plus1
| 行 | 意味 |
|---|---|
| plus1, y => y |
1 × y = y |
| minus1, plus1 => minus1 |
(-1) × 1 = -1 |
| minus1, minus1 => plus1 |
(-1) × (-1) = 1 |
第２段階 ── 対応づけを定義する
\func toMul (x : Add2) : Mul2 \elim x
| zero2 => plus1
| one2 => minus1
\func toAdd (x : Mul2) : Add2 \elim x
| plus1 => zero2
| minus1 => one2
0 を 1 に、1 を -1 に対応させています。
第３段階 ── 往復すると元に戻ることを示す
\func grp-rt1 (x : Add2) : toAdd (toMul x) = x \elim x
| zero2 => idp
| one2 => idp
\func grp-rt2 (x : Mul2) : toMul (toAdd x) = x \elim x
| plus1 => idp
| minus1 => idp
第４段階 ── 演算が保たれることを示す
ここが、この例の要点です。
\func preserve (x y : Add2) : toMul (add x y) = mul (toMul x) (toMul y) \elim x, y
| zero2, y => idp
| one2, zero2 => idp
| one2, one2 => idp
型に記述されている主張を読み解きます。
$$\mathrm{toMul}(\mathrm{add}(x, y)) = \mathrm{mul}(\mathrm{toMul}(x), \mathrm{toMul}(y))$$
左辺は、「足してから対応づける」です。
右辺は、「対応づけてから掛ける」です。
この２つが等しい。 つまり、対応づけが演算を保っています。
具体的に確かめます。 x も y も one2 の場合です。
左辺：toMul (add one2 one2) → toMul zero2 → plus1
右辺：mul (toMul one2) (toMul one2) → mul minus1 minus1 → plus1
どちらも plus1 になりました。
$1 + 1 = 0$ と $(-1) \times (-1) = 1$ が、対応しているということです。
第５段階 ── ２つの型が等しいことを示す
\func grpSame : Add2 = Mul2 => path (iso toMul toAdd grp-rt1 grp-rt2)
例④ ── 平面の矢印と、２つの数の組
実数は扱いが重いため、ここでは整数で代用します。
第１段階 ── ２つの型を定義する
\data Arrow | arrow Int Int
\func Pair => \Sigma Int Int
Arrow は、２つの整数から作られる型です。
矢印の終点の座標を、$x$ と $y$ で表しています。
Pair は、２つの整数の組です。
\Sigma Int Int が、Haskell の (Int, Int) にあたります。
第２段階 ── 対応づけを定義する
\func toPair (v : Arrow) : Pair \elim v
| arrow x y => (x, y)
\func toArrow (p : Pair) : Arrow => arrow p.1 p.2
p.1 と p.2 が、組の第１成分と第２成分です。
Haskell の fst p、snd p にあたります。
第３段階 ── 往復すると元に戻ることを示す
\func vec-rt1 (v : Arrow) : toArrow (toPair v) = v \elim v
| arrow x y => idp
\func vec-rt2 (p : Pair) : toPair (toArrow p) = p => idp
vec-rt2 には \elim がありません。
組については場合分けが不要で、そのまま計算して同じ形になるためです。
第４段階 ── ２つの型が等しいことを示す
\func vecSame : Arrow = Pair => path (iso toPair toArrow vec-rt1 vec-rt2)
３つをまとめて型検査します
上記のコードを１つのファイルにまとめ、Arend にかけます。
$ java -jar Arend.jar EXALL.ard
--- Typechecking \default ---
[ ] src.EXALL
--- Done (266ms) ---
エラーは出ませんでした。
３つの例すべてについて、２つの型が等しいことを示せています。
$$\mathrm{Bool} = \mathrm{Answer}, \qquad \mathrm{Add2} = \mathrm{Mul2}, \qquad \mathrm{Arrow} = \mathrm{Pair}$$
なお、Cubical Agda でも同じことを記述できますが、筆者の執筆環境には Cubical Agda を用意できなかったため、コード例は掲載していません。
【発展篇】コラム ── より厳密に説明すると
【発展篇】コラム ── より厳密に説明すると
この記事は分かりやすい入門者向けの記事を心がけましたので、厳密な議論を犠牲にした部分があります。以下、中上級者向けに補足説明すべき箇所を述べます。
場面ごとに分けて記します。
場面１について ── 区間を型構成子に渡せるかどうか
\Type は単一の場所ではありません
本文では「\Type は型が置かれる場所」と述べました。
実際には、\Type は階層を持ちます。
\func t0 : \Type0 => Nat
\func t1 : \Type1 => \Type0
\func t2 : \Type2 => \Type1
\Type とだけ記述した場合、処理系がレベルを推論します。
そして Arend の宇宙には、もう１つの添字があります。ホモトピーレベルです。
\Set0 = \0-Type0
\1-Type1
前者の数がホモトピーレベル、後者の数が階層の段です。本文では、この区別に踏み込んでいません。
なお、第３回目以降の記事では、Arend の宇宙には２つの添字があることを、入門者向けの平易な解説として説明する予定です。
Haskell の Type との対応は厳密ではありません
本文では \Type を Haskell の Type（*）に対応させました。
Haskell の * に階層はありません。* :: * が成り立つわけではなく、そもそも * の型を問う仕組みが標準にはありません。
説明のための便宜的な対応です。
\Sigma と Haskell のタプルの対応も、非依存の場合のみです
本文では \Sigma I I を (I, I) に対応させました。
これは、第２成分の型が第１成分の値に依存しない場合に限られます。
依存する場合は、こう記述します。
\data Bool | true | false
\func F (b : Bool) : \Set0 \elim b
| true => Nat
| false => Bool
\func dep : \Sigma (b : Bool) (F b) => (true, 3)
\func dep2 : \Sigma (b : Bool) (F b) => (false, true)
型検査を通過します。
第１成分が true なら第２成分は Nat、false なら Bool。
Haskell には、この形に対応するものがありません。
「もう１つの構成子」は、思考の補助です
本文では、Arend 公式マニュアルの次の記述を引きました。
One way to think about this data type is that it has one more constructor, which connects left and right and which cannot be accessed explicitly.
原文は One way to think about（こう考えるとよい）と述べています。
実際に構成子が存在するわけではありません。区間が２点の集合ではないことを、直観的に述べたものです。
I のホモトピーレベルは特殊です
本文では、\func t2 : \Type => I が通ることを示しました。
これは、I が \Type の要素であることを意味します。
ただし、I が \Set0 に属するかどうかは別問題です。区間は、通常の型とは異なるホモトピーレベルの扱いを受けます。
本文では、その点に踏み込んでいません。
Agda の Set も階層を持ちます
本文では、Cubical Agda の Set を「型が置かれる場所」と述べました。
Set は Set₀ の略記です。Set₁、Set₂ と階層が続きます。
Arend の \Type と同様、単一の場所ではありません。
i0 / i1 と left / right は、同じ理論のものではありません
本文では、両者を対応させました。
区間の両端を指すという役割は同じです。
ただし、Cubical Agda の区間はド・モルガン代数の構造を持ちます。最小 ∧、最大 ∨、反転 ~ の演算が備わっています。
Arend の区間には、これらの演算がありません。代わりに squeeze と squeezeR という補助関数が用意されています。
同じ「区間」という名前でも、備わっている構造が違います。
Arend と Cubical Agda は、同じ立方体型理論ではありません
本文では、両言語がともに立方体型理論を実装していると述べました。
Arend 公式論文は、次のように述べています。
The core theory of Arend represents one of the earliest and simplest forms of cubical type theory, in which the interval still functions as a type.
「最も初期かつ最も単純な形の１つ」 です。
Cubical Agda が実装するド・モルガン立方体型理論とは、別の理論体系です。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", https://arend-lang.github.io/assets/lang-paper.pdf
場面２について ── 面条件を自分で書き並べる
単位元律は、左右で非対称です
本文では、concat p idp = p が idp の一語で示せることを見ました。
しかし、左右を入れ替えると事情が変わります。
-- 右単位元律：計算だけで示せる
\func rightUnit {A : \Type} {a b : A} (p : a = b) : concat p idp = p => idp
-- 左単位元律：場合分けが必要
\func leftUnit {A : \Type} {a b : A} (q : a = b) : concat idp q = q \elim q
| idp => idp
両方とも型検査を通過しますが、証明の書き方が違います。
理由は、concat の定義にあります。
\func concat {A : \Type} {a b c : A} (p : a = b) (q : b = c) : a = c \elim q
| idp => p
第２引数 q について場合分けしているため、concat p idp は定義に従って p に計算されます。
一方 concat idp q は、q が変数のままでは計算が進みません。 そのため、場合分けが必要になります。
この非対称性は、定義の書き方から生じるものです。 \elim p として定義すれば、左右が入れ替わります。
inS は、部分要素の型への注入です
本文では、inS を「底面として渡すための包む操作」と述べました。
より正確には、部分要素の型への注入です。
hfill の第２引数は、面条件と整合していることが型のレベルで保証されている必要があります。inS は、その保証を型に持たせる操作です。
「外側の λ _ →」は、充填方向の変数を受け取ります
本文では、hfill (λ _ → λ { ... }) の外側のラムダを「縦方向の変数を受け取る部分」と述べました。
より正確には、充填を進める方向の区間変数を受け取ります。
この例では、面条件が充填方向に依存しないため、_ で受け流しています。依存する場合は、その変数を使って面条件を記述します。
compPath と concat は、定義が異なります
本文では、Cubical Agda の compPath を Arend の concat に対応させました。
役割は同じですが、定義の仕方が違います。
Arend の concat は、道について場合分けして定義します。
Cubical Agda の compPath は、hcomp を使って定義します。 場合分けが許されていないためです。
同じ操作を、別の手段で実現しているのです。
Set ℓ と \Type の対応も、厳密ではありません
本文では、Cubical Agda の Set ℓ を Arend の \Type に対応させました。
Agda の Set ℓ は、階層の添字を１つ持ちます。
Arend の \Type は、階層の添字に加えて、ホモトピーレベルの添字も持ちます。
\Set0 = \0-Type0
\1-Type1
添字の数が違います。 説明のための便宜的な対応です。
場面３について ── J 規則を自分で組み立てる
J が「強力」というのは、より一般的という意味です
本文では、J が subst より強力だと述べました。
より正確には、J のほうが一般的です。
subst は J から導けます。J の述語 P に、道を使わないものを渡せばよいのです。
逆に、subst だけから J を導くことはできません。 subst の述語は値しか受け取らないため、道についての情報を扱えないからです。
「y は x と同じものになる」は、簡略化です
本文では、p が idp のとき「y は x と同じものになります」と述べました。
Arend の公式マニュアルは、より正確に述べています。
After we match p with idp, variables a and a' become equivalent. To be more precise, we can refer to both variables, but the latter will evaluate to the former.
（筆者による日本語訳）
pをidpと照合したあと、変数aとa'は同等になる。より正確には、両方の変数を参照できるが、後者は前者に評価される。
出典：Prelude — Arend Theorem Prover
両方の変数が使えます。 ただし、片方がもう片方に評価されます。
idp は、通常の意味の構成子ではありません
本文では、「等しさの型には idp という構成子しかない」と述べました。
Arend の公式マニュアルは、idp について次のように述べています。
The constructor idp is not a correct definition since it is not allowed to use lambdas in constructors.
（筆者による日本語訳）
構成子
idpは、正しい定義ではない。構成子のなかでラムダを使うことが許されていないからである。
出典：同上
idp は、処理系に組み込まれた特別なものです。 通常のデータ型の構成子とは、扱いが異なります。
本文では、場合分けの説明のために「構成子」という語を使いました。
transport と coe は、同じ層の操作ではありません
本文では、Cubical Agda の transport を Arend の coe に対応させました。
役割は同じですが、体系のなかでの位置づけが違います。
Arend の coe は、Prelude に置かれた原始的な操作です。 区間型の除去子として、直接定義されています。
Cubical Agda の transport は、より原始的な transp から定義されます。
説明のための便宜的な対応です。
λ j → p (i ∧ j) の型について
本文では、λ j → p (i ∧ j) を「x から p i への道」と述べました。
これは正しい記述です。
ただし、この道の型は i に依存します。i が i0 のときは x から x への道、i1 のときは x から y への道になります。
Cubical Agda では、こうした「端点が依存する道」を PathP という型で扱います。本文では、その区別に踏み込んでいません。
Arend にも、複数の記法があります
本文では、「Arend では等しさの型の使い分けがありません」と述べました。
等しさを表す型が１種類である、という意味です。
ただし記法としては、Path と = の２つがあります。= は Path の中置記法であり、同じものを指しています。
Cubical Agda における「道の型」と「立方体的な同一視型」のような、別の型としての使い分けはありません。