📑

Mathematics in type thoery 日本語訳

2023/10/12に公開

数学とは何でしょうか？数学は基本的に４つのタイプに分類できると思います．定義，命題，証明，そしてアイデアです．

定義 (たとえば実数や $\pi$ ) や命題 (たとえばフェルマーの最終定理やリーマン仮説のステートメント) は数学の科学の一部です：こういったものは，ある基礎的なシステムの中で完全に厳密な意味を持ち，白黒はっきりしています．

証明はある意味で数学の通貨だといえます：証明は賞で報いられます．証明の構築は芸術であり，証明の検証は科学です．このことは，Lean, Coq, Isabelle/HOL, Agda などのコンピュータ証明検証システムが，証明を構築するよりもチェックすることをはるかに得意とする理由を，とても簡単に説明しています．

そしてアイデアは，数学の純粋に芸術的な部分です．「閃き」の瞬間，問題解決を可能にする洞察力，これこそが数学のとらえどころのないアイデアなのです．

アイデアは，形式的な意味で私が最も理解していない数学の一部です．ここに２つの疑問があります：

群とは何ですか？
群をどう考えていますか？

最初のものは正確な「科学的な」質問です．群とは，ある特別な構造を持ち，ある公理を満たす集合のことです．正式な答えは Wikipediaの群についてのページにあります．群とは定義です．しかし，２つめの質問は種類の異なる質問です．群について考える方法は人によって異なります． $G$ が $x^5=x^8=1$ を満たす要素 $x$ によって生成される群だとします． $G$ について何が言えるでしょうか？もしあなたが数学の学部生で，群の形式的な定義を見たばかりなら，おそらく何も言えないでしょう．群論をより深く理解している人なら，即座にこの群が自明であることがわかるでしょう．何が起こっているのかについて，はるかに洗練されたモデルを有しているからです．アイデアは複雑で，人によって異なるものです．「群とは何であるか」という問いについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．現在コンピュータは新しい定理を自力で証明することを苦手としていますが，その理由のひとつがこれです．コンピュータに群に関する定理を教えたり，群の例を教えたり，群論の定理や群の例を自動的に理解する AI を作ったりすることで，コンピュータの直感を発達させることができます．しかし直感というのはとても微妙なもので，私にはまったく理解できないので，ここではこういったアイデアについてはこれ以上語らないことにします．写像が canonical (正準) であるという概念は，定義というよりむしろアイデアだと思います．数学者によって，このイタチごっこのような言葉に対する考え方は違ってくるでしょう．この記事では，他の３つの概念 (定義，命題，証明) が型理論や Lean theorem proverでどのように実装されているかについてお話しようと思います．

定義，命題，証明

アイデアとは対照的に，数学の他の部分（定義，定理/予想, 証明）は基礎的なシステムで形式化することができ，したがって精確な方法でコンピュータ上に作成・保存することができます．これは pdf ファイルのことではありません！pdf ファイルこそ，私が脱却したいものなのです！つまり，様々ある数学の基礎付け（集合論，型理論，圏論）のうち1つを理解するコンピュータプログラミング言語が設計されており，その言語で数学者が問題の定義，命題，証明を書くことができるということです．

私には，圏論でどのように数学の基礎付けを行うのかを説明する資格はありません．集合論について，ひとつだけ観察してみましょう．集合論における定義，たとえば実数や $\pi$ の定義は集合です．そして証明とは，論理のステップをつなげたものです．集合論において，定義と証明は全く異なるもののように私には思えます．群とは，定義と証明の混合物です．―― 群とは，順序付き4つ組 $(G,m,i,e)$ であって，特定の公理を満たすもののことです．つまり，論理が付属した集合です．

しかし，型理論では驚くほど違います．今挙げた３つのもの ―― 定義，命題，証明 ―― はすべて同じ種類のものです！これらはすべて項です．群，証明，実数 ―― これらもすべて項です．定義と証明の統一，つまり集合と論理の統一が，型理論を実用的な基礎システムたらしめ，コンピュータに学部レベルのすべての数学を教えることを可能にしています．

宇宙，型，項

型理論では，すべてが項です．そしていくつかの項は型でもあります．すべての項が型であるわけではありませんが，すべての項は型を持っています．Lean では，コロンを使って項の型を表します．―― x : T という表記で，x が T という型の項であることを表します．たとえば，実数 $\pi$ は Lean の項であり，実数全体 $\mathbb{R}$ は型であり，π : ℝ が成り立ちます．つまり， $\pi$ は型 $\mathbb{R}$ の項です．集合論では $\pi\in\mathbb{R}$ と書きますが，型理論では π : ℝ と書きます．どちらも同じ数学的概念，つまり「 $\pi$ は実数である」を表します．

