【Arend 連載④】モノイド、群、環、体。一本道ではない数学の代数構造の階層をArend はどうコードに記述するのか

Last updated at 2026-09-03Posted at 2026-09-03

本記事は、連載記事の第４回です

Arend という定理証明支援系について、全７回にわたってお伝えしています。

これまでの流れ

第１回目の記事では、Arend が HoTT（ホモトピー型理論）を公理としてではなく、計算して確かめる対象として扱っていることをお伝えしました。

【Arend Theorem Prover 連載（初回）】「同型なものは等しい」を機械に検査させる ── 定理証明支援系 Arend がHoTTを公理としなかった理由

第２回目の記事では、Arend と Cubical Agda が どこで設計判断を分けたのか を扱いました。

区間 I を普通の型として扱うか、型の外に置くか。

その一点で、両言語は分かれました。

【Arend 連載②】なぜ Arend は「計算しきる力」よりも言語の使いやすさを優先したのか

第３回目の記事 では、等しさを型として扱うと何ができるようになるかを扱いました。移送、商型、関数外延性の３つです。

【Arend 連載③】Haskell の 3 == 3 は True を返して終わる。「なぜ等しいのか」を型として書ける言語では、Haskell にできないことができる

本記事の主題

今回の主題は、数学の代数構造を Arend でどう定義するか 、です。

モノイド、群、環、体。数学の構造は階層をなしています。

下の構造の条件を、上の構造がすべて引き継ぐ形です。

この階層を、そのまま Arend のコードとして記述できるでしょうか？

ここで光があたるのが、Arend の レコード です。

本記事のExecutive Summary

本記事を読むと、何が分かるのか

ところで皆さんは、Haskell で Monoid のインスタンスを書いたことがおありでしょうか？

Monoid には、mempty <> x = x という法則があります。

法則とは、演算が常に満たすべき条件のこと です。
代数学 では公理と呼ばれます。

この式が意味しているのは、次のことです。

mempty は単位元
<> は結合の演算

です。

単位元を左から結合しても、相手は変わらない。

そういう条件です。

Haskell では、コードに記述された法則は、単にプログラマが守るべき推奨事項であって、プログラマが書いた Haskell のコードのなかでその法則が守られているかどうかについて、Haskell の処理系は検査してくれません。

依存型 を持つ言語では、この 法則を型の定義に書き込むことができます 。

法則を満たさないものは、コンパイルした際に、型検査によって弾かれるため、そもそも作ることができない のです。

ただし、これは Arendに限った話ではありません。
Lean 4 でも、Rocq／Coq でも、Agda でも、同じことができます。

では、Arendが他の定理証明言語とは異なる大きな点は、何なのでしょうか？

Arend は、その言語仕様の仕組みのおかげで、数学の代数構造の階層を自然に組み上げていくことができます。

それに対して、Lean 4、Rocq／Coq、Agda といった他の定理証明支援系では、下の階層にある代数概念から、上の階層にある代数概念をうまく積み上げていくのが困難な場面があります。

どう困難なのかは、以下の記事で詳述しました。

Haskellのbaseには群も環も体もない ── 代数構造を型クラスでどこまで表現できるか

Arend は、包摂的部分型付けと顕在フィールド、部分実装 という仕組みが言語仕様の土台に組み込まれているため、こうした困難を回避することができます。

この記事では、Arendの言語仕様 がもつ、数学の代数構造の階層を自然に組み上げていく能力 に光を当てます。

定理証明言語で数学の代数概念を積み上げることが求められる理由

ところで、そもそもなぜ、定理証明言語で数学の代数概念を積み上げていく必要があるのでしょうか？

その背景には、20世紀に集合論で基礎づけられた数学を、2006年ごろから、型理論によって基礎づけられた数学へと移行することを目指す数学基礎論の大きな動向の存在があります。

集合論によって数学を基礎づけること が、数学を研究する上で、いくつか、実務的な弊害 をもたらすことが、世界の数学者コミュニティによって認識されてきました。

弊害① ── 同型なものが、等しくならない

$1/2$ と $2/4$ は、有理数として同じ数です。

しかし、集合論の言葉では 、$(1,2)$ と $(2,4)$ という別々の組になります。

同じことが、群でも起きます。
構造としてまったく同じ２つの群も、集合としては別のものです。

数学者は昔から、そうした２つを「同じもの」として扱ってきました。
しかし、集合論によって基礎づけられた数学では、その扱いを基礎から正当化するのは難しかった のです。

弊害② ── 記述すると、膨大な量になる

集合論では、すべての数学的対象を集合として表します。そのため、ひとつの定義を記述するのに何ページもの記号を要することがあります。

人間が読んで理解するぶんには、気になりません。しかし機械に検査させようとすると、その負担が一気に表面化します。

弊害③ ── 構造の階層が、そのまま表せない

群、環、体。数学の構造は積み上がり、途中で分岐し、また合流します。

集合論では、この階層を直接表す仕組みがありません。「この群はモノイドでもある」という関係を、そのつど記述することになります。

そこで、型理論への移行が始まった

2006年ごろ、これらを解こうとする動きが始まりました。
一価的基礎づけ、UF と呼ばれます。

集合論 の代わりに、型理論 の上で数学を組み立てる。

そこで白羽の矢が立ったのが、マーティン＝レーフ型理論、略して MLTT でした。

Rocq、Agda、Lean 4。定理証明支援系はいずれも、MLTT かその近縁の体系を土台にしています。

数学の基礎を作り替えることと、機械に検査させることは、最初からつながっていたのです。

本記事の第３部で、この経緯を扱います。

そのうえで、代数構造の階層をコードで記述する話に入ります。

この記事の結論

この記事の論旨展開と結論を先に要約してお伝えします。

第１に、Arend は、包摂的部分型付けと顕在フィールドと部分実装を、言語の土台に組み込んでいます。

これによって何ができるのかを、順に述べます。

できること① ── 上位概念を、下位概念が求められる場面へ持ち込める

群は、モノイドの代数的条件をすべて満たす上位概念です。

モノイドに求められるのは、演算と単位元と結合律。群は、それらに加えて逆元を持ちます。

そのため、モノイドが求められる場面には、群を持ち込むことができます。 群は、モノイドとしての条件をすでに満たしているからです。

Arend では、これを言語の側が認めています。

群の値を、モノイドを受け取る関数へ、そのまま渡せます。変換のための関数を書く必要がありません。

この仕組みが、包摂的部分型付けです。

できること② ── レコードの項目の値を、定義の時点で確定させておける

レコードとは、複数の値をひとまとめにして名前を付ける仕組みです。Haskell のレコード構文にあたります。

通常、レコードの項目は「これから埋めるもの」です。 値を作るときに、はじめて決まります。

Arend では、その一部を定義の時点で確定させておけます。

タロウくん：
・・・オブジェクト指向言語の既定値のようなものですか。

専任講師：
似ていますが、決定的に違う点があります。

既定値は、指定しなければその値になるだけで、あとから上書きできます。

Arend で確定させた値は、上書きできません。型の一部になっているからです。

たとえば「$y$ 座標が $0$ である点」というレコードを作ると、それは「$y$ が $0$ である」という情報を型そのものが持っています。

タロウくん：
・・・別の値を入れる余地がない。

専任講師：
この仕組みが、顕在フィールドです。

できること③ ── 一部だけを埋めた中間の型を作れる

そして、確定させる項目は一部だけでも構いません。

「担い手の型は自然数である。ただし、演算と単位元はまだ決めない」。
そういう中間の型を作れます。

タロウくん：
・・・途中まで埋めて、残しておく。

専任講師：
そこから、複数のものを作れます。

自然数の足し算のモノイドと、自然数の掛け算のモノイド。
共通する部分は中間の型にまとめ、違う部分だけを別々に埋めます。

この仕組みが、部分実装です。

３つが揃うと、階層を自然に組み上げられる

この３つが揃うことで、数学の代数構造の階層を、そのままコードに写すことができるようになります。

モノイドや群のような基本構造を組み合わせることで、環や体のような、より豊かな構造を作っていきます。

可換局所環と GCD 整域から体へ合流させる。
分岐した２つの経路から受け継いだ項目を、片方の言葉で埋める。

そうしたことも可能になります。

ところで、Lean・Rocq／Coq・Agda は、こうした言語仕様を、自らの言語構造の土台として持っていません。

これらの言語は、言語構造の土台部分を単純に保ち、必要な機能は外側の仕組みで補う設計を選択したのです。

群の値をモノイドとして渡したいときは、型検査器が変換関数を自動で挿入する。

各言語のコードを記述するプログラマの側から見れば、簡単なコードを書く場面では、Arendと他の定理証明言語とでは、大きな違いはありません。

しかし、代数構造の階層が深くなると、言語観の差が表面化してくることになります。

言語構造の土台部分をシンプルな状態に保つか、それとも、必要に迫られて複雑な構造にする選択を選ぶのか。

Arendが選択したこの論点に対する判断結果は、本連載シリーズの第２回目の記事で取り上げたArendの選択とは、一見すると異なるように見えます。

本連載シリーズの第２回目の記事では、Arend が区間 I を普通の型 ── 文字列型や整数型と同じ扱い ── として置くことで、言語の仕様をシンプルにし、使い勝手の良さを優先したと述べました。

その一方で、Cubical Agda は、区間を普通の型とは別のものとして扱い、言語の仕様を複雑にする選択をしました。

この記事で取り上げる言語構造の土台を複雑にするかシンプルに保つかという論点をめぐって、Arend と他の定理証明支援系が選択した方向性は、このように一見すると、第２回目の記事で確認した方向性とは反対側であるかのように見えてしまいます。

しかし、Arend 公式論文を調べた結果、そう見えるだけであることが分かりました。

本連載シリーズの第２回目の記事で述べたこと

本連載シリーズの第２回目の記事では、Arend は、区間 I を普通の型と同じ扱い方をしたことで、Cubical Agda に比べて、Arend は計算可能性を犠牲にしたことを紹介しました。

しかし、数学の形式化を行う実務では、数学の定理を証明したり反証したりするためには、計算可能性は必ずしも必要とされない、との認識が Arend の公式文書に記載されていることも取り上げました。

計算可能性を犠牲にすると、具体的な計算結果を得ることができなくなりますが、数学定理を証明したり反証したりすることはできるからです。

ただし、正しいことが証明された定理を使った計算を進めて、具体的な数を求めることはできません。

Arend は数学の実務ニーズを犠牲にすることなく、言語仕様をシンプルに保つことで、Cubical Agda よりもプログラマに負担がかからない言語を生み出すことができたのです。

本記事で扱う言語仕様も、同じ理由から来ている

本記事で扱う レコードの階層 や、包摂的部分型付け 、 顕在フィールド 、 部分実装の言語仕様 もこれと同様に、数学の形式化を行うためには必要な、現場から求められる機能だった のです。

結論として、Arend が他の定理証明支援系に比べて、目的も動機もなく、言語仕様を複雑にしたわけではない というのが、本記事執筆者の受け止め方です。

どちらの判断についても、Arend 公式論文は「形式化の実践」という言葉を根拠に置いています。

この論点については、Arend公式資料などの一次資料を紐解きながら、第７部で詳しく取り上げます。

では、土台に入れることの良い面と悪い面は、何なのか

ここまで、Arend が包摂的部分型付けと顕在フィールドを言語の土台に入れたこと、そして Lean・Rocq／Coq・Agda がこの２つを土台から外していることを述べました。

ただし、これは「他の処理系では代数構造の階層を表現できない」という意味ではありません。

Lean 4 の Mathlib は、現代数学の広い範囲を実際に形式化しています。
そこには群も環も体も含まれます。Rocq／Coq の Mathematical Components も同様です。

Lean 4 には構造体、継承、coercion、typeclass inference があります。

Rocq／Coq には canonical structures や Mathematical Components の mixin 階層があります。

Agda には record、instance arguments、module system があります。

どれも、代数構造の階層を組み上げるために使われています。

違うのは、その階層をどこで支えるか、です。

土台に入れることのメリット

#	内容
①	変換のための関数を書かずに済みます。群をモノイドとして渡すとき、変換関数が間に入りません
②	設計判断を先送りできます。何を型引数にするかを、定義の時点で決めなくてよいのです
③	分岐した２つの経路から継承したフィールドを、片方の言葉で埋められます。体を可換局所環と GCD 整域から作るとき、これが効きます
④	小さなレコードを大量に作らずに済みます。論文は、顕在フィールドがない場合にそうなると述べています

土台に入れることのデメリット

#	内容
①	土台が大きくなります。言語の中核が扱う規則が増えます
②	型理論の文献には、包摂的部分型付けを定理証明支援系に用いることへの否定的な議論があります
③	利用者が少なく、ライブラリの規模も Mathlib より小さいのが現状です

そして、次の点は確認できませんでした。

「Arend のほうが階層を短く記述できる」という主張を裏づける定量的な比較実験は、筆者が調べた範囲では見つかりませんでした。

（土台ではなく）言語の外側で補うことのメリット・デメリット

（メリット）

#	内容
①	土台が小さく保たれます
②	成熟した仕組みが揃っています。 coercion、typeclass、canonical structures
③	Mathlib という巨大な蓄積があります

（デメリット）

#	内容
①	変換の手当てが要ります。型検査器が変換関数を挿入します
②	ダイヤモンド継承の設計が難所になります。 Mathlib でも長く議論されてきました
③	型引数を後から増やすと、そのクラスを使っているコードが壊れます

どちらが優れているか、ではない

上記は、設計判断の違いです。

土台を小さく保つか。
それとも、土台に機能を入れて、上の層の負担を減らすか。

この記事は、Arendと、それ以外の言語が下した判断の中身を追いかけます。

本記事には、Arend 以外の言語も登場します

本記事の主題は Arend です。

しかし、Arend の設計判断を理解するには、他の言語がどうしているかを見る必要があります。

「Arend はこうしている」とだけ述べても、それが何を選び、何を諦めたことなのかが分かりません。

比較の相手があってはじめて、判断の意味が見えてきます。

そこで本記事では、次の言語を引き合いに出します。

言語・処理系	本記事で登場する理由
Arend	本記事の主題。レコードに包摂的部分型付けと顕在フィールドを持つ
Haskell	出発点。型クラスの法則が検査されない、という問題から入る
Lean 4	対比の中心。依存型を持ち、法則を型に記述できる。しかし土台の設計が違う
Rocq／Coq、Agda	同じく対比。 Lean 4 と同じ方式を採る
Matita	顕在フィールドを持つ、もうひとつの処理系
Nuprl	包摂的部分型付けを持つ体系

本記事の議論の流れ

青い枠が出発点です。 Haskell で誰もが経験する問題から始まります。

金色の枠が、本記事の中心です。 階層をどう書くか、Arend が何を土台に組み込んだか、それが実務でどう使われているか。

緑の枠が到達点です。 Arend の判断基準が、第２回目の記事と一貫していることを述べます。

第２回目の記事を読まれた方へ

第２回目の記事では、Arend が理論を単純に保つことを選んだと述べました。

本記事では、Arend が言語の土台に機能を足したと述べます。

逆のことを言っているように見えるはずです。

その答えは、記事の最後に示します。

本記事の読み方

本記事は長いため、関心に応じた入口を示しておきます。

関心	どこから読むか
Haskell の型クラス設計の悩みから読みたい	第１部から順に
なぜ型理論で数学を組み立てるのかを知りたい	第３部
Arend のレコードの機能だけ知りたい	第４部・第５部
実務での利用実績を知りたい	第６部
Arend と Lean 4 のどちらを選ぶべきかを知りたい	第６部の後半

第１部 ── Haskell の `Monoid` には、法則がある

しかし、コンパイラは検査しない

Haskell で Monoid のインスタンスを書いたことがあるでしょうか。

＜Haskell のコード＞

newtype MyType = MyType Int

instance Semigroup MyType where
  MyType x <> MyType y = MyType (x + y)

instance Monoid MyType where
  mempty = MyType 0

これで、MyType を Haskell の Monoid インスタンスとして宣言できました。

`Monoid` の法則

Monoid には、満たすべき法則があります。

「法則」とは、演算が常に満たすべき条件のことです。 代数学では公理と呼ばれます。

過去記事で解説済みですが、ここで改めて解説します。

Haskell の標準ライブラリのドキュメントに、次の３つが書かれています。

法則	意味
`mempty <> x = x`	単位元を左から結合しても、相手は変わらない
`x <> mempty = x`	単位元を右から結合しても、相手は変わらない
`(x <> y) <> z = x <> (y <> z)`	どこから計算しても、結果は同じ

式の読み方

記号の意味を確かめておきます。

記号	意味
`mempty`	単位元。何と結合しても、相手を変えない値
`<>`	結合の演算。２つの値をひとつにまとめる

１つ目の式 mempty <> x = x を読み下します。

左辺は「単位元と x を結合したもの」です。右辺は「x そのもの」です。

この式は、その２つが等しいと述べています。

タロウくん：
・・・単位元を結合しても、何も起きない。

専任講師：
そのとおりです。数の足し算でいえば、0 + x = x にあたります。

掛け算でいえば、1 * x = x です。

タロウくん：
・・・0 や 1 が、単位元にあたる。

専任講師：
そして３つ目の式は、結合律です。

(x <> y) <> z = x <> (y <> z)

左から順に計算しても、右から順に計算しても、結果が同じである。 そういう条件です。

タロウくん：
(1 + 2) + 3 と 1 + (2 + 3) が、どちらも 6 になるのと同じですね。

専任講師：
その性質を、演算一般について要求しているのです。

守らなくても、コンパイルが通る

ここに問題があります。

＜Haskell のコード＞

newtype Broken = Broken Int

instance Semigroup Broken where
  Broken x <> Broken y = Broken (x + y)

instance Monoid Broken where
  mempty = Broken 999   -- 単位元ではない

Broken 999 は、単位元ではありません。Broken 999 <> Broken 0 は Broken 999 になり、Broken 0 にはなりません。

しかし、このコードはコンパイルが通ります。

タロウくん：
・・・法則を守っていないのに、通るのですか。

専任講師：
通ります。

Haskell では、コードに記述された法則は、単にプログラマが守るべき推奨事項であって、プログラマが書いた Haskell のコードのなかでその法則が守られているかどうかは、Haskell の処理系は検査しません。

タロウくん：
では、何のための法則なのですか。

専任講師：
利用する側が、法則を前提にして書くためです。

mconcat という関数があります。リストの要素をすべて結合するものです。

＜Haskell のコード＞

mconcat :: Monoid a => [a] -> a

この関数は、どこから結合しても同じ結果になることを前提にしています。

タロウくん：
・・・結合律を前提にしている。

専任講師：
そして、その前提が破られていても、Haskell の処理系は何も指摘しません。

タロウくん：
・・・実行してみて、はじめておかしいと気づく。

専任講師：
本記事は、この問題から始めます。

法則を型に書き込めないか

タロウくん：
法則を、コンパイラに検査させられないのですか。

専任講師：
Haskell では難しいのです。

mempty <> x = x という主張を、型として記述する手段がありません。

タロウくん：
・・・第３回目の記事で扱った話ですね。3 = 3 が型にならない、という。

専任講師：
同じ問題です。

Haskell には依存型がないため、「２つの値が等しい」という主張を型として記述する手段がありません。

タロウくん：
では、依存型を持つ言語なら記述できるのですか。

専任講師：
記述できます。次の部で見ましょう。

第２部 ── 依存型があれば、法則を型に記述できる

Arend で書いてみる

Arend では、レコードの定義のなかに法則を書き込めます。

＜Arend のコード＞

\record Monoid (A : \Type)
  | unit : A
  | op : A -> A -> A
  | leftUnit (x : A) : op unit x = x
  | rightUnit (x : A) : op x unit = x
  | assoc (x y z : A) : op (op x y) z = op x (op y z)