いま $\pi$ は項ですが，型ではありません. Lean では x : π は意味を持ちません．集合論では， $x\in\pi$ は意味を持ちますが，これは集合論において全てが集合であることに起因する，奇妙な偶然です．さらに， $\pi$ の実際の要素は，実数がどのように実装されるか（たとえばデデキント切断としてか，コーシー数列としてか）に依存するため，集合論での $x\in\pi$ は，構文的には意味を持つものの，数学的な意味はありません．たまたま意味をなすだけで，システムの癖に過ぎません．もし「 $x \in \pi$ には意味があるはずだ」とあなたが断固として言うなら，「あなたは集合論に洗脳されているのだ」と私は言うでしょう．ガウスとオイラーがあなたを正しい方向に導いてくれるでしょう：ガウスとオイラーは，コーシーとデデキントが数列と切断を導入する以前に，実数に関する定理を証明していました． $\pi$ が要素を持つべき理由はありません．これは数学の基礎に集合論を使った際の癖であり，その癖は型理論を使った場合には解消されます．

先ほど，すべての項は型を持つと書きました．では ℝ の型はなんでしょうか？ℝ : Type が答えです．実数全体は，Type と呼ばれる「宇宙」型の項です ―― これは「すべての集合がなすクラス」の型理論における類似物です．

数学者が定義する数学的対象の多くは，型 Type を持つか，あるいは T : Type であるような型 T を持ちます．漠然とした経験則ですが，要素を持つもの（群，環，体など）は Type 型を持ち，要素を持たないもの（ $\pi$ , $\sqrt{2}$ や一般の群の要素 $g$ ）は T 型を持ちます．もう一つのあいまいな経験則として，大文字で書くもの（群や環など）や fancy letter（実数 ℝ や有理数 ℚ ）で書くものは Type 型を持ち，小文字で書くもの（群の要素 $g$ や実数 $r$ , 整数 $n$ ）は T 型を持つ傾向にあります．たとえば 2 : ℕ と ℕ : Type が成り立ちます．また $g$ が群 $G$ の要素であるとき，Lean では g : G と G : Type が成り立ちます．ここには３層の階層があります ―― 一番下に項があり，その上に型があり，最上部に宇宙があります．

宇宙 : Type
具体的な型 : ℝ, ℕ, G (群), R (環), X (集合論者が集合と呼ぶなにか), バナッハ空間など. 形式的には ℝ : Type などと書きます.
具体的な項 : π (型 ℝ の項), g (群 G の要素, つまり型 G の項), x (X の要素, つまり型 X の項). 形式的には g : G などと書きます.

この階層は，クラス（たとえばすべての集合のクラス）と集合の２つのレベルしかない集合論の階層よりも，表現力が高いです．

数学におけるコロンの標準的な使い方があります．―― 関数を書くための記法です．X と Y が集合（集合論を使っている場合）または型（型理論を使っている場合）であるとき，X から Y への関数を f : X → Y と書きます．これは実は Lean におけるコロンの使い方と一致しています．X から Y への関数の集まり $\mathrm{Hom}(X,Y)$ に対する Lean の表記法は X → Y であり，これは型です．（つまり X → Y : Type です．これは集合論で $\mathrm{Hom}(X,Y)$ を集合と考えることに対応しています）f : X → Y は f が X → Y 型の項であることを意味し．集合論でいう $f \in \mathrm{Hom}(X,Y)$ に対応します．これは型理論において，f が X から Y への関数であることを書き表すやり方です．

（これは試験に出ません）厳密に言えば，宇宙は型であり，型は項ですが，これは用語の問題です．多くの場合，ひとが型について語るとき，それは宇宙ではない型を意味し，ひとが項について語るとき，それは型ではない項を意味します．しかし常にそうとは限りません．私が初心者の頃は，これで混乱しました．

定理と証明

ここからが楽しいところです．ここまで，型とは型理論における集合の呼び名であり，項とは型理論における要素の呼び名でした．しかし，ここで Lean の型理論におけるもう一つの宇宙，命題の宇宙 Prop を見てみましょう．そこで起こることは，私たちの伝統的なメンタルモデルとは全く異なります．ここでは，定理のステートメントと証明が，型や項と同じようにどのようにモデル化できるかを見ていきます．

定理のステートメントと証明はどのようにモデル化されるのでしょうか？Lean の型理論には Type という宇宙だけでなく，Prop という第二の宇宙があります．Prop 型の項は命題です．ここで残念な表記の衝突があります．数学では，proposition (命題)という言葉はしばしば定理のこどもという意味で使われますが，定理は真です．（そうでなければ予想や反例と呼ばれます）したがって，数学において命題という言葉は真である文を指しますが，ここでは，論理学者と同じように命題という言葉を使います．つまり，命題とは一般的な真か偽かどちらかになる文のことであり，それが正しいか誤りかは関係ありません．