＜Arend の型検査結果＞

$ java -jar Arend.jar M3.ard

--- Typechecking \default ---
[ ] src.M3
--- Done (183ms) ---

型検査を通過します。

Arend では、レコードの定義のなかに、値だけでなく法則そのものも書き込めます。ここでは、単位元 unit、演算 op、そしてモノイドが満たす３つの法則を、ひとつのレコードにまとめています。

記号の読み方

本記事では、Arend のコードを何度も示します。

先に、記号の読み方をまとめておきます。

Arend	意味	Haskell でいえば
`\record`	レコードを定義する	`data` のレコード構文
`\class`	型クラスを定義する	`class`
`\func`	関数や値を定義する	関数定義（`f x = ...`）
`\data`	データ型を定義する	`data`
`=>`	定義の本体を書き始める	`=`
`\extends`	別のレコードを拡張する	`=>` による上位クラスの指定
`\cowith`	レコードの値を作る	レコード構文による値の生成
`\override`	継承した項目の型を絞り込む	──
`\Type`	型が置かれる場所	`*`
`\Set0`	等しさの根拠が高々１本の型を集めた場所	──
`\Prop`	要素が高々１つしかない型を集めた場所	──
`\Sigma`	組の型を作る	`(,)`
`\Pi (x : A) -> ...`	依存関数の型	──
`->`	関数の型を作る	`->`
`\|`	項目や選択肢を区切る	`\|`
`\elim x`	引数 `x` について場合分けする	`case x of`
`\lam x => ...`	無名関数を作る	`\x -> ...`
`:`	「〜の型を持つ」	`::`
`{A : \Type}`	暗黙の引数。呼び出し時に書かなくてよい	型変数 `a`
`a = b`	`a` と `b` が等しいことを表す型	──
`idp`	両辺が計算して同じ形になる証拠	──
`{?}`	まだ埋めていない箇所	──
`Nat.*`	自然数の掛け算	`*`
`Nat.+`	自然数の足し算	`+`

Arend の公式マニュアルは、次のページにあります。

言語リファレンス：https://arend-lang.github.io/documentation/language-reference/
入門用のチュートリアル：https://arend-lang.github.io/documentation/tutorial/

なお、\ はキーワードの目印です。 Haskell のラムダ式とは異なります。

Haskell の \x -> ... にあたるものは、Arend では \lam x => ... と記述します。\lam で１つのキーワードです。

１行ずつ読み解く

部分	意味
`\record Monoid (A : \Type)`	`Monoid` というレコードを定義する。型 `A` を受け取る
`\| unit : A`	単位元。`A` の値をひとつ持つ
`\| op : A -> A -> A`	演算。`A` の値を２つ受け取って、`A` の値を返す
`\| leftUnit (x : A) : ...`	左単位律。単位元を左から結合しても、`x` は変わらない
`\| rightUnit (x : A) : ...`	右単位律。単位元を右から結合しても、`x` は変わらない
`\| assoc (x y z : A) : ...`	結合律。計算のまとまり方を変えても、結果は変わらない

上の２行は、Haskell のレコード構文と同じ発想です。値と関数を、ひとまとめにしています。

注目すべきは、下の３行です。

leftUnit と rightUnit は、単位元が本当に単位元として働くことを示す法則です。

assoc は、演算の結合のしかたを変えても結果が変わらないことを示す法則です。

どれも値でも関数でもありません。たとえば assoc は、「$(x \cdot y) \cdot z$ と $x \cdot (y \cdot z)$ が等しい」という主張です。

この３行があるため、Arend で Monoid を作るときには、単位元と演算だけでなく、それらの法則の証明も渡さなければなりません。法則を満たさないものは、そもそも Monoid として作ることができないのです。

タロウくん：
・・・先ほどの Broken のようなものは、作れない。

専任講師：
作れません。証明を渡せないからです。

ただし、これは Arend 固有ではありません

タロウくん：
Arend はすごいですね。

専任講師：
そこは、はっきりさせておく必要があります。

これは Arend 固有の性質ではありません。

タロウくん：
・・・違うのですか。

専任講師：
依存型を持つ言語なら、どれでもできます。

Lean 4 で書いてみます。

＜Lean 4 のコード＞

class MyMonoid (α : Type) where
  ide : α
  op : α → α → α
  ide_left : ∀ x, op ide x = x
  ide_right : ∀ x, op x ide = x
  op_assoc : ∀ x y z, op (op x y) z = op x (op y z)

instance : MyMonoid Nat where
  ide := 999
  op := Nat.add

単位元として 999 を渡し、法則の証明を渡していません。

＜Lean 4 の型検査結果＞

$ lean LawTest.lean
LawTest.lean:10:24: error: fields missing: 'ide_left', 'ide_right', 'op_assoc'

弾かれます。

タロウくん：
・・・Lean 4 でも、同じことができるのですね。

専任講師：
Rocq／Coq、Agda、Idris 2 も同様です。

「法則を型として記述できる」は、依存型を持つ処理系すべてに共通する性質です。

では、Arend は何が違うのか

タロウくん：
では、Arend の何が違うのですか。

専任講師：
構造の階層をどう書くか、です。

Monoid を１つ定義するだけなら、どの言語でも同じです。しかし、モノイドや群のような基本構造を組み合わせて、環や体を作っていくとき、事情が変わります。

タロウくん：
・・・階層になると、何が起きるのですか。

専任講師：
そこを、次の部で扱います。

第３部 ── 本当の問題は、階層である

なぜ、型理論の上で数学を組み立てるのか

本記事は「数学の代数構造を Arend でどう定義するか」を扱います。

しかし、そもそもなぜ、型理論の上で数学を組み立てるのでしょうか。

その問いに、先に答えておきます。

過去記事で解説済みですが、ここで改めて解説します。

集合論で数学を基礎づけると、何が起きるのか

タロウくん：
先生、数学の基礎といえば、集合論だと聞いたことがあります。

専任講師：
20世紀を通じて、そう扱われてきました。

すべての数学的対象を集合として表す。自然数も、関数も、群も、すべて集合です。

タロウくん：
・・・それで、うまくいっているのですか。

専任講師：
人間が読んで理解するぶんには、うまくいっています。しかし、困ることがあります。

困難① ── 同型なものが、等しくならない

専任講師：
分数で説明します。

$1/2$ と $2/4$ と $3/6$。これらは、有理数として同じ数です。

タロウくん：
はい。

専任講師：
しかし、集合論の言葉で書くとどうなるか。

分数は「分子と分母の組」として表されます。

$1/2 \rightarrow (1, 2)$

$2/4 \rightarrow (2, 4)$

$3/6 \rightarrow (3, 6)$

タロウくん：
・・・組としては、すべて違うものです。

専任講師：
そこが問題です。

同じ数を表しているのに、集合としては別のものになってしまいます。

タロウくん：
第３回目の記事で扱った商型の話ですね。

専任講師：
同じ問題です。

そして、これは分数に限りません。

群でも、同じことが起きる

専任講師：
２つの群があるとします。

構造としては、まったく同じ。演算の表も、要素の対応も、ぴたりと重なる。

タロウくん：
・・・同型である、ということですね。

専任講師：
数学者は、そういう２つの群を「同じもの」として扱ってきました。

タロウくん：
同型なら等しい、というのは当たり前ではないのですか。

専任講師：
数学者は昔からそう扱ってきました。しかし、その扱いを基礎から正当化するのは難しかったのです。

タロウくん：
なぜですか。

専任講師：
集合論では、同型であることと等しいことは別のものだからです。

同型な２つの群も、集合としては違うものです。

タロウくん：
・・・慣行としては認めているが、根拠がなかったということですか。

専任講師：
そういうことです。

構造同一性原理

専任講師：
ホモトピー型理論は、これを構造同一性原理として支えます。

（原文引用）

Univalence axiom implies structure identity principle: isomorphic structures (such as groups, topological spaces and so on) are equal.

（筆者による日本語訳）

一価性公理は、構造同一性原理を導く。すなわち、同型な構造（群や位相空間など）は等しい。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・「同型なら等しい」が、定理として成り立つ。

専任講師：
慣行だったものが、体系の内部で支えられるのです。

困難② ── 記述すると、膨大な量になる

タロウくん：
ほかにも困難がありますか。

専任講師：
集合論による形式化は、記述するのに何ページもの記号を要します。

タロウくん：
紙に書くぶんには困らないのでは。

専任講師：
機械に検査させようとすると、その負担が一気に表面化します。

タロウくん：
機械に検査させる、というのは。

専任講師：
定理証明支援系という道具があります。証明を書く言語と、それを検査する処理系を合わせたものです。

本連載で扱っている Arend も、そのひとつです。

そこで、型理論が選ばれた

タロウくん：
・・・それで、数学の基礎を作り替えようという動きがあると。

専任講師：
2006年ごろから始まりました。一価的基礎づけ、UF と呼ばれます。

タロウくん：
集合論をやめる、ということですか。

専任講師：
集合論の代わりに、型理論の上で数学を組み立てます。

タロウくん：
型理論とは、Haskell の型のようなものですか。

専任講師：
近いものです。ただし、もっと強力です。型が値に依存できます。

タロウくん：
値に依存する、というのは。

専任講師：
Vector Int 3 のように、「長さ３の整数のベクトル」という型を記述できます。3 という値が、型の一部になっています。

タロウくん：
Haskell では記述できませんね。

専任講師：
依存型と呼ばれる仕組みです。この理論を、マーティン＝レーフ型理論、略して MLTT といいます。

なぜ、型理論だったのか

タロウくん：
なぜ、わざわざ型理論を選んだのですか。

専任講師：
理由はいくつかあります。ひとつは、いま述べた記号の量です。

集合論による形式化は、記述するのに何ページもの記号を要します。

タロウくん：
それが、型理論なら短くなる。

専任講師：
型そのものが、構造を表すからです。

「これは群である」という主張を、型として記述できます。 集合論では、いくつもの条件を並べることになります。

タロウくん：
・・・第２部で見た Monoid のレコードが、まさにそれですね。

専任講師：
そのとおりです。

そして、定理証明支援系との接続

タロウくん：
それが、機械に検査させることと関係するのですか。

専任講師：
Rocq、Agda、Lean 4。これらの定理証明支援系は、いずれも MLTT かその近縁の体系を土台にしています。

タロウくん：
・・・UF が選んだ理論と、同じですか。

専任講師：
同じです。そして、それは偶然ではありません。

タロウくん：
どういうことですか。

専任講師：
UF は最初から、証明支援系の利用に適した基礎づけを作ることを目的の一部としていました。

タロウくん：
・・・数学の基礎を作り替えることと、機械に検査させることが、最初からつながっていたのですね。

専任講師：
そういう経緯です。

そして本記事で扱う代数構造の階層は、その接続点にあたります。

数学の側では、モノイド、群、環、体という階層があります。それを、型として記述できるかどうか。 そこが問われているのです。

階層の設計は、一意に定まらない

専任講師：
では、階層の話に入ります。

モノイド、群、環、体。数学の構造は積み上がっています。下の条件を、上がすべて引き継ぎます。

タロウくん：
順番に定義していけばよいのでは。

専任講師：
そう単純ではありません。

この論点は、筆者が過去に書いた記事で詳しく扱いました。

Haskellのbaseには群も環も体もない ── 代数構造を型クラスでどこまで表現できるか

そこから、いくつか引用します。

どこで可換性を入れるか

過去記事に、次の記述があります。

可換性をどこで入れるか。モノイドの段階で分けるのか、群の段階か、それとも環になってからか。決め手がありません。

タロウくん：
・・・設計者が決めるしかない。

専任講師：
そして、決め方が分かれています。

同じ Haskell の中でも、algebra と numeric-prelude では切り方が異なります。

Lean の Mathlib でも問題だった

専任講師：
Haskell だけの問題ではありません。

Lean の Mathlib でも、代数構造の階層をどう設計するかという論点をめぐって、これまで長い議論がなされてきました。

タロウくん：
・・・数学の形式化で先を行っている Mathlib でも。

専任講師：
理由は、組み合わせの数です。

可換性、有限性、順序、位相 ── これらを掛け合わせると、クラスの数が手に負えなくなります。

それぞれの対処

専任講師：
Mathlib は、こう対処しています。

extends による継承を基本としつつ、性質ごとの小さなクラスを併用する設計が採られています。

そして Rocq／Coq では、別の方法が使われています。

Rocq の Mathematical Components では、混合（mixin）と呼ばれる仕組みが、より徹底した形で使われています。

タロウくん：
・・・どの体系でも、苦労している。

専任講師：
過去記事の結論は、こうでした。

型クラスによる代数構造の階層化は、どの体系でも難問である。

代数構造の階層は、１本道ではない

専任講師：
もうひとつ、厄介な事情があります。

階層は、１本道ではありません。

タロウくん：
どういうことですか。

専任講師：
Arend 公式論文が、具体例を挙げています。

（原文引用）

For example, a field is both a commutative local ring and a GCD domain so it is natural to define the type Field of fields as an extension of LocalCRing and GCDDomain which requires multiple inheritance.

（筆者による日本語訳）

たとえば、体は可換局所環であると同時に GCD 整域でもあるため、体の型 Field を LocalCRing と GCDDomain の拡張として定義するのが自然であり、そのためには多重継承が必要になる。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・出てくる言葉が分かりません。

専任講師：
順に説明します。

整域とは何か

整域とは、掛け算が可換な環のうち、次の性質を持つものです。

ゼロでないもの同士を掛けて、ゼロになることがない。

整数がその例になります。$a \neq 0$ かつ $b \neq 0$ であれば、$a \times b$ が $0$ になることはありません。

当たり前に思えるかもしれません。しかし、そうならない構造もあります。

タロウくん：
ゼロでないもの同士を掛けて、ゼロになる。そんなことがあるのですか。

専任講師：
まず、「整数を $6$ で割った余り」の世界を考えます。

この世界の要素は、$0, 1, 2, 3, 4, 5$ の６つです。
掛け算の結果も、$6$ で割った余りに置き換えます。

タロウくん：
・・・時計の文字盤のようなものですね。

専任講師：
この世界では、$2$ も $3$ も $0$ ではありません。

しかし、$2 \times 3 = 6$ です。
そして、 $6$ を $6$ で割った余りは $0$ です。

$$2 \times 3 = 6 = 0 \quad （6 で割った余りの世界では）$$

タロウくん：
・・・ゼロでないもの同士を掛けたのに、ゼロになりました。

専任講師：
このような組を、零因子と呼びます。

整域とは、可換環のうち、零因子を持たないもののことです。

行列の世界でも、同じことが起こります

専任講師：
零因子は、可換でない構造にも現れます。

$1$ 行 $1$ 列だけが $1$ で他が $0$ の行列と、$2$ 行 $1$ 列だけが $1$ で他が $0$ の行列を掛けると、すべてが $0$ の行列になります。

左の行列も右の行列も、零行列ではありません。
しかし、両者を掛けると零行列になります。

タロウくん：
・・・確かに、そうなりますね。

専任講師：
ただし、正方行列全体の掛け算は、一般には可換ではありません。

なので、この例は、「可換環としての整域ではない例」ではありません。
零因子という現象が、より広い構造にも現れる例です。

構造	零因子を持つか
整数	持たない（整域である）
多項式環（係数が整域の場合）	持たない（整域である）
整数を $6$ で割った余りの世界	持つ（$2 \times 3 = 0$）
正方行列	持つことがある。ただし、掛け算は一般に可換ではない
体	持たない（体は整域である）

なお、正確には $0 \neq 1$ という条件も必要です。
要素がひとつしかない構造を除くためのものです。

本記事では、この点に深入りしません。

**ここでは、通常の代数学で用いる「$0$ と $1$ が異なる可換環」を前提にしています。

** 正方行列の例は、零因子という現象が、可換でない構造にも現れることを示すため に挙げています。

タロウくん：
過去記事にも、似た話がありましたね。

専任講師：
関数の掛け算の例 です。

vector-space というライブラリを扱った箇所でした。

タロウくん：
・・・どういう例でしたっけ？
ちょっと忘れてしまいました。すいません。

専任講師：
関数どうしを掛けると、零因子が現れるという話です。

ちょっとおさらいしてみましょうか。

まず、関数の掛け算を決めます。
各点ごとに、値を掛け合わせます。

２つの関数 $f$ と $g$ があるとき、その積は $(f \times g)(x) = f(x) \times g(x)$ です。

タロウくん：
・・・それぞれの点で、値を掛ける。

専任講師：
そして、定義域として ${0, 1}$ という２点だけを考えます。

そこで、次の２つの関数を作ります。

	$x = 0$ のとき	$x = 1$ のとき
$f(x)$	$1$	$0$
$g(x)$	$0$	$1$

タロウくん：
・・・値を取る場所が、ずれています。

専任講師：
$f$ は $x = 0$ で $1$ を返すので、零関数ではありません。

$g$ は $x = 1$ で $1$ を返すので、こちらも零関数ではありません。

タロウくん：
どちらも、全体としては $0$ ではない。

専任講師：
では、積を計算してみましょう。

	$x = 0$ のとき	$x = 1$ のとき
$f(x) \times g(x)$	$1 \times 0 = 0$	$0 \times 1 = 0$

タロウくん：
・・・どちらの点でも $0$ になっています。

専任講師：
つまり、$f \times g$ は零関数です。

タロウくん：
零関数でないもの同士を掛けて、零関数になった。

専任講師：
これが零因子です。

タロウくん：
・・・行列の例と、同じことが起きている。

専任講師：
過去記事では「ゼロでないもの同士を掛けてゼロになる」と述べましたが、そこでは名前を付けていませんでした。

零因子 と呼びます。

可換局所環と GCD 整域

ところで、少し前に、以下の引用文を取り上げました。

たとえば、体は可換局所環であると同時に GCD 整域でもあるため、体の型 Field を LocalCRing と GCDDomain の拡張として定義するのが自然であり、そのためには多重継承が必要になる。

この引用文に、以下の２つの構造の名前が登場します。

名前	コードでの表記
可換局所環	`LocalCRing`
GCD 整域	`GCDDomain`

順に見ていきます。

可換局所環

可換局所環 （ LocalCRing ）とは、掛け算が可換な環のうち、「割り算できない要素」がひとつのまとまりに収まっているものです。

タロウくん：
どういうことですか？

専任講師：
整数で考えてみましょう。

整数のなかで、割り算ができる要素は $1$ と $-1$ だけです。
$2$ で割ると、多くの場合に整数の外へ出てしまいます。

タロウくん：
・・・$3 \div 2$ は整数になりません。

専任講師：
そこで、割り算できない要素を集めてみます。

整数の場合、$2$ の倍数、$3$ の倍数、$5$ の倍数。
素数ごとに、別々のまとまりができます。

タロウくん：
・・・ひとつにまとまっていない。

専任講師：
整数は、可換局所環ではありません。

可換局所環では、割り算できない要素がひとつのまとまりに収まります。

タロウくん：
そういう構造が、あるのですか。

専任講師：
あります。たとえば、体はそのひとつです。

体では、$0$ 以外のすべてが割り算できます。
割り算できない要素は $0$ だけです。

タロウくん：
・・・$0$ ひとつだけのまとまり。

専任講師：
それも「ひとつのまとまり」です。
だから 体は、可換局所環の条件を満たしています。

次に進みます。

GCD 整域（GCDDomain）とは、先ほど述べた整域のうち、どのふたつの要素についても最大公約数が定まるもののことです。

整数がその例になります。
$12$ と $18$ の最大公約数は $6$ である、という計算ができます。

本記事では、この２つの中身に踏み込みません。

引用文が伝えているのは、体という構造が、性質の異なる２つの構造の両方に属しているという事実です。

そのため、体を定義するには両方から引き継ぐ必要があります。

多重継承とは何か

多重継承とは、ひとつの構造が複数の構造を同時に引き継ぐことです。