例を見るとわかりやすいでしょう． $2 + 2 = 4$ は命題なので 2 + 2 = 4 : Prop と書くことができます．しかし， $2 + 2 = 5$ も命題なので，2 + 2 = 5 : Prop と書くこともできます．何度も言いますが，命題が真である必要はありません！命題は真か偽かどちらかになる文のことです．もう少し複雑な例を見てみましょう．

「すべての自然数 $x$ について $x + 0 = x$ である」という文は命題です．Lean では，これは (∀ x : ℕ, x + 0 = x) : Prop と表せます．命題は Prop 型を持つ項です．（先ほど見てきた項が型 Type を持っていたのと同様です）RH をリーマン仮説のステートメントとします．すると RH : Prop となります．それが真か偽か，特定の数学の公理と独立であるか，決定不能であるか，等は問いません．命題とは真か偽かどちらかになる文のことです．Lean の型理論の階層のうち，Prop 宇宙に住む部分を見てみましょう．

宇宙 : Prop
具体的な型 : 2 + 2 = 4, 2 + 2 = 5, フェルマーの最終定理のステートメント，リーマン仮説のステートメント
具体的な項 : ??

この３層構造の Prop 階層において，項にあたるものは何でしょうか？それは証明です！

命題は型，証明は項

これは，型理論の世界と集合論の世界との，そして３年前までの私の脳内世界との大きく異なる点です．何が起こっているのか理解しようとして，私は数学者が用語の濫用を行っていることに気づきました．まずそれについて考えてみましょう．ボルツァーノ＝ワイエルシュトラスの定理とは, 解析学における, 収束する部分列を持つ有界数列についてのステートメントです．数学者が「ボルツァーノ＝ワイエルシュトラスの定理」という言葉を実際にどのように使うかについて，少しお話ししましょう．数学者は，「ボルツァーノ＝ワイエルシュトラスの定理とは，収束する部分列を持つ数列に関するこのステートメントのことだ」と言うでしょう．しかし証明の途中で，証明を続けるためにこの定理を適用する必要がある場合は，「ボルツァーノ＝ワイエルシュトラスの定理によって，収束する部分列があることが推論される」と言います．何もおかしなことはないように思えます．しかし，私が指摘したいのは，「ボルツァーノ＝ワイエルシュトラスの定理」という言葉が２つの異なる意味で使われている，ということです．「ボルツァーノ＝ワイエルシュトラスの定理とは何か」という場合，かれらは定理のステートメントに言及しています．しかし，「ボルツァーノ＝ワイエルシュトラスの定理を使って」という場合，実際に使っているのはその証明です．バーチ・スウィンナートン＝ダイアー予想は，完全に整った命題であり，それが何であるかを正確に言うことができます．しかし，ある証明を完全なものにしたいのであれば，バーチ・スウィンナートン＝ダイアー予想をその証明の途中で使うことはできません．なぜなら現時点でこの予想は未解決問題だからです．ここで重要なのは，定理のステートメントと定理の証明とを明確に区別することです．数学者は「ボルツァーノ＝ワイエルシュトラスの定理」という言葉を，どちらの意味でも使うことがあります．このような非形式的な表記の濫用は初学者の混乱を招きます．なぜなら，以下では定理のステートメントと定理の証明を区別することが本当に重要だからです．この２つは全く異なるものです．

natural number game (自然数ゲーム) ^[1] の中で，私は数学者を相手にしていたのでこのような表記の濫用を行っていました．∀ x : ℕ, x + 0 = x という文は真であり，「これは Lean では add_zero と呼ばれる」と私は言っていました．natural number game において，私は add_zero : ∀ x : ℕ, x + 0 = x と書いていました．しかし，これが何を意味するかといえば，Lean で add_zero と呼ばれる項が ∀ x : ℕ, x + 0 = x の証明である，ということなのです！コロンは型理論的に使われています．私は natural number game では意図的にこの概念を曖昧にしました．add_zero はすべての $x$ に対して $x + 0 = x$ であるという「アイデア」と何らかの形で等しいと，数学者に信じさせたわけです．しかし裏では ∀ x : ℕ, x + 0 = x は命題であり，型でもあり，add_zero はその証明であり，項でもあります．ここで重要なのは，定理のステートメントとその証明を区別することです．ステートメントは型であり，証明は項です．

宇宙 : Prop
具体的な型 : 2 + 2 = 4, 2 + 2 = 37, フェルマーの最終定理 ∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0
具体的な項 : 2 + 2 = 4 の証明（2 + 2 = 4 型を持つ項），フェルマーの最終定理の証明（∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0 という型を持つ項）

定理の要素

つまり π : ℝ というステートメントに対する私たちのメンタルモデルは，型である ℝ は「ものの集まり」であり，項である π はその集まりのメンバーである，ということです．このアナロジーを続けるなら，2 + 2 = 4 というステートメントはある種の集まりであり，2 + 2 = 4 の証明はそのメンバーです．言い換えれば，Lean は 2 + 2 = 4 をある種の集合であるとし，2 + 2 = 4 の証明はその集合の要素であるとするようなモデルを提案しているのです．Lean では，ある命題の証明はすべて等しいという公理が組み込まれています．つまり a : 2 + 2 = 4 かつ b : 2 + 2 = 4 ならば a = b となります．これは Prop 宇宙の中だから起こることです ―― これが Lean における命題の振る舞いです．Type 宇宙の中ではこのようなことはありえません．―― π : ℝ かつ 37 : ℝ ですが， $\pi\not=37$ です．この Prop 宇宙の特別な癖は「proof irrelevance (証明無関係)」と呼ばれます．形式的には，P : Prop に対して a : P かつ b : P ならば a = b である，と言い表せます．もちろん，ある命題が偽ならば，その命題には証明は全くありません！偽の命題は空集合のようなものです．つまり，Lean の命題のモデルは，真の命題は１つの要素を持つ集合のようなもので，偽の命題は $0$ 個の要素を持つ集合のようなものだと言っています．

f : X → Y であるとき，f は X から Y への関数であるということを思い出しましょう．ここで， $P$ と $Q$ を命題とし， $P\implies Q$ がわかっているとします．これは何を意味するでしょうか？これは $P$ ならば $Q$ であるということを意味します． $P$ が真であるとき， $Q$ も真だということです． $P$ の証明があれば， $Q$ の証明も作れるということです． $P\implies Q$ は $P$ の証明から $Q$ の証明を得る関数です． $P$ の要素を $Q$ の要素に送る関数です．P → Q 型を持つ項です．繰り返しますが， $P\implies Q$ の証明は h : P → Q という項 h です．natural number game で，私が → 記号を含意を表すのに使ったのは，このためです．

false を一般的な偽の文（ $0$ 個の要素を持つ集合と考えられる）とし，true を一般的な真の文（ $1$ 個の要素を持つ集合と考えられる）とします．false → false 型の項，または true → true 型の項を作ることはできるでしょうか？もちろんです．―― 恒等関数を使えばよいだけです．実際，どちらの場合も関数は一意に定まります．―― hom 集合のサイズは $1$ です．false → true 型の項を作ることはできるでしょうか？もちろん， $0$ 個の要素を持つ集合から $1$ 個の要素を持つ集合への関数はあり，この関数も一意です．では true → false 型の項を作ることはできますか？これはできません．true の証明をどこに送ればいいのでしょうか？false の証明は存在しないので，送る先がありません．したがって true → false はサイズ $0$ の集合です．これは → の標準的な真理値表に相当し，最初に分析した３つの文は真で，最後の文は偽です．

フェルマーの最終定理の証明は関数

では ∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0 の証明とはどのようなものでしょうか？この命題には矢印が含まれているので，フェルマーの最終定理のステートメントは $\mathrm{Hom}(A,B)$ という形の集合の一種です．Lean では，フェルマーの最終定理の証明は実際に関数です！その関数が何をするかは次の通りです．それは４つの入力を持ちます．最初の３つの入力は自然数 x, y, z です．４番目の入力は証明で，命題 n > 2 ∧ x^n + y^n = z^n の証明です．そして出力は命題 x*y=0 の証明です．これは「フェルマーの最終定理の証明とは何か」という問いについてのきわめて型破りな考え方であり，証明を実際に理解しようとする際には全く役に立たないことを強調しておきましょう． ―― しかし，これは数学がどのように機能するかについての完全に一貫したメンタルモデルです．数と証明の概念を統一することで，―― つまり両方を項として考えることで，―― 証明を関数として考えることができます．Lean は関数型プログラミング言語であり，特に関数を中心に設計されています．現在 Lean や Coq や Isabelle/HOL といった型理論を使用する証明支援系が，Metamath や Mizar のような集合論を使用する証明支援系より進んでいるのは，このためだと私は確信しています．

定理を証明しましょう！関数を書きましょう！


宇宙	`Type`	`Prop`
型の例	ℝ	2 + 2 = 5, (∀ a : ℕ, a + 0 = a)
項の例	37, π	`add_zero`, `rfl`

訳者: @aconite-ac, @Seasawher

脚注

訳注: natural number game は，ペアノの公理から始めて整数の基本的な性質を Lean で示すブラウザゲームです．ここで紹介されているのは Lean3 版ですが，Lean4 版がこちらにあります．ソースコードはこちらです． ↩︎

GitHubで編集を提案