たとえば、体は可換局所環でもあり、GCD 整域でもあります。
体を定義するとき、この両方から条件を引き継ぎたい。

それが多重継承です。

オブジェクト指向言語でも同じ語が使われますが、ここでは代数構造の階層について述べています。

Haskell の型クラスでも、複数の上位クラスを持てます。

＜Haskell のコード＞

class (Semigroup a, Show a) => MyClass a where

=> の左に、複数のクラスを並べています。この点は Arend も同じです。

違いは、そのあとにあります。 多重継承した先で、引き継いだ項目をどう扱えるか。そこが本記事の主題になります。

図にすると

専任講師：
階層の形を、図にします。

        モノイド
           │
           群
           │
           環
         ／   ＼
可換局所環     GCD 整域
         ＼   ／
           体

タロウくん：
・・・下から積み上がって、途中で分岐して、また合流している。

専任講師：
この形を、そのままコードで記述できるかどうか。それを、これから見ていきます。

第４部 ── Lean・Rocq／Coq・Agda は、土台を単純に保った

階層を記述するには、２つの仕組みが必要

Lean、Rocq／Coq、Agda は、言語の土台となる型理論のなかで、２つの仕組みを避けてきました。

ここでいう土台とは、型検査器が直接扱う規則の集まりのことです。

言語には、土台の部分と、その上に載っている部分があります。土台の規則は、型検査器が最終的な判定に使うものです。上に載っている部分は、書きやすさのための仕組みで、最終的には土台の言葉へ翻訳されます。

便利な機能を土台に入れず、上の層で実現する。 そういう設計が採られてきた、ということです。

ひとつ目 ── 包摂的部分型付け

避けてきた仕組みのうち、ひとつ目は、群はモノイドの条件をすべて満たすのだから、群の値をそのままモノイドとして使ってよい。そういう扱いを、言語の側で認める仕組みを指します。

この扱いのことを、専門用語では 包摂的部分型付け（subsumptive subtyping）と呼びます。

「包摂」とは、一方が他方を含んでいることです。 群はモノイドの条件をすべて満たすのだから、群であるものは同時にモノイドでもある。その包み込みの関係を、そのまま型の関係として認める、ということです。

Lean、Rocq／Coq、Agda は、この 包摂的部分型付け を避けてきたのです。

避けてきた、とはどういうことなのかは、このすぐあとで解説します。

２つ目 ── 顕在フィールド

避けてきた仕組みの２つ目は、顕在フィールド（manifest fields）と呼ばれるものです。

これは何かというと、レコードの項目のうち、いくつかの値を定義の時点で確定させておく仕組み のことです。

レコードを定義した瞬間に確定した値は、レコード型の一部になります。既定値のように、あとから上書きできるものではありません。

「顕在」とは、隠れていないこと、外から見えていることを意味します。

通常のレコードでは、項目の値は「これから埋めるもの」です。値を作るときに、はじめて決まります。

顕在フィールドでは、その値が定義の側で決まっています。型を見ただけで、その項目の値が分かるのです。

	項目の値が決まる時点
通常の項目	値を作るとき
顕在フィールド	型を定義するとき

「避けてきた」とは、どういうことか

避けてきた、という言葉の意味ですが、上記の２つを、Lean、Rocq／Coq、Agda は言語の土台となる型理論には入れず、外側の仕組みで補ってきた、という意味です。

Arend 公式論文が、その点を述べています。

（原文引用）

The development of major theorem provers from MLTT family such as Lean, Coq and Agda has been avoiding subsumptive subtyping and manifest fields in the core theory thus making record types the same as sigma types. Subsumptive subtyping there is replaced with coercive subtyping A <c B in which case typechecker inserts an application c a : B of some function c : A → B whenever a term a : A is used in a context where a term of type B is expected.

（筆者による日本語訳）

Lean、Coq、Agda といった MLTT 系統の主要な定理証明支援系の開発は、中核理論において包摂的部分型付けと顕在フィールドを避けてきた。その結果、レコード型はシグマ型と同じものになっている。そこでは包摂的部分型付けが強制的部分型付け $A <_c B$ に置き換えられており、この場合、型 $B$ の項が期待される文脈で型 $A$ の項が使われるたびに、型検査器がある関数 $c : A \to B$ の適用 $c,a : B$ を挿入する。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・知らない言葉が出てきました。

専任講師：
順に説明します。

シグマ型とは何か

シグマ型とは、ふたつの値を組にした型です。数学で $\Sigma$ と書くことから、この名で呼ばれます。

Arend では \Sigma と記述します。

＜Arend のコード＞

\func Pair : \Type => \Sigma Nat Nat
\func p : Pair => (3, 5)

＜Haskell で書けば＞

type Pair = (Int, Int)
p :: Pair
p = (3, 5)

＜Arend の型検査結果＞

$ java -jar Arend.jar V4D.ard

--- Typechecking \default ---
[ ] src.V4D
--- Done (105ms) ---

Haskell のタプルにあたるものです。

ただし、依存型を持つ言語では、これ以上のことができます。 第１成分の値によって、第２成分の型が変わる組も作れます。「長さ $n$ のリスト」と「その $n$ 」を組にする、といった具合です。

そして、レコードとの違いです。

＜Arend のコード＞

\record RPair
  | fst : Nat
  | snd : Nat

\func r : RPair \cowith
  | fst => 3
  | snd => 5

シグマ型では、成分を位置で指します。第１成分、第２成分という具合です。

レコードでは、成分に名前が付いています。fst、snd と呼び分けられます。

引用文にある「レコード型はシグマ型と同じもの」という表現は、「名前が付いているだけで、それ以上のことはできない」という意味です。

強制的部分型付けとは何か

引用文に、強制的部分型付け（coercive subtyping）という語が出てきました。

包摂的部分型付けとの違いを述べます。

包摂的部分型付けでは、群の値はそのままモノイドとして通ります。何も足されません。

強制的部分型付けでは、群からモノイドへ変換する関数が用意されます。そして、群の値をモノイドとして使おうとするたびに、型検査器がその変換関数を自動で挿入します。

	群の値をモノイドとして使うとき
包摂的部分型付け	そのまま通る。何も挿入されない
強制的部分型付け	変換関数が自動で挿入される

書く側から見れば、どちらも「変換を自分で書かなくてよい」点は同じです。

違うのは、言語の土台がどう扱っているかです。強制的部分型付けでは、変換が明示的な項として残ります。

本記事で参照する Arend 公式論文の対比では、Lean、Rocq／Coq、Agda の主要な方式は、こちらの側として説明されています。

タロウくん：
・・・書く側から見れば、違いがないのですね。

専任講師：
簡単な場面ではそうです。しかし、階層が深くなると差が出ます。

そこは、第５部で見ましょう。

宇宙とは何か

タロウくん：
先生、コードに \Set0 という記号が出てきます。これは何ですか。

専任講師：
宇宙の名前です。

タロウくん：
宇宙、ですか。

専任講師：
過去記事で解説済みですが、ここで改めて解説します。

型にも、型がある

Haskell で 3 の型は Int でした。では、Int の型は何でしょうか。

タロウくん：
・・・型に、型があるのですか。

専任講師：
あります。Haskell では * と記述します。種、あるいは kind と呼ばれます。

＜Haskell のコード＞

Int :: *
Bool :: *

この「型を集めた場所」を、Arend では宇宙と呼びます。

通常の型理論では、宇宙は１つの数で並ぶ

専任講師：
Agda では、宇宙が１列に並んでいます。

$$\mathrm{Type}_0 : \mathrm{Type}_1 : \mathrm{Type}_2 : \cdots$$

Nat や Bool は $\mathrm{Type}_0$ に属し、その $\mathrm{Type}_0$ 自身は $\mathrm{Type}_1$ に属します。

タロウくん：
・・・階層が積み上がっている。

専任講師：
この数を、宇宙のレベルと呼びます。

Arend では、もう１つの軸が加わる

専任講師：
Arend の宇宙は、２つの数で指定されます。

（原文引用）

In Arend universes Type (n, k) are also parameterized by the homotopy level k (apart from the usual predicative level n).

（筆者による日本語訳）

Arend では、宇宙 Type (n, k) は、通常の可述的レベル n とは別に、ホモトピーレベル k によっても径数づけられている。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
２次元の表のようなものですか。

専任講師：
そう考えてよいです。縦軸が大きさ、横軸がホモトピーレベルです。

タロウくん：
・・・「大きさ」とは何のことですか。

縦軸の「大きさ」とは何か

専任講師：
言葉のとおり、集まりの大きさです。

タロウくん：
何の集まりですか。

専任講師：
型の集まりです。順に見ていきましょう。

まず、Nat という型があります。この中身は、$0, 1, 2, \ldots$ という数です。

タロウくん：
はい。

専任講師：
次に、Nat や Bool や String を、すべて集めたものを考えます。

タロウくん：
・・・型を集めたもの。

専任講師：
それが \Set0 です。

Nat の中身は数でした。\Set0 の中身は、型そのものです。

タロウくん：
・・・\Set0 のほうが、扱っているものが大きい。

専任講師：
そこが「大きさ」です。

なぜ、階層に分ける必要があるのか

タロウくん：
なぜ、階層に分けるのですか。すべての型をひとつに集めれば済むのでは。

専任講師：
そうすると、体系が壊れます。

タロウくん：
壊れる、といいますと。

専任講師：
「すべての型を集めたもの」自身も、型です。

タロウくん：
・・・ということは、その集まりのなかに入る。

専任講師：
自分自身を含んでしまうのです。

「自分自身を含まない集合の集合」を考えると矛盾が出る、という話をご存じでしょうか。

タロウくん：
ラッセルのパラドックスですね。

専任講師：
型理論でも、同じ形の矛盾が生じます。

そして矛盾が出ると、どんな主張でも証明できてしまいます。 証明支援系として使えなくなるのです。

タロウくん：
・・・だから、自分自身に入れないようにする。

専任講師：
１つ上の階層に置きます。

実際に確かめる

専任講師：
Arend で試してみましょう。

＜Arend のコード＞

-- 個々の型は、最下層に入る
\func a1 : \Set0 => Nat

-- 「\Set0 の型をすべて集めたもの」は、1つ上に入る
\func a2 : \1-Type1 => \Set0

-- さらに上へ
\func a3 : \1-Type2 => \Set1

＜Arend の型検査結果＞

$ java -jar Arend.jar V4G.ard

--- Typechecking \default ---
[ ] src.V4G
--- Done (87ms) ---

型検査を通過します。

タロウくん：
・・・\Set0 が、\1-Type1 に入っている。

専任講師：
大きさが１つ上がっています。

では、自分自身に入れようとするとどうなるか。

＜Arend のコード＞

\func bad : \Set0 => \Set0

＜Arend の型検査結果＞

$ java -jar Arend.jar V4M.ard

[ERROR] src.V4M:1:22: Type mismatch
  Expected type: \Set0
    Actual type: \1-Type1
  In: \Set0

弾かれます。

タロウくん：
・・・「\Set0 を期待したが、実際は \1-Type1 だった」。

専任講師：
処理系が、階層を守っているのです。

名簿にたとえると

タロウくん：
・・・もう少し、イメージが欲しいです。

専任講師：
名簿にたとえます。

社員名簿があるとします。そこには、社員の名前が並んでいます。

タロウくん：
はい。

専任講師：
次に、社内にある名簿を、すべて集めた一覧を作ります。

社員名簿、備品台帳、取引先一覧。それらの名前が並んだ「名簿の名簿」です。

タロウくん：
・・・扱っている単位が、一段上がっている。

専任講師：
さらに、その一覧を集めた一覧も作れます。

タロウくん：
・・・いくらでも上に行ける。

専任講師：
そして、「名簿の名簿」に自分自身を載せると、おかしなことになります。

タロウくん：
自分を含む名簿。

専任講師：
そこを禁じているのが、大きさの階層です。

階層	名簿のたとえ	型理論では
最下層	社員名簿。中身は人	`Nat`。中身は数
１つ上	名簿の一覧。中身は名簿	`\Set0`。中身は型
さらに上	一覧の一覧	`\Set1`。中身は `\Set0` の型

Haskell との違い

タロウくん：
Haskell では、こういう階層がありませんね。

専任講師：
* の１つだけです。

＜Haskell のコード＞

Int :: *
Bool :: *

そして、* 自身の型を問う手段がありません。

タロウくん：
・・・そこで止まっている。

専任講師：
Haskell では、型のレベルで数学の議論を組み立てないからです。

証明支援系では、「すべての集合について〜」といった主張を扱います。そのとき、階層が必要になるのです。

「可述的」という語について

専任講師：
論文では、この縦軸を「可述的レベル」と呼んでいます。

可述的（predicative）とは、「自分自身を含む集まりについて語ることを禁じる」立場のことです。

タロウくん：
・・・いま扱った階層のことですね。

専任講師：
そのとおりです。本記事では「大きさ」と呼びます。

タロウくん：
では、横軸は。

横軸のホモトピーレベルとは何か

専任講師：
第３回目の記事で扱った「等しさの根拠が何本あるか」です。

過去記事で解説済みですが、ここで改めて解説します。

3 = 3 という等しさの根拠は、実質１本でした。何通りに書いても、それらは互いに等しくなります。

一方、Bool = Bool の根拠は２本ありました。 何も変えない対応と、true と false を入れ替える対応です。

タロウくん：
・・・型によって、根拠の本数が違う。

専任講師：
その違いを、階層に分けたものがホモトピーレベルです。

名前	ホモトピーレベル	意味
`\Prop`	$-1$	要素が高々１つしかない型
`\Set0`	$0$	等しさの根拠が高々１本の型
`\1-Type0`	$1$	等しさの根拠どうしの等しさが、高々１本
`\2-Type0`	$2$	その等しさどうしの等しさが、高々１本
`\3-Type0`	$3$	さらにその等しさどうしの等しさが、高々１本
`\4-Type0`	$4$	さらにもう１段、等しさを重ねたものが高々１本
`\5-Type0`	$5$	さらにもう１段、等しさを重ねたものが高々１本

タロウくん：
・・・「等しさの等しさの等しさ」と、どこまでも続くのですか。

専任講師：
続きます。ただし、多くの数学では \Set0 までで足ります。

２つの軸を、表にすると

縦が大きさ、横がホモトピーレベルです。

	レベル $-1$	レベル $0$	レベル $1$	レベル $2$	レベル $3$	レベル $4$	レベル $5$
大きさ 0	`\Prop`	`\Set0`	`\1-Type0`	`\2-Type0`	`\3-Type0`	`\4-Type0`	`\5-Type0`
大きさ 1	──	`\Set1`	`\1-Type1`	`\2-Type1`	`\3-Type1`	`\4-Type1`	`\5-Type1`
大きさ 2	──	`\Set2`	`\1-Type2`	`\2-Type2`	`\3-Type2`	`\4-Type2`	`\5-Type2`
大きさ 3	──	`\Set3`	`\1-Type3`	`\2-Type3`	`\3-Type3`	`\4-Type3`	`\5-Type3`
大きさ 4	──	`\Set4`	`\1-Type4`	`\2-Type4`	`\3-Type4`	`\4-Type4`	`\5-Type4`
大きさ 5	──	`\Set5`	`\1-Type5`	`\2-Type5`	`\3-Type5`	`\4-Type5`	`\5-Type5`

表は、上にも右にも続きます。ここでは５までを示しました。

タロウくん：
・・・名前の付け方に、規則がありますね。

専任講師：
\n-Type p の n がホモトピーレベル、p が大きさです。

\1-Type1 なら、ホモトピーレベル１、大きさ１。表の２行目、３列目です。

タロウくん：
\Set0 と \Set1 は。

専任講師：
\Set は、ホモトピーレベル０の別名です。

\Set p は \0-Type p と同じものを指します。

同じように、\Prop はホモトピーレベル $-1$ の別名です。

タロウくん：
・・・\Prop の列だけ、大きさの欄が空いています。

専任講師：
\Prop には、大きさの階層がありません。

「すべての命題について〜」という主張も、そのまま \Prop に入ります。上の階層へ上がらないのです。

タロウくん：
・・・だから１つしかない。

専任講師：
そういうことです。

レベルの数は、有限か無限か

タロウくん：
先生、確かめさせてください。

このレベルの数は、無限に存在するのですか。それとも、どこかで打ち止めになるのですか。

専任講師：
どちらの軸も、上限がありません。

タロウくん：
・・・両方とも、無限に続く。

専任講師：
大きさのほうから説明します。

Nat は最下層に入ります。「最下層の型をすべて集めたもの」は、１つ上の階層に入ります。その「１つ上の階層の型をすべて集めたもの」は、さらに上へ行きます。

タロウくん：
・・・集めるたびに、上がっていく。

専任講師：
集める操作は、いつでも繰り返せます。だから、上限がありません。

タロウくん：
ホモトピーレベルのほうは。

専任講師：
こちらも同じです。

型があれば、その上に等しさの型があります。等しさの型があれば、さらにその上に「等しさどうしの等しさ」の型があります。

タロウくん：
・・・いくらでも積み上げられる。

専任講師：
そのとおりです。

どのレベルにも収まらない型もあります

専任講師：
もうひとつ、述べておくべきことがあります。

どのホモトピーレベルにも収まらない型が存在します。

タロウくん：
・・・無限に階層があるのに、どこにも入らない。

専任講師：
等しさを何回重ねても、「高々１本」に落ち着かない型があるのです。

（原文引用）

We say that a type is of homotopy level ∞ if no such k exists.

（筆者による日本語訳）

そのような k が存在しないとき、その型はホモトピーレベル無限大であるという。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
どんな型が、そうなるのですか。

専任講師：
第５回目の記事で扱う円周が、その例です。

円周の上では、一周する道、二周する道、三周する道と、いくらでも違う道が作れます。そして、その道どうしの関係も無限に増えていきます。

タロウくん：
・・・どこかで打ち止めにならない。

専任講師：
そういう型は、表のどのマスにも入りません。

実際に使うのは、どのあたりか

タロウくん：
・・・無限にあると言われても、実感が湧きません。

専任講師：
実際に使うのは、左のほうです。

よく使う場所	何に使うか
`\Prop`	「正しい」という主張。真偽値のかわり
`\Set0`	自然数、整数、文字列など、普通のデータ
`\Set1`	「集合をすべて集めたもの」。圏を定義するときなど
`\1-Type1`	圏そのもの

タロウくん：
・・・レベル２より先は。

専任講師：
通常の数学では、ほとんど使いません。

高次の圏論やホモトピー論を扱うときに、はじめて必要になります。本記事で扱う代数構造の階層は、\Prop と \Set0 と \Set1 で足ります。

それで、何が嬉しいのか

タロウくん：
・・・２つの軸があると、何が嬉しいのですか。

専任講師：
証明を持ち回らずに済みます。

タロウくん：
持ち回る、といいますと。

専任講師：
コードで見比べましょう。

まず「集合である」ということを、そのまま書いてみます。

＜Arend のコード＞

-- 「集合である」＝ 等しさの根拠が高々1本
\func isSet (A : \Type) => \Pi {x y : A} (p q : x = y) -> p = q

x = y の根拠 p と q があったとき、その２つが必ず等しくなる。 それが「集合である」ということです。

タロウくん：
はい。

専任講師：
Agda では、この証明を引数として受け取ることになります。

＜Arend で、Agda の方式を再現すると＞

-- 集合であることの証明 s を、引数として受け取る
\func useAgdaStyle (A : \Type) (s : isSet A) {x y : A} (p q : x = y) : p = q
  => s p q

引数に s : isSet A が並んでいます。 これが「A は集合である」という証明です。

タロウくん：
・・・毎回、渡すのですか。

専任講師：
そこが問題です。別の補題を作ると、また渡すことになります。

＜Arend で、Agda の方式を再現すると＞

-- さらに別の補題でも、s を渡し続けることになる
\func useAgdaStyle2 (A : \Type) (s : isSet A) {x y : A} (p q : x = y) : p = q
  => useAgdaStyle A s p q

＜Arend の型検査結果＞

$ java -jar Arend.jar V4H.ard

--- Typechecking \default ---
[ ] src.V4H
--- Done (114ms) ---

タロウくん：
・・・s が、あちこちに現れています。

専任講師：
補題を10個作れば、10箇所に書くことになります。

タロウくん：
・・・それが「持ち回る」ということですか。

専任講師：
そうです。証明を、荷物のように持ち歩くことになります。

Arend では、型そのものに書かれている

専任講師：
Arend では、\Set0 と書くだけで済みます。

＜Arend のコード＞

-- Nat は \Set0 に属する
\func natIsSet0 : \Set0 => Nat

型検査を通過します。

タロウくん：
・・・Nat が \Set0 に属している、と書いただけ。

専任講師：
そして \Set0 に属していれば、「等しさの根拠が高々１本である」ことは型の側で決まっています。

証明を引数に取る必要がありません。

タロウくん：
・・・荷物を持たずに済む。

専任講師：
そこが、２つの軸を持つことの効き目です。

（原文引用）

This allows a single polymorphic definition to be instantiated across universes of varying homotopy level, including Prop, Set n, and the universes of all types Type n.

（筆者による日本語訳）

これにより、単一の多相的な定義を、Prop、Set n、およびすべての型の宇宙 Type n を含む、さまざまなホモトピーレベルの宇宙にわたって具体化できる。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・ひとつ書けば、いろいろな場所で使える。

専任講師：
そこは第６回目の記事で詳しく扱います。本記事では、\Set0 と \Prop が宇宙の名前であることを押さえておけば十分です。

型理論の宇宙と、集合論の宇宙

タロウくん：
先生、そもそも「宇宙」という呼び方が気になります。

専任講師：
日常の宇宙とは、まったく別のものです。

ただし、この呼び名には由来があります。

タロウくん：
由来、ですか。

専任講師：
集合論にも「宇宙」という概念があるのです。

集合論の宇宙

専任講師：
グロタンディーク宇宙と呼ばれます。

タロウくん：
・・・グロタンディーク。

専任講師：
20世紀の数学者アレクサンドル・グロタンディークが導入したものです。

圏論を扱うとき、「すべての集合の集まり」を考えたくなる場面があります。しかし、そのまま考えると矛盾が出ます。

タロウくん：
・・・先ほどのラッセルのパラドックスですね。

専任講師：
そこで、大きさを制限した集まりを用意しました。それがグロタンディーク宇宙です。

同じ動機から生まれている

タロウくん：
型理論の宇宙と、関係があるのですか。

専任講師：
動機は同じです。どちらも、ラッセルのパラドックスを避けるために作られました。

そして、どちらも階層をなします。

$U : U' : U'' : U''' : \cdots$

タロウくん：
・・・先ほど見た表と、同じ形です。

専任講師：
発想は共通しています。

しかし、置かれている場所が違う

タロウくん：
では、違いは何ですか。

専任講師：
どこに置かれているか、です。

集合論では、宇宙の存在を公理として追加します。

タロウくん：
公理として、というのは。

専任講師：
集合論の基本規則には、宇宙は含まれていません。 必要になったら、「そういうものが存在する」と外から足すのです。

タロウくん：
・・・後から付け足す。

専任講師：
そして、この追加は軽いものではありません。

グロタンディーク宇宙が存在するという主張は、到達不能基数という、非常に大きな数の存在と同じ強さを持ちます。

タロウくん：
・・・重い仮定なのですね。

専任講師：
一方、型理論の宇宙は、体系の内部に組み込まれた構文上の階層です。

集合論の側では公理として追加するものが、型理論では言語の一部として最初から備わっています。

タロウくん：
・・・外から足すか、最初から入っているか。

専任講師：
そこが違いです。

Arend で \Set0 と記述できるのは、その階層が言語の文法に含まれているからです。

並べると

	集合論	型理論
呼び名	グロタンディーク宇宙	宇宙（universe）
動機	ラッセルのパラドックスの回避	同じ
階層をなすか	なす	なす
どこにあるか	公理として、外から追加する	言語の一部として、最初から備わる
存在の重さ	到達不能基数の存在と同じ強さ	文法の一部

タロウくん：
・・・同じ問題に、別のやり方で答えている。

専任講師：
そう捉えていただければ十分です。

本記事では、宇宙の理論そのものには踏み込みません。

\Prop、\Set0、\Set1 という名前が、「型が置かれる場所」を指していると押さえておけば、以降の議論は追えます。

詳しくは、第６回目の記事で扱います。

顕在フィールドは、代数構造を定義する上でどう役立つのか

顕在フィールド は、代数構造を定義する上でどう役立つのかを理解するために、半環と環の関係を例に挙げることにします。

半環とは何か

半環とは、足し算と掛け算のふたつの演算を持つ構造です。ただし、引き算にあたる操作を備えていません。

自然数がその例になります。$0, 1, 2, \ldots$ という数の集まりです。

足し算と掛け算はできます。しかし $3 - 5$ を計算しようとすると $-2$ になり、自然数の外に出てしまいます。

環との違いは、足し算の逆元を要求するかどうかです。環は要求し、半環は要求しません。

	足し算	掛け算	足し算の逆元
半環	できる	できる	要求しない
環	できる	できる	要求する

半環の定義に、掛け算の公理が入っている

ところで、半環の定義 には、$0 \times x = 0$ という等式が、公理として 含まれています。掛け算についての性質でありながら、公理として置かれている のです。

タロウくん：
なぜ、公理にする必要があるのですか？

専任講師：
半環では、$0 \times x = 0$ という等式を導くことができないからです。

環になると、事情が変わります。環は半環に足し算の逆元を加えたものですから、次のように進めることができます。

$$0 \times x = (0 + 0) \times x = 0 \times x + 0 \times x$$

両辺から $0 \times x$ を引けば、$0 = 0 \times x$ が残ります。逆元があるので、この引き算ができます。

タロウくん：
・・・環では、公理として置く必要がない。

専任講師：
ところが、ここで面倒が生じます。

環を半環の拡張として定義したいのですが、半環には、$0 \times x = 0$ という項目が残っています。

環では導けるのだから 公理として要求したくない。それでも、拡張である以上、その項目を空欄のままにはできません。

ここで、顕在フィールドが、この空欄を埋める手段になります。

＜Arend のコード＞

\class Semiring \extends AbMonoid, Monoid {
  | ldistr {x y z : E} : x * (y + z) = x * y + x * z
  | rdistr {x y z : E} : (x + y) * z = x * z + y * z
  | zro_*-left {x : E} : zro * x = zro
  | zro_*-right {x : E} : x * zro = zro
}

\class Ring \extends Semiring, AbGroup {
  | zro_*-left {x} => {?}   -- 0 * x = 0 の証明。逆元を使って導ける
  | zro_*-right {x} => {?}  -- x * 0 = 0 の証明
}

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"（Arend 公式論文に掲載されているコードです）

タロウくん：
先生、確かめさせてください。

このコードでは、どこの顕在フィールドを、どの値で埋めているのですか？

専任講師：
２箇所です。
表にします。

埋めている場所	何を埋めているか
`Ring` の `zro_*-left`	$0 \times x = 0$ の証明
`Ring` の `zro_*-right`	$x \times 0 = 0$ の証明

タロウくん：
・・・どちらも、Semiring から継承したフィールドですね。

専任講師：
Semiring の側では、次のように宣言されています。

| zro_*-left {x : E} : zro * x = zro

コロン : の後ろにあるのは、型です。
「$0 \times x = 0$ である」という主張を表しています。

タロウくん：
・・・型だけを宣言して、中身は決めていない。

専任講師：
Semiring を作るときには、この証明を渡す必要があります。
半環では導けないので、外から与えるしかありません。

タロウくん：
では、Ring の側は？

専任講師：

| zro_*-left {x} => {?}

=> の後ろにあるのが、埋めた中身です。

タロウくん：
・・・{?} になっています。

専任講師：
論文では、証明の中身を省略して {?} と書いています。
実際のコードでは、ここに逆元を使った証明が入ります。

タロウくん：
・・・埋めている場所は分かりました。

では、どの値で埋めているのですか。

専任講師：
値といっても、数ではありません。
$0 \times x = 0$ という等式の証明そのものです。

第２部で見た assoc と同じです。
結合律のフィールドには、結合律の証明を渡しました。

タロウくん：
・・・証明が、値として入っている。

専任講師：
そして、その証明は環の側で作ることができます。
逆元があるからです。

タロウくん：
・・・半環では作れなかったものが、環では作れる。
だから埋められる。

専任講師：
Semiring の zro_*-left は、公理として置かれたフィールドです。
そして Ring の側では、同じ名前に => を付けて中身を与えています。

この => が 顕在フィールド であり、半環から継承したフィールドを、環の側で埋めている のです。

タロウくん：
・・・継承したフィールドを埋めながら、階層を積み上げていく。

専任講師：
顕在フィールドがなければ、そうはいきません。

論文が、その場合に何が起きるかを述べています。

（原文引用）

Without manifest fields, in bundled or unbundled case, typically one has to define more of the small, atomic records and combine them to define various composite records, the option of constructing composite records as specializations of other composite records becomes unavailable.

（筆者による日本語訳）

顕在フィールドがなければ、束ねた場合でも束ねない場合でも、通常はより多くの小さく原子的なレコードを定義し、それらを組み合わせてさまざまな複合レコードを定義することになる。複合レコードを、別の複合レコードの特殊化として構成するという選択肢が使えなくなるのである。

出典：同上

タロウくん：
環を半環の特殊化として書くのではなく、小さなレコードを集めて作り直す。

専任講師：
モノイド、群、環、体と階層が深くなるほど、その作り直しが積み重なります。

なぜ避けてきたのか

Lean、Rocq／Coq、Agda が、包摂的部分型付けと顕在フィールドを避けてきた理由については、筆者が調べた範囲では、一次資料で確認できませんでした。

各処理系の開発チームが理由を述べた資料も、見つかりませんでした。

ただし、型理論の文献には、関連する議論があります。

（原文引用）

we shall analyse them from a particular angle, discussing the idea that subsumptive subtyping is suitable for type assignment systems as employed in functional programming languages, but not suitable for type theories with canonical objects as implemented in proof assistants, and showing that coercive subtyping provides a very general framework for the latter.

（筆者による日本語訳）

我々はある特定の角度からこれらを分析し、次の考えを論じる。包摂的部分型付けは、関数型プログラミング言語で用いられるような型割当ての体系には適しているが、定理証明支援系で実装されるような、正準的対象を持つ型理論には適していない。そして、強制的部分型付けが後者に対して非常に一般的な枠組みを提供することを示す。

出典：Z. Luo, S. Soloviev, T. Xue, "Coercive subtyping: Theory and implementation", Information and Computation, vol. 223, 2013年, pp. 18–42

正準的対象とは何か

引用文に、正準的対象 という語が出てきました。

第３回目の記事で扱った正準性と、関係のある概念です。

正準的対象とは、その型の値として最も基本的な形をしたもののことです。

自然数でいえば、zero と「１を足す」だけで作られた形がそれにあたります。$2 + 3$ を計算して得られる 5 は正準形であり、5 そのものが正準的対象です。

「正準的対象を持つ型理論」とは、値がこうした基本的な形へ計算されることを前提とする型理論を指します。

Arend、Agda、Lean、Rocq／Coq は、いずれもこの系統に属します。

引用文は、そうした型理論に包摂的部分型付けは向かない、と論じています。

タロウくん：
・・・定理証明支援系には向かない、と述べられている。

専任講師：
そして Lean・Rocq／Coq・Agda が採っているのは、この引用文でいう強制的部分型付けのほうです。

タロウくん：
Arend は、向かないとされたほうを選んだ。

専任講師：
そう読めます。

ここで、２点、大事なことをお伝えしないといけません。

第１に、この論文は Lean・Rocq／Coq・Agda の設計判断について述べたものではないということです。

これらの各言語の開発チームが、この議論を理由に避けたのかどうかは確認できていません。

第２に、Arend 公式論文が、この議論に応答しているかどうかも確認できませんでした。

タロウくん：
・・・つながりは、筆者の推測にすぎない。

専任講師：
そのとおりです。

包摂的部分型付けを選んだ弊害は、何だったのか

タロウくん：

Arend は、定理証明支援系です。
それなのに定理証明支援系に向かないとされる選択肢を選んでしまった。

このことがもたらす弊害は、第２回目の記事で扱った、Arend は計算しきる能力を犠牲にした、ということですか？

証明や反証さえできれば、具体的な数は算出できなくても実務上の弊害にはならない、と。

専任講師：
鋭いところを突かれましたが、その２つは別の話です。

順に分けて答えます。

Arend が正準性を持たない理由

公式論文が、はっきり書いています。

（原文引用）

However, it lacks sufficient computational rules to render the theory fully computational: the MLTT property that every closed term of type Nat evaluates to a canonical number does not hold in Arend.

（筆者による日本語訳）

しかし、その理論を完全に計算可能にするだけの計算規則を欠いている。すなわち、Nat 型のすべての閉じた項が正準的な数へ評価されるという MLTT の性質は、Arend では成り立たない。

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・「計算規則を欠いている」。

専任講師：
この文が置かれているのは、区間型と一価性について述べた箇所 です。

一価性を扱う iso という操作に、計算規則が十分に備わっていない。それが理由だと述べられています。

タロウくん：
・・・ 包摂的部分型付けの話ではないですね。

専任講師：
論文のなかで、正準性を持たない理由として包摂的部分型付けを挙げた記述は、筆者が調べた範囲では見つかりませんでした。

結局、包摂的部分型付けを採用したことによる弊害はなにか

タロウくん：
では、包摂的部分型付けを選んだことの弊害は、何なのですか。

専任講師：
そこが、確認できなかった点です。

先ほど引いた論文は、「包摂的部分型付けは、正準的対象を持つ型理論には適していない」 と述べています。

しかし、その引用文だけでは、具体的に何が起きるのかが分かりません。

タロウくん：
・・・「適していない」としか書かれていない。

専任講師：
そして、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 の型理論は、その計算的側面を高めるように調整できる可能性がある。しかし形式化における実践的な経験は、そのような強化の必要性を大きくは示していない。

出典：同上

タロウくん：
・・・実践では必要とされなかった、と。

専任講師：
ただし、これは 計算可能性をめぐっての記述 です。

包摂的部分型付けを選んだことについて、同じように「実践では問題にならなかった」と述べた記述は、筆者が調べた範囲では見つかりませんでした。

整理すると

#	内容	判定
①	Arend が正準性を持たない理由は、一価性の計算規則が不完全なこと	公式論文に記載あり
②	正準性を持たない理由が包摂的部分型付けであること	記載が見つからなかった
③	包摂的部分型付けが Arend にもたらす具体的な弊害	確認できなかった
④	計算可能性は、形式化の実践では必要とされなかった	公式論文に記載あり
⑤	包摂的部分型付けについても同様に問題なかったかどうか	記載が見つからなかった

タロウくん：
・・・①と④は確かめられている。②と③と⑤は、確かめられていない。

専任講師：
そこを混同しないことが大事です。

「定理証明支援系に向かないとされる選択肢を選んだ」という事実と、「だから正準性を失った」という因果は、別のものです。

後者を裏づける資料は、見つかりませんでした。

型理論の文献に、包摂的部分型付けを定理証明支援系に用いることへの否定的な議論が存在する。

そして、Arend は、それを土台に組み込んだ。

これが確認できた事実です。

結果として、何が起きるのか

議論を戻しましょう。

結論として、Lean、Rocq／Coq、Agda を使って数学の階層構造を書くときには、外側で手当てをすることになります。

Lean、Rocq／Coq、Agda では、群の値をモノイドとして渡したいとき、変換のための関数を別に用意するか、型クラスの仕組みを使って、処理系に探させます。

言い換えると、群の値をモノイドとして渡したいとき、型検査器が変換のための関数を自動で挿入します。

言語の中核が「群はモノイドの一種である」と認めているわけではありません。

第５部 ── Arend は、包摂的部分型付けと顕在フィールドを Arend 自身の土台に組み込みました

まず、包摂的部分型付けです

＜Arend のコード＞

\data Bool | true | false

\func notB (b : Bool) : Bool \elim b
  | true => false
  | false => true

\func xor (x y : Bool) : Bool \elim x
  | true => notB y
  | false => y

-- モノイド：演算と単位元を持つ
\record Monoid (A : \Type)
  | unit : A
  | op : A -> A -> A

-- 群：モノイドを拡張し、逆元を加える
\record Group \extends Monoid
  | inv : A -> A

-- Bool と xor は群をなす
\func BoolXor : Group \cowith
  | A => Bool
  | unit => false
  | op => xor
  | inv => \lam x => x

-- モノイドを受け取る関数
\func twice {A : \Type} (M : Monoid A) (x : A) : A => Monoid.op {M} x x

-- 群 BoolXor を、そのままモノイドとして渡せる
\func t : Bool => twice BoolXor true
\func c : t = false => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar V4B.ard

--- Typechecking \default ---
[ ] src.V4B
--- Done (203ms) ---

コードを読み解く

まず、xor という演算を定義しています。

xor は排他的論理和です。２つの値が違えば true、同じなら false を返します。

`x`	`y`	`xor x y`
`true`	`true`	`false`
`true`	`false`	`true`
`false`	`true`	`true`
`false`	`false`	`false`

この演算と false を組み合わせると、群になります。

群の条件	`Bool` と `xor` では
単位元がある	`false`。何と組み合わせても相手を変えない
逆元がある	自分自身。`xor x x` は必ず `false` になる

タロウくん：
・・・自分が自分の逆元になっている。

専任講師：
そのとおりです。だから inv => \lam x => x と記述できます。

拡張の宣言

\record Group \extends Monoid が、「群はモノイドを拡張したものである」 という宣言です。

Haskell でいえば、次のような形にあたります。

＜Haskell で書けば＞

class MyMonoid a => MyGroup a where
  inv :: a -> a

そして、ここからが違います。

群を、そのままモノイドとして渡せる

twice は Monoid を受け取る関数です。

\func twice {A : \Type} (M : Monoid A) (x : A) : A => Monoid.op {M} x x

受け取った M の演算を使って、x を２回組み合わせています。

そして、次の行で 群である BoolXor をそのまま渡すことができています。

\func t : Bool => twice BoolXor true

変換のための関数は書いていません。

言語が「群はモノイドの一種である」と認めているためです。

結果を確かめる

\func c : t = false => idp

xor true true は false になります。その結果を、idp で確かめています。

タロウくん：
・・・型検査が通ったということは、結果が false になっている。

専任講師：
処理系が計算して、確かめたということです。

次に、顕在フィールドです

＜Arend のコード＞

\record Point
  | x : Nat
  | y : Nat

-- y を 0 に固定したレコード
\record OnAxis \extends Point
  | y => 0

\func p1 : OnAxis \cowith
  | x => 5

\func checkY : OnAxis.y {p1} = 0 => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar V4C.ard

--- Typechecking \default ---
[ ] src.V4C
--- Done (115ms) ---

コードを読み解く

Point は、平面上の点を表すレコードです。 x と y の２つの座標を持ちます。

OnAxis は、その y を 0 に固定したものです。

\record OnAxis \extends Point
  | y => 0

| y => 0 が、顕在フィールドです。

通常の項目なら | y : Nat と書きます。型を指定するだけです。

顕在フィールドでは | y => 0 と書きます。値そのものを与えます。

書き方	意味
`\| y : Nat`	`y` は自然数である。値は、あとで決める
`\| y => 0`	`y` は `0` である。もう決まっている

値を作るとき

\func p1 : OnAxis \cowith
  | x => 5

x だけを与えています。y は渡していません。

タロウくん：
・・・y は、もう決まっているから。

専任講師：
そのとおりです。
定義の時点で 0 に確定しています。

タロウくん：
先生、確かめさせてください。

座標が $(5, 0)$ になるのは、p1 ですか？
それとも OnAxis ですか？

専任講師：
OnAxis は型で、p1 はその型の値です。

	何か	何を表すか
`OnAxis`	型	$y$ が $0$ である点、全体
`p1`	値	そのうちの、$x$ が $5$ である点

OnAxis は $(x, 0)$ という形の点をすべてまとめたものです。
$x$ は決まっていません。

p1 は、その x に 5 を与えたものです。

タロウくん：
・・・$x$ 軸の上に乗っている点、すべてが OnAxis。

専任講師：
そして p1 は、そのうちのひとつです。

x に 5 を与えたので、$(5, 0)$ になります。

実際に取り出してみます。

＜Arend のコード＞

\func px : Nat => Point.x {p1}
\func py : Nat => Point.y {p1}

\func c1 : px = 5 => idp
\func c2 : py = 0 => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar PT.ard

--- Typechecking \default ---
[ ] src.PT
--- Done (151ms) ---

型検査を通過します。

px が 5、py が 0。
それを idp で確かめています。

タロウくん：
・・・y を渡していないのに、0 が取り出せる。

専任講師：
顕在フィールドが、型の側で決めているからです。

\func checkY : OnAxis.y {p1} = 0 => idp

p1 の y は 0 である。それが idp で確かめられます。

既定値との違い

タロウくん：
・・・オブジェクト指向言語の既定値と、どう違うのですか？

専任講師：
既定値は、あとから上書きできます。

顕在フィールドは、上書きできません。
型の一部になっているからです。

タロウくん：
・・・OnAxis と書いた時点で、y が 0 であることが決まっている。

専任講師：
「y が 0 である Point」 という、別の型なのです。

継承したフィールドの型を、より具体的な型に置き換えることができる

もうひとつ、Arend のレコード には、できることがあります。

レコードを拡張するとき、継承したフィールドの型を、より具体的な型に置き換えることができる、という機能です。

タロウくん：
・・・型を置き換える、ですか？

専任講師：
身近な例で説明します。

郵便の宛先で考える

「宛先」というフィールドを持つレコードがあるとします。
宛先の型は「文字列」です。

タロウくん：
住所を文字列で持つ、ということですね。

専任講師：
そういうことです。
次に、社内便のレコードを作りたいとします。

社内便の宛先は、社内の部署に限られます。

タロウくん：
・・・文字列であることに変わりはないが、対象が限られている。

専任講師：
そこで「宛先」の型を、文字列から部署へ置き換えます。

継承したフィールドの名前はそのまま。型だけを限定する のです。

タロウくん：
・・・ レコードを一から作り直さなくてよい。

専任講師：
この機能について、Arend 公式論文では以下のように説明されています。

（原文引用）

If D is an extension of C and x : A is a field of C then the type of the field x can be overriden in D and changed to a subtype B: x : B, B < A.

（筆者による日本語訳）

D が C の拡張であり、x : A が C のフィールドであるとき、D において x の型を部分型 B に上書きできる。

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・記号が並んでいて、分かりにくいです。

専任講師：
失礼しました。
表にまとめて整理してみますね。

引用文の記号	郵便の例では
`C`	継承元のレコード。宛先を持つ
`D`	拡張したレコード。社内便
`x`	フィールドの名前。宛先
`A`	もとの型。文字列
`B`	限定した型。部署
`B < A`	部署は、文字列の一種である

タロウくん：
・・・D において x の型を B に上書きする、というのは、この場合だと・・・

専任講師：
社内便 において、宛先の型を部署に置き換える 、ということです。

数学の例で見る

専任講師：

今度は、数学の写像の例で説明してみましょう。
この写像の例は、公式論文で挙げられているものです。

例えば、集合のあいだの写像を表すレコードがあるとします。
始域と終域という２つのフィールドを持ち、どちらも集合です。

始域とは、写像の出発点となる集まりです。
終域とは、行き先の集まりです。

タロウくん：
・・・$f : A \to B$ の $A$ と $B$ ですね？

専任講師：
そのとおりです。
数学では、写像を扱う場面が繰り返し現れます。

集合のあいだの写像。
モノイドのあいだの写像。
群のあいだの写像。
環のあいだの写像。

タロウくん：
・・・構造ごとに、写像がある。

専任講師：
個々の写像を考えるたびに、その都度、新しいレコードを定義していたら、同じようなコードを何度も書くことになります。

始域を持つ。
終域を持つ。
始域から終域への対応を持つ。

その骨組みは、どれも同じであるにもかかわらず。

タロウくん：
・・・違うのは、始域と終域が何であるか、だけですものね。

専任講師：
そうなんです。
このような場面で、Arendに備わっている 継承したフィールドの型を置き換える 機能が効果を発揮します。

集合の写像のレコードを１つ作っておく。
そのレコードを継承して、始域と終域の型だけを置き換える。

この手順です。

タロウくん：
・・・骨組みは使い回して、型だけを変える、という発想ですね。賢いです。

専任講師：
では、モノイドのあいだの写像はどうでしょうか。

タロウくん：
始域と終域が、集合ではなくモノイドになる。

専任講師：
そのとおりです。
集合の写像のレコードを拡張し、始域と終域の型をモノイドに限定します。

＜Arend のコード＞

\record SetHom
  | Dom : \Set0
  | Cod : \Set0
  | fun : Dom -> Cod

\record Monoid (A : \Set0)
  | unit : A
  | op : A -> A -> A

\record MonoidHom \extends SetHom
  | \override Dom : Monoid
  | \override Cod : Monoid

＜Arend の型検査結果＞

$ java -jar Arend.jar OV.ard

--- Typechecking \default ---
[ ] src.OV
--- Done (121ms) ---

\override が、その上書きです。

SetHom から継承した Dom と Cod の型を、Monoid に限定しています。

タロウくん：
この機能を使うと、写像のレコードを、その都度、何度も書き直さなくてよくなりますね。

専任講師：
便利さに気付いたようですね。

土台となる写像のレコードは１つで済みます。

群の写像も、環の写像も、体の写像も。
すべて SetHom を拡張することで、作ることができるからです。

部分実装 ── 一部だけを埋めておく

部分実装とは、レコードの項目の一部だけを埋めて、残りを空けたままにしておくことです。

＜Arend のコード＞

\record Monoid (A : \Set0)
  | unit : A
  | op : A -> A -> A

-- A だけを埋めた中間の型
\record NatMonoid \extends Monoid
  | A => Nat

NatMonoid は、Monoid の A を Nat に固定したものです。
unit と op は、まだ埋まっていません。

そして、この 中間の型 から、複数のものを作っていくことができます。

＜Arend のコード＞

\func addM : NatMonoid \cowith
  | unit => 0
  | op => \lam x y => x Nat.+ y

\func mulM : NatMonoid \cowith
  | unit => 1
  | op => \lam x y => x Nat.* y

＜Arend の型検査結果＞

$ java -jar Arend.jar V4E.ard

--- Typechecking \default ---
[ ] src.V4E
--- Done (122ms) ---

自然数の足し算と掛け算、どちらもモノイドをなします。

共通する部分を NatMonoid にまとめ、残りだけを別々に埋めています。

タロウくん：
・・・Sum と Product を作るのと、似ています。

専任講師：
似ていますが、違うところ があります。

Haskell の Sum と Product は、中身が同じ Int でありながら、型としては別のものです。

取り出すときには、包みを外す必要があります。

Arend の addM と mulM は、どちらも Nat そのものを扱います。
包み直していません。

タロウくん：
・・・別の型を作らずに済んでいる。

専任講師：
その通りです。
そこは、このあと詳しく扱います。

匿名拡張 ── 名前を付けずに、その場で作る

匿名拡張（anonymous extension）とは、レコードを拡張した型を、名前を付けずにその場で作ることです。

先ほどの NatMonoid は、名前を付けて定義しました。匿名拡張では、その名前を省けます。

＜Arend のコード＞

\record Monoid (A : \Set0)
  | unit : A
  | op : A -> A -> A

-- 匿名拡張：名前を付けずに、その場で作る
\func f (M : Monoid { | A => Nat }) : Nat => Monoid.unit {M}

\func g : Monoid Nat 0 (\lam x y => x Nat.+ y) \cowith
\func h : Nat => f g
\func c : h = 0 => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar V4I.ard

--- Typechecking \default ---
[ ] src.V4I
--- Done (134ms) ---

Monoid { | A => Nat } が、匿名拡張です。

「A が Nat であるようなモノイド」という型を、その場で作っています。

タロウくん：
・・・NatMonoid という名前を、付けずに済んでいる。

専任講師：
名前を付ける必要があると、一度しか使わない型にも名前を考えることになります。

匿名拡張は、その手間を省きます。

レコードの引数とフィールドを区別しない

専任講師：
Arend では、同じ Nat に対して、足し算のモノイドと掛け算のモノイドを並べて記述することができます。

＜Arend のコード＞

\func natAdd : Monoid Nat 0 (\lam x y => x Nat.+ y) \cowith
\func natMul : Monoid Nat 1 (\lam x y => x Nat.* y) \cowith

タロウくん：
・・・newtype で包み直していませんね。

専任講師：
Monoid Nat 0 (足し算) と Monoid Nat 1 (掛け算) は、別々の型だから です。

タロウくん：
・・・型が違う。

専任講師：
単位元も演算も、型の一部になっています。
単位元が 0 か 1 か。演算が足し算か掛け算か。

そこが違えば、別の型 です。

タロウくん：
Haskell では、どちらも MyMonoid Int になってしまう。

専任講師：
型としては同じものになるので、足し算のモノイドと掛け算のモノイドを区別できません。だから newtype で包み直して、Sum と Product という別の型を作ることになります。

タロウくん：
・・・Arend では、包まなくても型が違う。

専任講師：
これができるのは、Arend が引数とフィールドを区別しないからです。

タロウくん：
引数とフィールド、ですか。

専任講師：
順に説明します。

レコードには、２通りの書き方がある

＜Arend のコード＞

-- 書き方①：モノイドの演算が働く対象の型を「引数」として宣言する（丸括弧のなか）
\record MonoidA (A : \Set0)
  | unitA : A
  | opA : A -> A -> A

-- 書き方②：モノイドの演算が働く対象の型も「フィールド」として宣言する
\record MonoidB
  | B : \Set0
  | unitB : B
  | opB : B -> B -> B

タロウくん：
・・・書き方が違うだけで、中身は同じに見えます。

専任講師：
名前の置き場所が違います。

	置き場所	書き方
引数	レコード名の直後、丸括弧のなか	`\record MonoidA (A : \Set0)`
フィールド	縦棒 `\|` を付けて、下に並べる	`\| B : \Set0`

タロウくん：
・・・A は引数で、B はフィールド。

専任講師：
Haskell でいえば、引数は型クラスの型引数にあたります。

＜Haskell で書けば＞

class MyMonoid a where
  unit :: a
  op   :: a -> a -> a

a が型引数です。そして Haskell には、これをフィールドとして記述する手段がありません。

使い方は、どう違うのか

専任講師：
まず、書き方①を使ってみます。

＜Arend のコード＞

\func mA : MonoidA Nat \cowith
  | unitA => 0
  | opA => \lam x y => x Nat.+ y

MonoidA Nat と、引数を渡しています。

タロウくん：
Haskell の MyMonoid Int と同じ形ですね。

専任講師：
次に、書き方②です。

＜Arend のコード＞

\func mB : MonoidB \cowith
  | B => Nat
  | unitB => 0
  | opB => \lam x y => x Nat.+ y

B を、他のフィールドと同じように埋めています。

タロウくん：
・・・渡し方が違う。

どちらの渡し方もできる

専任講師：
書き方②のレコードを、引数のように渡すことができます。

＜Arend のコード＞

\func mB2 : MonoidB Nat \cowith
  | unitB => 0
  | opB => \lam x y => x Nat.+ y

タロウくん：
・・・B をフィールドとして宣言したのに、MonoidB Nat と渡せている。

専任講師：
逆もできます。書き方①のレコードを、フィールドとして埋めることができます。

＜Arend のコード＞

\func mA2 : MonoidA \cowith
  | A => Nat
  | unitA => 0
  | opA => \lam x y => x Nat.+ y

＜Arend の型検査結果＞

$ java -jar Arend.jar PF.ard

--- Typechecking \default ---
[ ] src.PF
--- Done (130ms) ---

４つとも、型検査を通過します。

タロウくん：
・・・引数として宣言しても、フィールドとして宣言しても、どちらの渡し方もできる。

専任講師：
これが「引数とフィールドを区別しない」ということです。

タロウくん：
・・・冒頭で見た Monoid Nat 0 (足し算) も、この仕組みで記述されているのですね。

専任講師：
unit と op をフィールドとして宣言してあるからです。そして、引数のようにも渡すことができます。

だから、単位元と演算まで型のなかに入ります。

そのほかに、何の役に立つのか

タロウくん：
先生、ほかにも役立つ場面はありますか。

専任講師：
２つあります。

型を、必要な細かさで指定できる

専任講師：
関数を定義するとき、引数の型をどこまで細かく指定するかは、場面によって変わります。

＜Arend のコード＞

-- どんなモノイドでもよい
\func f1 (M : Monoid) : ...

-- Nat 上のモノイドに限る
\func f2 (M : Monoid Nat) : ...

-- Nat 上で、単位元が 0 のモノイドに限る
\func f3 (M : Monoid Nat 0) : ...

タロウくん：
・・・引数の個数を変えるだけで、細かさが変わる。

専任講師：
Haskell でこれをやろうとすると、型クラスを分けることになります。

タロウくん：
・・・Monoid と NatMonoid と ZeroUnitNatMonoid を作る、ということですか。

専任講師：
そして、それらの関係を別途つなぐ必要が出てきます。

設計をあとから変えられる

専任講師：
もうひとつが、実務では一番効きます。

ライブラリの設計を始めた時点では、何を型引数にすべきか分かりません。

タロウくん：
・・・使ってみて、はじめて分かる。

専任講師：
Haskell では、あとから型引数を増やすと、そのクラスを使っているコードがすべて壊れます。

タロウくん：
・・・利用者に影響が出る。

専任講師：
Arend では、フィールドとして宣言しておけば、使う側が必要に応じて引数として渡すことができます。

定義を書き直さずに済むのです。

タロウくん：
・・・最初の設計判断を、先送りにできる。

専任講師：
論文は、この効き目をこう述べています。

（原文引用）

This flexibility blurs the traditional distinction between parameters and fields in classes and records, enabling more versatile hierarchical structure development.

（筆者による日本語訳）

この柔軟性は、クラスとレコードにおける径数とフィールドの伝統的な区別をぼかし、より融通のきく階層構造の開発を可能にする。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・「より融通のきく階層構造の開発」。

専任講師：
モノイドから群、環、体へと階層を積み上げるとき、途中で設計を変えたくなる場面が出てきます。

そのときに、下の階層の定義を書き直さずに済む。そういうことです。

階層を、実際に組んでみる

専任講師：
では、第３部で見た階層を、実際に書いてみましょう。

１本道の部分

＜Arend のコード＞

\record Monoid (A : \Set0)
  | unit : A
  | op : A -> A -> A
  | assoc (x y z : A) : op (op x y) z = op x (op y z)

\record Group \extends Monoid
  | inv : A -> A
  | invLeft (x : A) : op (inv x) x = unit

\record AbGroup \extends Group
  | comm (x y : A) : op x y = op y x

＜Arend の型検査結果＞

$ java -jar Arend.jar V4L.ard

--- Typechecking \default ---
[ ] src.V4L
--- Done (127ms) ---

モノイドの上に群を積み、群の上に可換群を積んでいます。

\extends を並べるだけです。

分岐して合流する部分

専任講師：
次に、分岐と合流を書いてみます。

＜Arend のコード＞

-- 束：上限と下限を持つ
\record Lattice (E : \Set0)
  | join : E -> E -> E
  | meet : E -> E -> E

-- 分岐1：任意個の上限を持つ
\record CompleteLattice \extends Lattice
  | bigJoin : (Nat -> E) -> E

-- 分岐2：分配律を満たす
\record DistributiveLattice \extends Lattice
  | distr (x y z : E) : meet x (join y z) = join (meet x y) (meet x z)

-- 合流：両方を継承する
\record MyLocale \extends CompleteLattice, DistributiveLattice

＜Arend の型検査結果＞

$ java -jar Arend.jar V4K.ard

--- Typechecking \default ---
[ ] src.V4K
--- Done (129ms) ---

タロウくん：
・・・\extends CompleteLattice, DistributiveLattice と、カンマで並べるだけですね。

専任講師：
そこが多重継承です。

Lattice から２つに分岐し、MyLocale で合流しています。

そして Lattice の項目 join と meet は、両方の経路から受け継がれます。しかし重複しません。

タロウくん：
・・・同じものだと、処理系が判断している。

専任講師：
そこが「共有」です。

この形が、第３部で見た体の階層と同じものです。

        Lattice
       ／      ＼
CompleteLattice  DistributiveLattice
       ＼      ／
        MyLocale

タロウくん：
・・・図のとおりに書けている。

専任講師：
冒頭に掲げた問いへの答えが、ここにあります。

数学の階層は、分岐して合流します。Arend では、その形をそのままコードに写せます。

第６部 ── 数学概念の階層を組み上げるArendの柔軟さは、数学研究の実務でどう活用されて、実績を挙げているのか

ここまで、Arend のレコードにできることを見てきました。

しかし、それは理論上の話に留まるのでしょうか。それとも、実際に使われているのでしょうか。

この部では、次の３つを扱います。

#	問い
①	Arend のレコードには、どんなメリットがあるとされているのか
②	そのメリットは、実務で活用され、実績を挙げているのか
③	Lean 4 の Mathlib と比べて、どう位置づけられるのか

そして、Arend コミュニティで一般的に指摘されていることと、筆者の見解を、区別して示します。

Arend コミュニティが指摘するメリット

メリット１ ── 階層の分岐と合流を、そのまま記述できる

（原文引用）

Multiple inheritance together with manifest fields provide a flexible framework for grouping data associated to mathematical objects using sharing, extensions and subtyping.

（筆者による日本語訳）

多重継承と顕在フィールドは、共有・拡張・部分型付けを用いて、数学的対象に付随するデータをまとめるための柔軟な枠組みを提供する。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・読んでも、何ができるのかが分かりません。

専任講師：
噛み砕きます。数学の構造には、２種類の関係があります。

ひとつは「積み上がる」関係です。モノイドの上に群があり、群の上に環がある。

もうひとつは「合流する」関係です。体は、可換局所環でもあり、GCD 整域でもある。２つの流れが、体という一点で合流します。

タロウくん：
・・・木の枝分かれではなく、網の目のようになる。

専任講師：
引用文が言っているのは、その網の目を、そのままコードで表せるということです。

「共有」は、複数の構造が同じ項目を持つこと。「拡張」は、上に積み上げること。「部分型付け」は、群の値をモノイドとして渡せることです。

実際に使われているコード

Arend 公式論文に、体の定義がそのまま載っています。

＜Arend のコード＞

\class Field \extends LocalCRing, GCDDomain
  | #0 x => Inv x
  | #0-+ => LocalRing.sumInv=>eitherInv

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"（Arend 公式論文に掲載されているコードです）

（原文引用）

This example illustrates the usefulness of partial implementations for defining structures which extend several branches of hierarchies in such a way that some data and properties of one branch is implemented in terms of data and properties of other branches.

（筆者による日本語訳）

この例は、階層の複数の分岐を拡張するような構造を定義する際に、一方の分岐のデータや性質を、他方の分岐のデータや性質を用いて実装できるという、部分実装の有用性を示している。

出典：同上

タロウくん：
・・・やはり難しいです。

専任講師：
コードの２行目を見てください。

| #0 x => Inv x

#0 は、GCD 整域の側から来た項目です。 「その要素がゼロと離れているか」を表します。

Inv x は、可換局所環の側から来た概念です。 「その要素が逆元を持つか」を表します。

タロウくん：
・・・片方の項目を、もう片方の言葉で埋めている。

専任講師：
そこが引用文のいう「一方の分岐のデータを、他方の分岐のデータを用いて実装する」です。

体においては、ゼロと離れていることと、逆元を持つことが一致します。

だから、片方を定義したら、もう片方はそこから埋まる。その埋め込みを、型の定義のなかに記述できるのです。

タロウくん：
・・・第５部で見た顕在フィールドが、ここで効いている。

専任講師：
そのとおりです。

メリット２ ── 項目の型を、部分型に絞り込める

第５部で扱った \override です。

arend-lib の実コードにも、この機能が使われています。

＜Arend のコード＞

\record FrameHom \extends SetHom {
  \override Dom : Locale
  \override Cod : Locale

出典：同上（Arend 公式論文に掲載されているコードです）

タロウくん：
・・・集合の写像から、ロケールの写像を作っている。

専任講師：
土台となる写像のレコードは１つで済みます。

メリット３ ── 性質の証明は、比較のときに無視される

（原文引用）

Arend makes an explicit distinction between property fields and data fields. The result of comparison of two objects depends only on comparison of data fields, proofs of properties are ignored.

（筆者による日本語訳）

Arend は、性質の項目とデータの項目を明示的に区別する。２つの対象を比較した結果は、データの項目の比較のみに依存し、性質の証明は無視される。

出典：同上

タロウくん：
・・・なぜ、それが役に立つのですか。

専任講師：
第２部で見た Monoid を思い出してください。

\record Monoid (A : \Type)
  | unit : A
  | op : A -> A -> A
  | assoc (x y z : A) : op (op x y) z = op x (op y z)

上の２行がデータ、３行目が性質です。

タロウくん：
はい。

専任講師：
２つのモノイドが同じかどうかを判定するとき、３行目の証明は見ません。

単位元と演算が同じなら、同じモノイドとみなされます。結合律の証明の書き方が違っても、関係ありません。

タロウくん：
・・・証明の書き方の違いで、別物になってしまうと困る。

専任講師：
論文は、具体的な帰結を挙げています。

（原文引用）

One consequence of this would be that if C : Cat then C is computationally equal to (C^op)^op.

（筆者による日本語訳）

この帰結のひとつは、C が圏であるとき、C が $(C^{op})^{op}$ と計算的に等しくなることである。

出典：同上

専任講師：
$C^{op}$ とは、圏のすべての矢印の向きを逆にしたものです。

タロウくん：
・・・２回逆にすれば、元に戻る。

専任講師：
数学では、当たり前のことです。

しかし証明支援系では、そうならないことがあります。向きを２回逆にした結果が、元の圏と「等しいと証明はできるが、計算の上では別物」になってしまうのです。

タロウくん：
Arend では、そうならない。

専任講師：
性質の証明を無視するからです。 データの部分だけを見れば、$(C^{op})^{op}$ は $C$ そのものです。

実務での利用実績

理論上のメリットに留まっていません。

arend-lib に実際に形式化されているもの

Arend の標準ライブラリを arend-lib といいます。

（原文引用）

This part contains the following: schemes via locally ringed locales; PID domains and the proof that they are 1-dimensional Smith domains; splitting fields of polynomials and algebraic closure for countable, decidable fields; connection between zero-dimensional and integral extensions; matrices over commutative rings, determinants, characteristic polynomials, Cayley-Hamilton theorem; linear algebra over Smith domains; integral ring extensions; polynomials over one or several variables; Nakayama's lemma; derivative over topological rings; directed limits for sequences and functions; series and power series; natural, integer, rational, real and complex numbers and various structures on them; categories, functors, adjoint functors, Kan extensions, (co)limits; elementary topoi and Grothendieck topoi; topological spaces, locales, uniform spaces, completion of spaces.

（筆者による日本語訳）

この部分には次が含まれる。局所環付きロケールによるスキーム。PID 整域と、それが１次元 Smith 整域であることの証明。多項式の分解体と、可算かつ決定可能な体に対する代数閉包。零次元拡大と整拡大の関係。可換環上の行列、行列式、特性多項式、Cayley–Hamilton の定理。Smith 整域上の線形代数。整環拡大。一変数および多変数の多項式。中山の補題。位相環上の微分。数列と関数の有向極限。級数と冪級数。自然数、整数、有理数、実数、複素数と、それらの上の各種構造。圏、関手、随伴関手、Kan 拡張、（余）極限。初等トポスと Grothendieck トポス。位相空間、ロケール、一様空間、空間の完備化。

出典：同上

タロウくん：
・・・名前を聞いたことのないものばかりです。

専任講師：
どれも、大学の数学科で学部後半から大学院にかけて扱う内容です。

いくつか挙げます。

名前	どういうものか
Cayley–Hamilton の定理	行列は、自分自身の特性多項式に代入するとゼロになる
中山の補題	可換環論の基本的な道具。代数幾何でも頻繁に使う
スキーム	代数幾何の中心的な対象。方程式の解の集まりを、幾何学的に扱うための枠組み
Grothendieck トポス	圏論の枠組みで「空間」を一般化したもの

タロウくん：
・・・練習問題ではない。

専任講師：
そして、総合ホモトピー論の側でも形式化が進んでいます。

（原文引用）

The following has been formalized synthetically that is under types as homotopy types viewpoint: Eckmann-Hilton argument; K1(G); Hopf fibration; localization of universes and modalities; Generalized Blakers-Massey theorem.

（筆者による日本語訳）

次のものが、型をホモトピー型と見る観点のもとで、総合的に形式化されている。Eckmann–Hilton の議論。$K_1(G)$。Hopf ファイブレーション。宇宙の局所化とモダリティ。一般化 Blakers–Massey 定理。

出典：同上

専任講師：
Hopf ファイブレーションは、３次元球面を２次元球面へ写す、有名な構成です。

一般化 Blakers–Massey 定理は、2010年代に HoTT の枠組みで新しい証明が与えられた定理です。

タロウくん：
・・・HoTT の研究そのものにも使われている。

部分実装と多重継承が、実際に使われている箇所

論文には、arend-lib のコードが載っています。

ロケールの定義

（原文引用）

The class Locale forms a diamond in lattice hierarchy.

（筆者による日本語訳）

クラス Locale は、束の階層のなかでダイヤモンドを形成する。

出典：同上

タロウくん：
ダイヤモンド、ですか。

専任講師：
１つの構造から２つに分岐し、その先で再び合流する形です。

図にすると、菱形になります。だからダイヤモンドと呼ばれます。

        Bounded.Lattice
        ／           ＼
CompleteLattice   DistributiveLattice
        ＼           ／
           Locale

タロウくん：
・・・体が、可換局所環と GCD 整域から合流するのと同じ形。

専任講師：
まさに同じ形です。

そして Locale は、位相空間を点を使わずに扱うための概念で、arend-lib の代数幾何の部分で中心的な役割を果たしています。

タロウくん：
・・・第５部で書いた MyLocale は、これを真似たものですか。

専任講師：
そのとおりです。実際の Locale は、もっと多くの項目を持ちます。

アパートネス関係の定義

＜Arend のコード＞

\class AddGroupWith# \extends AddGroup, Set_#
  | \fix 8 #0 : E -> \Prop
  | #0-zro : Not (zro `#0)
  | #0-negative {x : E} : x `#0 -> negative x `#0
  | #0-+ {x y : E} : (x + y) `#0 -> x `#0 || y `#0
  | #0-tight {x : E} : Not (x `#0) -> x = zro
  | # x y => (x - y) `#0

出典：同上（Arend 公式論文に掲載されているコードです）

論文の説明を引きます。

（原文引用）

However, for example, in case of groups specifying the full binary relation x # y is redundant since it can be expressed in terms of x # 0. This can be done using partial implementations.

（筆者による日本語訳）

しかし、たとえば群の場合、二項関係 x # y の全体を指定するのは冗長である。x # 0 を用いて表現できるからである。これは部分実装を使ってできる。

出典：同上

専任講師：
アパートネス関係とは、「２つの値が離れている」ことを表す関係です。

構成的数学では「等しくない」という言い方が扱いにくいため、代わりにこれを使います。

タロウくん：
・・・群では、それを簡単にできる。

専任講師：
群では引き算ができます。だから「$x$ と $y$ が離れている」は「$x - y$ がゼロから離れている」と言い換えられます。

コードの最後の行が、その言い換えです。

| # x y => (x - y) `#0

２つの値についての関係を、１つの値についての性質から埋めています。

タロウくん：
・・・第５部で見た顕在フィールドが、実際のライブラリで使われている。

専任講師：
そういうことです。

Matita との比較

第４部で、顕在フィールドを持つ体系として Matita の名前を挙げました。ここで詳しく扱います。

（原文引用）

There are also implementations: manifest fields are supported, for example, by the proof assistant Matita.

（筆者による日本語訳）

実装もある。顕在フィールドは、たとえば定理証明支援系 Matita によってサポートされている。

出典：同上

Matita とは何か

項目	内容
開発元	イタリア・ボローニャ大学計算機科学科（Andrea Asperti 氏の研究チーム）
初版	1999年
最終リリース	0.99.1（2012年3月）
実装言語	OCaml
土台の型理論	CIC（Rocq／Coq と同じ系統）
名前の由来	イタリア語で「鉛筆」

タロウくん：
最終リリースが2012年ですか。

専任講師：
公式サイトは2023年時点でアーカイブされています。 現在も活発に開発されているとは言いにくい状況です。

ただし、GitHub 上には派生版が存在します。

Matita の位置づけ

（原文引用）

It has since then evolved into a fully fledged ITP, specifically designed as a light-weight, but competitive system, particularly suited for the assessment of innovative ideas, both at foundational and logical level.

（筆者による日本語訳）

その後、本格的な対話的定理証明支援系へと発展した。軽量でありながら競争力のある体系として設計されており、基礎的なレベルでも論理的なレベルでも、革新的なアイデアを評価するのにとくに適している。

出典：A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi, "The Matita Interactive Theorem Prover", CADE-23, LNCS 6803, 2011年, pp. 64–69

タロウくん：
・・・「革新的なアイデアを評価するのに適している」。

専任講師：
新しい仕組みを試す場、という位置づけです。

Rocq／Coq と同じ CIC を土台にしながら、実装は別に行われています。証明項のレベルでは、Rocq／Coq と部分的に互換性があります。

Matita の利用実績

分野	内容
コンパイラ検証	EU の CerCo プロジェクト。C 言語の一部から MCS-51 マイコンのアセンブリへの、計算量を保存するコンパイラを形式検証
プログラミング言語理論	POPLmark Challenge（束縛変数の扱いに関する形式化課題）part 1a に、３通りの解答
解析学	ルベーグの優収束定理の構成的な形式証明
計算理論	多テープチューリング機械の形式化
型理論	形式体系 $\lambda\delta$ の証明の認証

タロウくん：
・・・数学よりも、計算機科学寄りですね。

専任講師：
そこが Arend との大きな違いです。

Arend と Matita の比較

	Arend	Matita
開発元	JetBrains Research	ボローニャ大学
開発開始	2015年	1999年
開発状況	継続中	2012年以降、大きな更新なし
土台の型理論	HoTT-I（MLTT に区間型を加えたもの）	CIC
HoTT への対応	中核が HoTT 向けに設計されている	対応していない
顕在フィールド	持つ	持つ
包摂的部分型付け	持つ	持たない
主な適用分野	構成的数学、総合ホモトピー論	コンパイラ検証、プログラミング言語理論
開発環境	IntelliJ IDEA プラグイン	独自の画面（MathML による数式表示）

タロウくん：
・・・顕在フィールドは両方が持つが、包摂的部分型付けは Arend だけ。

専任講師：
そこが分かれ目です。

Arend 公式論文が「Coq、Lean、Agda には存在しない」と述べているのは、この２つを組み合わせて土台に置いている点です。

タロウくん：
すみわけは、どうなっていますか。

専任講師：
目指すものが違います。

Matita は、Rocq／Coq と同じ CIC を土台に、実装や利用者との対話の仕方で新しいことを試す体系でした。ライブラリを検索可能な知識ベースとして扱う設計や、数式の美しい表示に力が注がれています。

Arend は、HoTT を土台から支えることを目指した体系です。区間型、宇宙の階層、条件付き帰納型。どれも HoTT のために設計されています。

タロウくん：
・・・顕在フィールドを持つという共通点はあっても、目的が違う。

専任講師：
そのとおりです。

強みと弱み

以下は、筆者の見解を含みます。事実と区別して読んでください。

	Arend の強み	Arend の弱み
事実	HoTT が土台に組み込まれている	知名度が低く、利用者が少ない
事実	包摂的部分型付けと顕在フィールドの両方を持つ	正準性を備えていない
事実	IntelliJ IDEA という成熟した開発環境が使える	ライブラリの規模が Mathlib より小さい
筆者の見解	代数構造の階層を書くとき、記述量が減ると考えられる	他の処理系との定量的な比較は確認できなかった

	Matita の強み	Matita の弱み
事実	Rocq／Coq と証明項のレベルで部分的に互換	2012年以降、大きな更新がない
事実	コンパイラ検証で EU プロジェクトの実績がある	HoTT に対応していない
筆者の見解	実装が軽量で、新しい仕組みを試しやすい	現在の利用者数は確認できなかった

タロウくんの質問 ── Lean 4 の Mathlib から乗り換えるべきか

タロウくん：
先生、確かめさせてください。

arend-lib にはこれだけの定理が形式化されていて、Arend の型理論には実用にとって決定的に重要な計算規則が含まれている。

ということは、Lean 4 の Mathlib を使うよりも、定理証明エンジニアは Arend に乗り換えた上で、数学定理の証明検証の仕事をすべき、という結論に至るのですか？

でも、数学の AI による証明に相次いで採用されている Lean 4 に対して、Arend は圧倒的に知名度が小さいし、数学研究プロジェクトでの採用実績も乏しいですよね？

専任講師：
その通りです。乗り換えるべきだ、という結論にはなりません。

分けて答えます。

定理証明言語コミュニティにおける一般的な評価

事実として確認できることを述べます。

#	事実
①	Lean 4 の Mathlib は、現代数学の広い範囲を機械検証可能な形で収めている
②	arend-lib は、構成的数学と総合ホモトピー論に焦点を絞っている
③	Arend 公式論文は、Lean について「選択公理の強い形が組み込まれているため、一価性の基盤には適さない」と述べている

タロウくん：
・・・そもそも、目指しているものが違う。

専任講師：
Lean 4 は、古典論理を前提として現代数学を広く形式化する道を選んでいます。

Arend は、構成的数学と一価性を前提とする道を選んでいます。

同じ土俵で優劣を比べるものではありません。

Arend と Lean 4 は、具体的にどう方向が違うのか

タロウくん：
先生、さきほど「目指す方向が違う」とおっしゃいました。

具体的には、どう違うのですか。

専任講師：
３つの点で違います。順に見ていきましょう。

違い① ── 排中律を、最初から入れるかどうか

専任講師：
排中律とは、「どんな主張についても、それが正しいか正しくないかのどちらかである」という原則です。

タロウくん：
・・・当たり前ではないのですか。

専任講師：
数学では、当たり前とされてきました。

しかし、そこには落とし穴があります。「正しくないと仮定すると矛盾する。だから正しい」という論法が使えるのです。

タロウくん：
背理法ですね。

専任講師：
そうです。そして背理法で「存在する」と示しても、実物は手に入りません。

「存在しないと仮定すると矛盾する。ゆえに存在する」。それだけでは、どこにあるのかが分からないのです。

タロウくん：
・・・プログラムとしては、動かない。

専任講師：
Lean 4 は、排中律を最初から組み込んでいます。

Arend は、組み込んでいません。

（原文引用）

Whereas Coq and Lean (based on CIC) do not particularly favor constructivism (Lean even has the axioms of choice and excluded middle built-in), Agda (based on MLTT) leans more towards constructive mathematics.

（筆者による日本語訳）

Rocq／Coq と Lean は CIC に基づいており、構成主義をとくに重んじるわけではない。Lean にいたっては、選択公理と排中律が組み込まれている。一方 Agda は MLTT に基づいており、構成的数学の側に寄っている。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・Lean は、数学者が普段使う論理をそのまま使える。

専任講師：
そこが Lean 4 の強みです。

現代数学の証明の多くは、排中律を使っています。それをそのまま形式化できるのです。

Arend では、排中律を使う証明は、そのままでは通りません。

違い② ── 一価性を扱えるかどうか

タロウくん：
では、Lean 4 で HoTT を扱うことはできますか。

専任講師：
扱えません。

（原文引用）

An important caveat is that the ITP should not incorporate built-in features that contradict the univalence axiom. For instance, Lean is unsuitable for UF as it incorporates a strong form of the axiom of choice built-in.

（筆者による日本語訳）

重要な但し書きがある。定理証明支援系は、一価性公理と矛盾する機能を組み込みで持つべきではない。たとえば Lean は、選択公理の強い形を組み込みで持つため、一価性の基盤には適さない。

出典：同上

タロウくん：
・・・組み込みの機能と、一価性が衝突する。

専任講師：
そういうことです。

Lean 4 には、選択公理の強い形が最初から入っています。それと一価性を同時に成り立たせようとすると、体系が壊れます。

タロウくん：
片方を諦めるしかない。

専任講師：
Lean 4 は、選択公理を取りました。

Arend は、一価性を取りました。

そして、これは優劣ではありません。何を扱いたいかの違いです。

違い③ ── ライブラリが何を集めているか

専任講師：
目指すものが違えば、集まるものも違います。

	Lean 4（Mathlib）	Arend（arend-lib）
前提とする論理	古典論理（排中律あり）	構成的論理（排中律なし）
集めているもの	現代数学の広い範囲	構成的数学と総合ホモトピー論
規模	大きい	小さい
一価性	扱えない	扱える

タロウくん：
・・・Mathlib のほうが広い。

専任講師：
その代わり、構成的な議論には向きません。

そして、構成的な世界には、古典的な世界にはない事情があります。

（原文引用）

The mathematical landscape in the constructive setting is richer than in the classical setting since classically equivalent definitions often become inequivalent constructively.

（筆者による日本語訳）

構成的な設定における数学的風景は、古典的な設定よりも豊かである。古典的に同値な定義が、構成的にはしばしば同値でなくなるからである。

出典：同上

タロウくん：
・・・「豊か」というのが、よく分かりません。

専任講師：
言い換えます。「同じもの」だったはずのものが、２つに分かれるのです。

タロウくん：
分かれる、ですか。

専任講師：
具体例で見ましょう。

古典的な数学では、次の２つは同じことを意味します。

#	言い方
A	「そういうものが存在する」
B	「そういうものが存在しないと仮定すると、矛盾が出る」

タロウくん：
・・・背理法ですね。B から A が言える。

専任講師：
排中律があれば、そのとおりです。

しかし排中律がないと、B から A へ渡れません。

タロウくん：
・・・矛盾は示せたが、実物は手に入っていない。

専任講師：
そこが分かれ目です。

古典的には１つだった「存在する」が、構成的には２つに分かれます。 実物を作れる場合と、矛盾だけを示せた場合です。

タロウくん：
それが「豊か」ということですか。

専任講師：
区別が増える、という意味での豊かさです。

そして、区別が増えると、扱いの難しさも増えます。

具体例 ── 代数幾何で何が起きるか

専任講師：
arend-lib には、代数幾何の形式化が含まれています。

そこで、いま述べた問題が実際に起きました。

タロウくん：
代数幾何、といいますと。

専任講師：
方程式の解の集まりを、図形として扱う分野です。

$x^2 + y^2 = 1$ という方程式の解は、平面上の円になります。方程式を扱うことが、図形を扱うことになります。

タロウくん：
・・・数式と図形を、行き来する。

専任講師：
その行き来を、一般的な形で扱うために「スキーム」という概念が使われます。

そして、スキームを作るには、まず「点」を決める必要があります。

タロウくん：
図形なのだから、点がある。

専任講師：
古典的な代数幾何では、点として素イデアルというものを使います。

タロウくん：
素イデアル。

専任講師：
整数で説明します。

$2$ の倍数全体を考えてください。$\ldots, -4, -2, 0, 2, 4, \ldots$ という集まりです。

この集まりには、次の性質があります。２つの数を掛けた結果がこの中にあるなら、少なくとも片方はこの中にある。

タロウくん：
・・・$a \times b$ が偶数なら、$a$ か $b$ のどちらかは偶数。

専任講師：
そのとおりです。この性質を持つ集まりを、素イデアルと呼びます。

$2$ の倍数全体、$3$ の倍数全体、$5$ の倍数全体。素数ごとに、ひとつずつあります。

タロウくん：
・・・素数と対応している。だから「素」イデアル。

専任講師：
一般の環でも、同じ考え方で素イデアルを定めます。そして、それを点とみなすのです。

構成的な世界では、点が手に入らない

タロウくん：
それで、何が問題になるのですか。

専任講師：
「素イデアルが存在する」ことを、構成的には示せない場合があるのです。

（原文引用）

Classically, an affine scheme is defined as the topological space Spec R, whose points are the prime ideals of a ring R, equipped with a canonical sheaf of rings. However, in a constructive setting, prime ideals may not exist.

（筆者による日本語訳）

古典的には、アフィンスキームは位相空間 Spec R として定義される。その点は環 R の素イデアルであり、環の標準的な層を備えている。しかし構成的な設定では、素イデアルは存在しないかもしれない。

出典：同上

タロウくん：
なぜ、示せないのですか。

専任講師：
古典的な証明が、選択公理という原則を使うからです。

タロウくん：
選択公理。

専任講師：
箱がたくさん並んでいると思ってください。どの箱にも、中身が入っています。

「それぞれの箱から、ひとつずつ取り出したものを集められる」。これが選択公理です。

タロウくん：
・・・当たり前ではないですか。

専任講師：
箱が有限個なら、当たり前です。ひとつずつ、順に取り出せばよいのです。

問題は、箱が無限にある場合です。

タロウくん：
・・・順に取り出していたら、終わらない。

専任講師：
そして「どう選ぶか」を決める規則がなければ、選び方を記述できません。

選択公理は、**「規則を示せなくても、選べたことにしてよい」**と認めるものです。

タロウくん：
・・・構成的な立場からは、認めがたい。

専任講師：
実物を作らずに「ある」と言っているからです。

そして、素イデアルの存在証明は、この選択公理を使います。正確には、選択公理から導かれる Zorn の補題という道具を使います。

タロウくん：
Zorn の補題。

専任講師：
「一番大きなものが存在する」ことを示すための道具です。

素イデアルを見つける古典的な方法は、こうです。条件を満たす集まりを次々に大きくしていき、これ以上大きくできないところまで来たら、それが素イデアルである。

タロウくん：
・・・その「これ以上大きくできないところ」があると言うために、Zorn の補題を使う。

専任講師：
そのとおりです。そして、それは選択公理から出てきます。

構成的な立場では選択公理を使わないので、この方法が使えません。

では、どうするのか

タロウくん：
点が手に入らないなら、図形を扱えないのでは。

専任講師：
点を使わない方法があります。

（原文引用）

In contrast, the locale of "open subsets" corresponding to radical ideals of R always preserves the meaningful structure.

（筆者による日本語訳）

対照的に、R の根基イデアルに対応する「開部分集合」のロケールは、常に意味のある構造を保つ。

出典：同上

タロウくん：
・・・ロケール。

専任講師：
「開集合」の側から空間を捉える枠組みです。

タロウくん：
開集合、といいますと。

専任講師：
平面の上で、円の内側を考えてください。ただし、縁は含めません。

そういう「縁を含まない領域」が開集合です。

タロウくん：
はい。

専任講師：
通常、空間はまず点の集まりとして定め、そのあとで開集合を決めます。

ロケールでは、順序を逆にします。開集合どうしの関係だけを先に決め、点については何も言わないのです。

タロウくん：
・・・点がなくても、空間として扱える。

専任講師：
開集合どうしの重なりや包含の関係。それだけあれば、多くの議論が成り立ちます。

そして、開集合のほうは構成的にも作れます。

タロウくん：
だから、点が手に入らなくても困らない。

専任講師：
arend-lib が代数幾何をロケールで組んでいるのは、この理由によります。

タロウくん：
・・・第５部で見た Locale は、そのためのものだったのですね。

専任講師：
そういうことです。

タロウくん：
・・・構成的にやろうとすると、枠組みごと変える必要がある。

専任講師：
そこが「構成的な風景は豊かである」の中身です。

古典的には、点で考えても開集合で考えても同じでした。構成的には、その２つが分かれるのです。

コミュニティでの知名度について

タロウくん：
先生、Arend の知名度についても伺いたいのですが。

専任講師：
観察できる事実を並べます。

知られている証拠

#	事実
①	2019年8月の公開時、HoTT メーリングリストで Andrej Bauer、Nicolai Kraus、Jon Sterling、Michael Shulman が反応している
②	Andrej Bauer の連続講演企画「Every proof assistant」で、2020年4月に Arend が取り上げられた
③	nLab の「formalized libraries of homotopy type theory」に記載がある
④	Hacker News でも取り上げられた（2019年8月）

一方で

#	事実
①	Rocq／Coq、Agda、Lean と比べると、言及数は明らかに少ない
②	日本語の解説記事は見当たらない

タロウくん：
・・・専門家には知られているが、広くは知られていない。

専任講師：
「HoTT の研究者には知られているが、一般のプログラマにはほとんど知られていない」という程度でしょう。

【本記事執筆者の見解】

以下は、筆者が調べた範囲での判断です。出典のある事実ではありません。

第１に、いま数学の形式化を仕事にするなら、Lean 4 と Mathlib を選ぶのが現実的です。

利用者数、ライブラリの規模、AI との連携の実績。どれも Lean 4 が先行しています。

第２に、Arend が向く場面は限られています。

構成的数学を扱いたい。一価性を計算規則つきで使いたい。そうした目的があるときに、選択肢に入ります。

第３に、記述量の比較は、筆者には確認できませんでした。

「Arend のほうが階層を短く記述できる」という主張を裏づける定量的な比較実験は、筆者が調べた範囲では見つかりませんでした。論文が挙げているのは、設計上の説明と実際のコード例です。

第４に、本記事で引いた資料は、いずれも Arend 側のものです。

他の処理系の開発チームによる反論や、第三者による比較評価は確認していません。

その前提で読んでいただく必要があります。

事実と見解の整理

#	内容	区分
①	arend-lib に大学院レベルの定理が形式化されている	事実（公式論文）
②	部分実装と多重継承が、arend-lib の実コードで使われている	事実（公式論文に掲載されたコード）
③	Lean 4 の Mathlib のほうが規模が大きく、利用者も多い	事実
④	Arend と Lean 4 は、目指す方向が違う	事実（両者の公式資料）
⑤	数学の形式化を仕事にするなら、現時点では Lean 4 が現実的	筆者の見解
⑥	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"

同じ論文は、こうも述べています。

（原文引用）

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.

（筆者による日本語訳）

そのような完全に計算可能な理論の発展は理論的な関心の対象であるが、二層の枠組みの複雑さは、現状では実用上その採用を正当化しない。

出典：同上

タロウくん：
・・・理論としての関心は認めている。

専任講師：
しかし、実用上は割に合わないという判断です。

レコードについて ── 実践で必要とされた

同じ論文が、レコードの設計についてはこう述べています。

（原文引用）

Formalization of mathematics crucially relies on mechanisms for grouping data and properties of mathematical structures.

（筆者による日本語訳）

数学の形式化は、数学的構造のデータと性質をまとめる仕組みに決定的に依存している。

出典：同上

タロウくん：
・・・「決定的に依存している」。

専任講師：
先ほどの「必要性を大きくは示していない」と、対になる言葉です。

そして論文は、包摂的部分型付けと顕在フィールドを、次のように位置づけています。

（原文引用）

Finally, the type theory of Arend includes the following extensions, which are of significant practical importance for formalization and yet are not present in Coq, Lean, or Agda.

（筆者による日本語訳）

最後に、Arend の型理論は次の拡張を含む。これらは形式化にとって実践上きわめて重要でありながら、Coq、Lean、Agda には存在しない。

出典：同上

タロウくん：
・・・「実践上きわめて重要」。

専任講師：
同じ論文のなかで、片方は「必要とされていない」、もう片方は「きわめて重要」と述べられています。

並べてみると

	第２回目の記事で扱った論点	本記事で扱った論点
何を選んだか	単純な理論	豊かな土台
何を手放したか	計算しきる力	土台の小ささ
論文の言葉	実践的な経験は、そのような強化の必要性を大きくは示していない	形式化は、まとめる仕組みに決定的に依存している
判断の基準	形式化の実践	形式化の実践

タロウくん：
・・・言葉が、どちらも「形式化の実践」を指している。

専任講師：
計算可能性は、実際に形式化をしてみると必要とされなかった。レコードの階層は、実際に形式化をしてみると必要だった。

タロウくん：
だから、片方は足さず、片方は足した。

専任講師：
一貫していると読めます。

タロウくん：
理論の美しさで決めたのではない。

専任講師：
そう読める、という言い方に留めておきます。

開発チームが「この基準で決めた」と明言した資料は、筆者が調べた範囲では見つかりませんでした。

論文から読み取れるのは、どちらの判断についても「形式化の実践」という言葉が根拠として置かれている、という事実だけです。

本記事を振り返って

タロウくん：
・・・整理させてください。

Haskell の Monoid には法則があるが、コンパイラは検査しない。そこから始まりました。

専任講師：
依存型があれば、法則を型に記述できます。

タロウくん：
ただし、それは Arend 固有ではなかった。Lean 4 でもできる。

専任講師：
本当の問題は、階層でした。

タロウくん：
モノイド、群、環、体。積み上がるだけでなく、分岐して合流する。

専任講師：
その形を、そのままコードに写せるか。

タロウくん：
Lean・Rocq／Coq・Agda は、土台を単純に保った。包摂的部分型付けと顕在フィールドを、外側の仕組みで補ってきた。

専任講師：
Arend は、その２つを土台に組み込みました。

タロウくん：
そして、それは実際に使われている。arend-lib の代数幾何や圏論の部分で。

専任講師：
第２回目の記事と逆に見える判断も、同じ基準から出ていました。

タロウくん：
・・・形式化の実践で必要かどうか。

専任講師：
そこが、Arend の物差しです。

次回の予告

【Arend Theorem Prover 連載（５回目）】では、高次帰納型を扱います。

Haskell の data で定義できるのは、値の作り方だけでした。

Arend では、そこに「これとこれは同じ」という指定も並べられます。

第３回目の記事で見た商型が、その仕組みで作られていました。

そして、この仕組みで作ることができるものは、商型だけではありません。

「点をひとつ置き、その点から自分自身への道をひとつ置く」。
それだけで、円周を表す型になります。

＜Arend のコード＞

\data S1
  | base
  | loop : base = base

図形を、データ型として書く。

それが、高次帰納型 です。

本記事の第４部で触れた 「どのホモトピーレベルにも収まらない型」が、ここで実際に現れます 。

連載リンク

【発展篇】中上級者向けのコラム

この記事は分かりやすい入門者向けの記事を心がけましたので、厳密な議論を犠牲にした部分があります。

以下、中上級者向けに補足説明すべき箇所を、本文の部ごとに分けて述べます。

第１部・第２部について

📌 中上級者向け：Haskell にも型レベルの等しさはあります

本文では、Haskell の Monoid 型クラスに、任意の値についての法則を証明として書き込み、処理系に検査させる手段はない、と説明しました。これは標準の Monoid クラスについて述べたものです。

より進んだ Haskell には、GADTs、DataKinds、型族、Data.Type.Equality など、型レベルの等しさを扱うための仕組みがあります。

data a :~: b where
  Refl :: a :~: a

そのため「Haskell では等しさをまったく扱えない」という意味ではありません。

ただし、標準の Monoid クラスは、左右単位律や結合律の証明をフィールドとして要求しません。本記事で対比しているのは、まさにこの点です。

Arend や Lean などでは、構造の定義そのものに法則の証明を置けます。Haskell の標準 Monoid では、法則はライブラリ利用者と実装者のあいだの契約として文書化されています。

📌 中上級者向け：「依存型を持つ言語ならできる」の意味

本文で「依存型を持つ言語なら、法則を型として記述できる」と述べたのは、本記事で比較している Arend、Lean 4、Rocq／Coq、Agda のような定理証明支援系についての説明です。

より厳密には、依存型を持つ言語にもさまざまな設計があります。

等しさをどのような型で表すか。命題とデータをどう区別するか。証明をどこまで計算に使うか。宇宙をどう管理するか。これらは、処理系ごとに異なります。

ここでいう「同じことができる」とは、構造のフィールドとして「この法則が成り立つ」という証明を要求し、証明なしにはその構造の値を作れないようにできる、という意味です。

証明をどこまで自動化できるか、実用ライブラリをどう設計するかは、処理系ごとに別の問題です。

第３部について

📌 中上級者向け：HoTT は集合論を否定する理論ではありません

本文では、集合論では同型と等号が区別されること、HoTT／UF では一価性によって構造同一性原理が得られることを紹介しました。これは、HoTT／UF が得意とする視点を示すためです。

ただし、集合論は現代数学の基礎として現在も広く使われています。

集合論のもとでも、数学者は同型な構造を適切に同一視しながら豊かな数学を展開してきました。

HoTT／UF は「集合論が誤りだから捨てる」という主張ではありません。

むしろ、同一性・同型・同値の関係を、型理論の内部でどのように表すかについて、別の基礎づけを与える試みです。

本文の「同型なら等しい」という言い方も、どんな対象でも無条件に同一視するという意味ではなく、構造に対応した適切な同型・同値を用いるという意味で理解してください。

📌 中上級者向け：型理論による数学基礎づけの歴史

本文では、2000年代半ばから一価的基礎づけ（UF）という流れが大きく進展したことを紹介しました。

ただし、型理論による数学の基礎づけ、構成主義数学、定理証明支援系の歴史は、それ以前から続いています。

年代	出来事
1970年代	Martin-Löf 型理論の提唱
1980年代	Nuprl の開発
1984年	Rocq／Coq の前身の開発開始
1990年代	Agda の前身の開発開始

2000年代半ばという時点は、型理論そのものの始まりではありません。

一価性の発見・提唱をきっかけに、同型と等号の関係を新しい形で扱う基礎づけが大きく注目され、のちの HoTT／UF へつながった時期を指しています。

📌 中上級者向け：分数の商と構造同一性原理は、同じ話ではありません

本文では、$1/2$ と $2/4$ を例に、「表現は違っても同じものとして扱いたい」という直観を作りました。

通常の集合論では、有理数は分子と分母の組に同値関係を入れ、その商を取ることで構成されます。

この構成を終えた後では、$(1, 2)$ と $(2, 4)$ は有理数として同じ要素です。

一方、構造同一性原理は、群・環・位相空間のような構造について、適切な同型と等号を結び付ける原理です。

両者は「表現の違いをどう扱うか」という直観では似ていますが、技術的には別の問題です。

本文では、この共通する直観だけを入口として使っています。

📌 中上級者向け：体が可換局所環かつ GCD 整域である理由

本文で必要なのは、体が複数の枝から性質を受け継ぐ例である、という点です。ここではその背景を少しだけ補います。

可換局所環とは、標準的には極大イデアルをただ１つ持つ可換環です。

体では、$0$ 以外のすべての元が逆元を持つため、可逆でない元は $0$ だけです。そのため、体は可換局所環になります。

また体は零因子を持たないので整域です。

さらに、$0$ でない元どうしについては、一方が他方を割り切るため、最大公約数を考える条件も満たします。この意味で、体は GCD 整域でもあります。

ただし「最大公約数」は単元倍を除いて定まる、$0 \neq 1$ を仮定する、といった慣習的な細部があります。

本記事の中心は環論の定義ではなく、こうした複数の枝がコード上で合流するときに、Arend の部分実装が役立つ点です。

📌 中上級者向け：多重継承のダイヤモンド問題について

本文では、Lattice から分岐して MyLocale で合流する例を示しました。

この形は、オブジェクト指向言語ではダイヤモンド問題として知られています。

D が B と C を継承し、B と C がともに A を継承する。このとき、D のなかに A の情報が２つ入ってしまうのではないか、という問題です。

C++ では仮想継承という仕組みで対処します。Java では多重継承そのものを禁じています。

依存型理論では、事情が異なります。

Arend では、レコードの項目は名前で識別されます。B から来た A の項目と、C から来た A の項目は、同じ名前を持ちます。そのため、同一の項目として扱われます。

これが、本文で「共有」と呼んだ仕組みです。

ただし、項目の型が経路によって異なる場合には、注意が必要です。 \override によって型が絞り込まれていると、２つの経路で異なる型が要求されることがあります。その場合、型検査器はより狭いほうの型を採ります。

第４部について

📌 中上級者向け：包摂的部分型付けと強制的部分型付けの違いを、厳密にいうと

本文では、両者の違いを「変換関数が挿入されるかどうか」として説明しました。

より正確には、次のように定式化されます。

包摂的部分型付けでは、$A < B$ という関係があるとき、$a : A$ という型付けから $a : B$ という型付けが直ちに導かれます。項 $a$ そのものは変わりません。

強制的部分型付けでは、$A <_c B$ という関係は、関数 $c : A \to B$ を伴います。型 $B$ の項が期待される文脈で $a : A$ が使われると、型検査器が $c,a : B$ という適用を挿入します。項が書き換わるのです。

この違いは、項の等しさを扱うときに表面化します。強制的部分型付けでは、挿入された変換関数が項のなかに残るため、２つの項が等しいかどうかの判定に影響します。

なお、強制的部分型付けの理論的な定式化は、Zhaohui Luo らによって整備されました。その研究のなかで、包摂的部分型付けが正準的対象を持つ型理論には適さないという議論も示されています。

本記事では、この議論と各処理系の設計判断とのつながりについて、一次資料で確認できた範囲を超える主張はしていません。

出典：Z. Luo, S. Soloviev, T. Xue, "Coercive subtyping: Theory and implementation", Information and Computation, vol. 223, 2013年, pp. 18–42

📌 中上級者向け：「レコード型はシグマ型と同じ」とは、何を意味するのか

本文では、シグマ型を「組の型」、レコードを「名前付きのフィールドを持つ型」として紹介しました。

Arend 公式論文の「レコード型はシグマ型と同じもの」という表現は、レコードを単なる依存ペアの組合せとして扱う設計を指しています。

これは、レコードの構文が存在しないという意味ではありません。 また、実装上の使いやすさまで完全に同一という意味でもありません。

この論文の問題意識は、通常の依存レコードに加えて、顕在フィールドや包摂的部分型付けを言語の土台の規則として持たせるかどうかです。

Arend は、数学の構造を階層的に組み立てる実務では、その追加の表現力が役立つと考えています。

📌 中上級者向け：半環の公理は、体系によって異なります

本文では、半環の定義に $0 \times x = 0$ が公理として含まれると述べました。

これは、Arend 公式論文が挙げている Semiring の定義に基づく記述です。

しかし、半環の定義は文献によって異なります。

多くの教科書では、半環を「加法について可換モノイド、乗法についてモノイド、両者が分配律で結ばれ、加法の単位元が乗法について吸収的である」と定めます。この「吸収的」という条件が、$0 \times x = 0$ にあたります。

一方、乗法の単位元を要求しない定義や、加法の可換性を要求しない定義もあります。

本文の記述は、Arend 公式論文の Semiring に沿ったものであり、半環の唯一の定義を述べたものではありません。

📌 中上級者向け：可述的（predicative）と宇宙階層について

本文では、可述的（predicative）を「自分自身を含む集まりについて語ることを禁じる立場」と説明しました。

これは、入門者に宇宙階層の必要性を理解してもらうための直感的な説明です。

しかし、predicativity は、この一文だけで定義できる概念ではありません。

より一般には、ある対象を定義・形成するとき、その対象自身を含む全体についての量化や参照をどこまで許すかという、型や集合の形成規則・量化規則に関する性質として理解する必要があります。

したがって、「自分自身を含む集まりは禁止される＝ predicative」と完全に同一視するのは正確ではありません。

また、型理論における宇宙階層は、単純にラッセルのパラドックスだけを避けるための仕組みとして説明し尽くせるものでもありません。

本記事では、すべての型をひとつの宇宙に集め、その宇宙自身も同じ宇宙に入れる、という構成を避けるために階層を作る、という直感を採用しました。

入門者向けには、この理解で十分です。ただし型理論の基礎論としては、宇宙の形成規則と predicativity を分けて考える必要があります。

📌 中上級者向け：宇宙は「型を集めた場所」ではありません

本文では、\Set0 の中身は型そのものです、と説明しました。

これは便利な直感ですが、厳密には「宇宙＝その宇宙に属する型を全部集めた集合」と考えるべきではありません。

型理論における宇宙は、型を分類するための型そのものです。

たとえば、

$$A : \mathrm{Type}_0$$

と書いたとき、これは「$A$ は $\mathrm{Type}_0$ に属する型である」という型付けを表します。

集合論で「すべての型を要素として持つ集合が存在する」と主張しているのとは、意味が異なります。

また、

$$\mathrm{Type}_0 : \mathrm{Type}_1$$

という階層を持たせることで、$\mathrm{Type}_0$ 自身を $\mathrm{Type}_0$ に入れず、ひとつ上の宇宙に置くことができます。

この構造は、型理論の一貫性や型形成規則と密接に関係しています。

したがって本文の「型を集めた場所」という説明は、あくまで直感的なものです。より正確には「型を分類するための型」と理解するほうが、型理論的には適切です。

📌 中上級者向け：グロタンディーク宇宙と、型理論の宇宙の違い

本文では、型理論の宇宙と集合論のグロタンディーク宇宙を、どちらも階層を作って「大きすぎる集まり」を扱わないようにする、という共通点から比較しました。

この比較は、直感を得るうえでは有用です。しかし、両者は同じ数学的対象ではありません。

グロタンディーク宇宙は、集合論の中で定義される特別な集合です。 閉性条件を満たす「十分に大きな集合」を提供します。

一方、型理論の宇宙は、型理論そのものの構文・型付け規則の一部です。

また、グロタンディーク宇宙の存在を集合論に追加することは、一般には非常に強い集合論的仮定になります。典型的には到達不能基数との対応が知られています。

これに対して、型理論の宇宙階層は、型理論の基礎体系の一部として導入されます。

したがって、「グロタンディーク宇宙を型理論の宇宙に翻訳すれば完全に同じ」という意味ではありません。

本記事では、「大きすぎる全体をひとつにまとめず、階層化する」という設計思想の類似性に限定して比較しています。

第５部について

📌 中上級者向け：顕在フィールドと既定値の違いを、厳密にいうと

本文では、両者の違いを「あとから上書きできるかどうか」として説明しました。

より正確には、次の点が本質的です。

顕在フィールド $x \Rightarrow a$ を持つレコード型 $D$ の要素は、その項目の値が $a$ と計算的に等しい組になります。

すなわち、$D$ という型そのものが、「$x$ が $a$ である」という情報を含んでいます。型検査器は、$D$ の要素を扱うとき、$x$ の値を $a$ として直接使えます。

既定値は、これとは異なります。値を作るときに省略できるという、記述上の便宜にすぎません。 型のレベルでは何も保証されず、別の値で上書きされる可能性が残ります。

また、顕在フィールドは部分実装の基礎でもあります。 レコード $C$ の項目の一部を顕在フィールドで埋めた拡張 $D$ を作ると、$D$ は $C$ の部分型になり、かつ残りの項目は未実装のまま残ります。

そして、匿名拡張はこの仕組みの上に作られています。 本文で扱った Monoid Nat という記法は、内部的には顕在フィールドによる匿名の拡張です。

📌 中上級者向け：`\record` と `\class` の違い

本文では、主に \record を使いました。しかし Arend 公式論文が引用しているコードには \class が現れます。

両者の違いは、インスタンス推論の対象になるかどうかです。

\class で定義したものは、\instance として登録できます。登録されたインスタンスは、型検査器が文脈から自動的に探し出します。 Haskell の型クラスと同じ発想です。

\record にはこの仕組みがありません。値を明示的に渡す必要があります。

もうひとつの違いは、分類フィールド（classifying field）です。

\class の最初の明示的な項目は、既定で分類フィールドになります。インスタンス推論は、この項目の値を手がかりに行われます。

本記事では、レコードの構造そのものに焦点を当てるため、インスタンス推論の仕組みには立ち入っていません。

📌 中上級者向け：Mathlib の `extends` は、Arend の `\extends` と同じではありません

本文では、Mathlib が extends による継承を使っていると述べました。

しかし、両者の仕組みは異なります。

Lean 4 の extends は、親クラスの構造体を、子クラスの項目として埋め込みます。 子の値から親の値を取り出すには、その項目にアクセスします。そして、型検査器が自動的にその取り出しを挿入します。

これが、本文で述べた強制的部分型付けにあたります。

Arend の \extends では、子の型が親の型の部分型になります。取り出しの操作は入りません。

この違いは、ダイヤモンド継承のときに表面化します。

Lean 4 では、同じ祖先を２経路で継承すると、祖先の情報が２つ埋め込まれる可能性があります。それらが一致することを、別途保証する必要が生じます。 Mathlib では、この問題への対処として old_structure_cmd の廃止や flat structure の設計変更が議論されてきました。

Arend では、部分型付けが土台にあるため、この種の重複が生じにくい設計になっています。

ただし、両者を定量的に比較した資料は、筆者が調べた範囲では見つかりませんでした。

📌 中上級者向け：「引数とフィールドを区別しない」の厳密な意味

本文では、「Arend では、引数とフィールドを区別しません」と説明しました。

これは Arend の柔軟性を理解するための簡略化です。

より正確には、Arend では顕在フィールドがパラメータのように振る舞えるため、従来の型理論で明確に区別されることの多かった「パラメータ」と「フィールド」の境界が曖昧になります。

たとえば、

Monoid
Monoid Nat
Monoid Nat 1
Monoid Nat 1 (掛け算)

と書くと、後ろに値を適用していくことで、対象を段階的に特殊化できます。

Arend 公式論文も、次のように説明しています。

（原文引用）

records' fields also behave like parameters

（筆者による日本語訳）

レコードのフィールドは、径数のようにも振る舞う。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

したがって厳密には、「引数とフィールドが完全に同一の概念になる」という意味ではありません。

「顕在フィールドによって、フィールドをパラメータのように扱えるため、従来の区別が曖昧になる」ということです。

第６部・第７部について

📌 中上級者向け：Lean・Rocq／Coq・Agda は、実用上も同じではありません

本文では、Arend 公式論文が示す比較軸に沿って、包摂的部分型付けと顕在フィールドを言語の土台に置くかどうかを説明しました。

しかし、Lean、Rocq／Coq、Agda は実用上も同じではありません。

処理系	代数構造の階層を扱うための仕組み
Lean 4	構造体、継承、coercion、typeclass inference、Mathlib の設計規約
Rocq／Coq	coercions、type classes、canonical structures、Mathematical Components の mixin 階層
Agda	record、instance arguments、module system

したがって、「他の処理系では代数構造の階層を表現できない」という意味ではありません。

本記事の比較は、同じ目的を達成するために、Arend が一部の機能をレコードの中核仕様として直接支え、他の処理系では補助機構やライブラリ設計で扱うことが多い、という設計上の違いに焦点を当てています。

📌 中上級者向け：「Lean 4 では HoTT を扱えない」の厳密な意味

本文では、入門者向けに Lean 4 と HoTT の関係を簡潔に「扱えません」と表現しました。

ここは、より厳密には区別が必要です。

Lean 4 上で HoTT に関係する概念や定理を形式化すること自体が不可能、という意味ではありません。

問題になるのは、Lean 4 自体を、一価性を備えた HoTT／一価的基礎づけの基礎体系としてそのまま利用できるかという点です。

Lean 4 の基礎体系には、古典数学で利用される公理・原理を導入できる仕組みがあります。

そして Arend 公式論文は、強い形の選択公理を組み込みで持つ Lean は、一価性の基盤として適さないと説明しています。

したがって、より正確には次のようになります。


Lean 4 上で HoTT 的な数学を形式化すること	可能な範囲がある
Lean 4 自体を一価的な基礎理論として使うこと	適さない

本記事で問題にしているのは、後者です。

この区別を本文に入れると、入門者にとっては「では Lean 4 で HoTT のコードは一切書けないのか」という別の疑問が発生するため、本文では簡略化しました。

📌 中上級者向け：「排中律を最初から組み込んでいる」の厳密な意味

本文では、「Lean 4 は、排中律を最初から組み込んでいます」と表現しました。

より正確には、Lean 4 では排中律を公理として利用できます、と理解してください。

排中律

$$P \lor \lnot P$$

そのものを、自然数の足し算のような通常の計算規則として実装している、という意味ではありません。

同様に、選択公理も数学的な原理として利用されます。

この区別は、「計算規則として何が定義されているか」と「どの命題を公理として仮定できるか」を分けて考えるうえで重要です。

本連載の第１回目・第２回目の記事で扱った「公理として持つか、計算規則として持つか」という論点と、同じ区別です。

また、本文では「Lean 4 は、古典論理を前提として現代数学を広く形式化する道を選んでいます」とも述べました。

これも設計思想を直感的に説明する表現です。Lean 4 の核そのものを「古典論理そのもの」とみなすべきではありません。

Lean では、排中律や選択公理などの古典的原理を公理として利用できます。そのため Mathlib では、古典数学の多くを自然に形式化できます。

一方、これらの原理を使わずに構成的な証明を書くこともできます。

したがって「Lean 4 は古典論理しか使えない」という意味ではありません。本記事で述べているのは、Lean 4 の標準的な数学形式化環境では、古典数学で用いられる原理を利用できるという点です。

📌 中上級者向け：素イデアルの存在と選択公理の関係

本文では、構成的数学との対比を説明するため、「素イデアルの存在証明は、選択公理を使います」と説明しました。

より正確には、一般の環について素イデアルの存在を示す古典的な証明では、Zorn の補題が使われるという意味です。

Zorn の補題は、選択公理と同値な原理として知られています。そのため、選択公理から Zorn の補題を経由して、最大性を持つ対象の存在を示すことができます。

ただし、「素イデアルの存在は、論理的に必ず選択公理そのものを仮定しなければ証明できない」とまで一般化するのは注意が必要です。

環の種類や採用する基礎体系によって、より弱い原理で証明できる場合もあります。

また、本文で述べたロケールへの移行も、「選択公理がないから、仕方なく点を捨てる」という単純な話ではありません。

構成的数学では、点を前提としない空間の記述そのものに数学的な意味があります。

したがって本記事では、古典的な点ベースのスキームの構成が、構成的な設定ではそのまま維持できない場合がある、という具体例として扱っています。

なお、本文で「実物を作らずに『ある』と言っている」と述べた点についても、補足します。

構成主義が「証明できない存在をすべて否定する」という立場だと理解すると、誤解が生じます。

構成的数学で重要なのは、存在証明が、実際に対象を構成する情報をどの程度含んでいるかという点です。

$$\exists x : A,\ P(x)$$

という命題の構成的な証明は、一般には、具体的な $x$ と $P(x)$ の証明を与える情報を持ちます。

一方、

$$\lnot\lnot \exists x : A,\ P(x)$$

から

$$\exists x : A,\ P(x)$$

を導くには、一般には排中律などの古典的原理が必要です。

本文の「矛盾が出ることは示せても、実物を取り出せない場合がある」という説明は、この違いを直感的に示したものです。

記事全体について

📌 中上級者向け：本記事の Haskell と Lean 4 のコードについて

本記事に掲載した Arend のコードは、すべて実機で検証しました。

Arend 1.10（Java 21）

型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。

一方、Haskell と Lean 4 のコードについては、執筆環境に処理系を用意できませんでした。

これらのコードは、各言語の公式ドキュメントおよび標準ライブラリの記述に基づいて記述したものです。動作を保証するものではありません。

とくに、Lean 4 の型検査結果として示したエラーメッセージは、筆者が過去に別環境で確認した記録に基づくものです。 バージョンによって表示が異なる可能性があります。

📌 中上級者向け：訳語について

本記事で用いた訳語のうち、日本語として定着していないものがあります。原語を併記しておきます。

訳語	原語	備考
包摂的部分型付け	subsumptive subtyping	定訳が確認できませんでした
強制的部分型付け	coercive subtyping	同上
顕在フィールド	manifest fields	同上
匿名拡張	anonymous extension	Arend 固有の語です
部分実装	partial implementation	同上
可述的	predicative	「述定的」と訳す文献もあります
ホモトピーレベル	homotopy level	──

訳語の選定にあたっては、上村太一氏『ホモトピー型理論』を参考にしました。

上村太一『ホモトピー型理論』2023年

出典一覧

Arend

Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
https://arend-lang.github.io/assets/lang-paper.pdf
Language Reference, Arend Documentation
https://arend-lang.github.io/documentation/language-reference/
Tutorial, Arend Documentation
https://arend-lang.github.io/documentation/tutorial/
arend-lib（Arend の標準ライブラリ）
https://github.com/JetBrains/arend-lib

部分型付けと顕在フィールド

Xavier Leroy, "Manifest types, modules, and separate compilation", POPL'94
https://caml.inria.fr/pub/papers/xleroy-manifest_types-popl94.pdf
Zhaohui Luo, "Manifest Fields and Module Mechanisms in Intensional Type Theory", TYPES'08, LNCS 5497, 2009年
https://link.springer.com/chapter/10.1007/978-3-642-02444-3_15
Z. Luo, S. Soloviev, T. Xue, "Coercive subtyping: Theory and implementation", Information and Computation, vol. 223, 2013年, pp. 18–42
https://www.cs.mcgill.ca/~taoxue/docs/ic13_subtyping.pdf

Matita

A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi, "The Matita Interactive Theorem Prover", CADE-23, LNCS 6803, 2011年, pp. 64–69
https://link.springer.com/chapter/10.1007/978-3-642-22438-6_7
A. Asperti, C. Sacerdoti Coen, E. Tassi, S. Zacchiroli, "User Interaction with the Matita Proof Assistant", Journal of Automated Reasoning, vol. 39, no. 2, 2007年, pp. 109–139
https://link.springer.com/article/10.1007/s10817-007-9070-5
CerCo（Certified Complexity）プロジェクト
http://cerco.cs.unibo.it/

ホモトピー型理論

The Univalent Foundations Program, "Homotopy Type Theory: Univalent Foundations of Mathematics", Institute for Advanced Study, 2013年
https://homotopytypetheory.org/book/
上村太一『ホモトピー型理論』2023年（著者はホモトピー型理論の意味論を専門とする研究者。アムステルダム大学で博士号を取得。本記事の訳語は、これに従いました）
https://uemurax.github.io/hott-ja/0000.html

過去記事

『Haskellのbaseには群も環も体もない ── 代数構造を型クラスでどこまで表現できるか』
https://qiita.com/etale_cohomology/items/e39eec870aa5a2c93bc3

検証環境

本記事に掲載した Arend のコードは、すべて実機で検証しました。

Arend 1.10（Java 21）

型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。

一方、Haskell と Lean 4 については、執筆環境に処理系を用意できませんでした。

これらのコードは、各言語の公式ドキュメントおよび標準ライブラリの記述に基づくものです。

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

【Arend 連載④】モノイド、群、環、体。一本道ではない数学の代数構造の階層をArend はどうコードに記述するのか

本記事は、連載記事の第４回です

これまでの流れ

本記事の主題

本記事のExecutive Summary

本記事を読むと、何が分かるのか

定理証明言語で数学の代数概念を積み上げることが求められる理由

弊害① ── 同型なものが、等しくならない

弊害② ── 記述すると、膨大な量になる

弊害③ ── 構造の階層が、そのまま表せない

そこで、型理論への移行が始まった

この記事の結論

できること① ── 上位概念を、下位概念が求められる場面へ持ち込める

できること② ── レコードの項目の値を、定義の時点で確定させておける

できること③ ── 一部だけを埋めた中間の型を作れる

３つが揃うと、階層を自然に組み上げられる

本連載シリーズの第２回目の記事で述べたこと

本記事で扱う言語仕様も、同じ理由から来ている

では、土台に入れることの良い面と悪い面は、何なのか

土台に入れることのメリット

土台に入れることのデメリット

（土台ではなく）言語の外側で補うことのメリット・デメリット

どちらが優れているか、ではない

本記事には、Arend 以外の言語も登場します

本記事の議論の流れ

第２回目の記事を読まれた方へ

本記事の読み方

第１部 ── Haskell の Monoid には、法則がある

しかし、コンパイラは検査しない

Monoid の法則

式の読み方

守らなくても、コンパイルが通る

法則を型に書き込めないか

第２部 ── 依存型があれば、法則を型に記述できる

Arend で書いてみる

記号の読み方

１行ずつ読み解く

ただし、これは Arend 固有ではありません

では、Arend は何が違うのか

専任講師： そこを、次の部で扱います。

第３部 ── 本当の問題は、階層である

なぜ、型理論の上で数学を組み立てるのか

集合論で数学を基礎づけると、何が起きるのか

困難① ── 同型なものが、等しくならない

群でも、同じことが起きる

構造同一性原理

困難② ── 記述すると、膨大な量になる

そこで、型理論が選ばれた

なぜ、型理論だったのか

そして、定理証明支援系との接続

階層の設計は、一意に定まらない

どこで可換性を入れるか

Lean の Mathlib でも問題だった

それぞれの対処

代数構造の階層は、１本道ではない

整域とは何か

行列の世界でも、同じことが起こります

可換局所環と GCD 整域

可換局所環

多重継承とは何か

図にすると

専任講師： この形を、そのままコードで記述できるかどうか。それを、これから見ていきます。

第４部 ── Lean・Rocq／Coq・Agda は、土台を単純に保った

階層を記述するには、２つの仕組みが必要

ひとつ目 ── 包摂的部分型付け

２つ目 ── 顕在フィールド

「避けてきた」とは、どういうことか

シグマ型とは何か

強制的部分型付けとは何か

宇宙とは何か

型にも、型がある

通常の型理論では、宇宙は１つの数で並ぶ

Arend では、もう１つの軸が加わる

縦軸の「大きさ」とは何か

なぜ、階層に分ける必要があるのか

実際に確かめる

名簿にたとえると

Haskell との違い

「可述的」という語について

横軸のホモトピーレベルとは何か

第１部 ── Haskell の `Monoid` には、法則がある

`Monoid` の法則

専任講師：
そこを、次の部で扱います。

専任講師：
この形を、そのままコードで記述できるかどうか。それを、これから見ていきます。