💻 computer science

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

本論文は、Cubical Agda におけるホモトピー型理論に基づくコーシー実数の構成を形式化し、このアプローチが他の構成的定義に内在する可算選択、セトイドのオーバーヘッド、および宇宙レベルの追跡の問題を回避しつつ、公理なしで型チェックされることを示す。

原著者： Jackson Brough

公開日 2026-04-29

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Jackson Brough

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

宇宙のすべてを測定するための完璧で無限の定規を構築しようとしていると想像してください。古典数学の世界では、この定規は簡単に記述できます。すべての可能な「近似」測定値（3.1、3.14、3.141 など）を採取し、「2 つの測定値の列が互いに限りなく近づけば、それらは定規上の同じ点を表す」と言えばよいのです。

しかし、構成主義数学（実際に議論している対象を「構築」または「計算」できなければならないと主張する数学のスタイル）では、この単純なアプローチは行き詰まります。定規が完備であることを証明するには、魔法のような選択を行う必要があります。つまり、最終的な点を表すために、無限の選択肢から特定の測定値を 1 つ選び出すのです。構成主義数学は、「魔法は禁止だ。どのように選んだのかを示せなければ、まだ定規を構築したことにはならない」と言います。

長年にわたり、数学者たちは妥協を余儀なくされました。彼らは計算を煩雑にする「帳簿付け」のトリックを使うか、あるいは「宇宙レベル」（箱の大きさを記録するようなもの）の追跡を必要とする方法で定規を構築していました。

新しい設計図（HoTT 書における実数）
この論文は、有名な『ホモトピー型理論（HoTT）』の書物から取り入れられた、定規を構築するための新しい設計図を提示します。この方法は、部品を貼り合わせてからそれらを滑らかにしようとするのではなく、定規と「滑らかさ」の規則を同時に構築します。

壁と設計図が完全に同時に描かれている家を建てると考えてください。

レンガ: 分数のような、単純で既知の数から始めます。
接着剤: 「2 つの点が十分に近ければ、それらは実際には同じ点である」という特別な規則を追加します。
魔法: 「近さ」の規則が家そのものの定義に組み込まれているため、後でそのような魔法のような選択をする必要はありません。レンガを敷き終えた瞬間、家は完成します。

課題：コンピュータ翻訳者
著者のジャクソン・ブラフは、この理論的な設計図を、コンピュータが理解し検証できる言語であるCubical Agdaに翻訳しようと試みました。

複雑なダンスの振り付けを、厳格で文字通りの指示しか理解できないロボットに説明しようとしていると想像してください。

問題: この設計図を翻訳しようとした以前の試みは失敗しました。コンピュータ言語には適切な「動き」（具体的には、定規と近さの規則の同時定義を処理する能力）が欠けていたからです。翻訳者は「この動きが存在すると仮定する」と言わざるを得ず、それは数学における不正行為でした。
解決策: Cubical Agda は、これらの複雑な動きをネイティブに理解する、より新しく、賢いロボットです。これにより、著者は不正行為をすることなく、設計図を設計された通りに正確に記述することができました。

翻訳中に何が起こったか
この論文は単にコードを入力することについてではなく、著者がコンピュータに数学を理解させようとした際に何が起こったかについてです。コンピュータの厳格さは、著者に元の説明に潜んでいた隠れた隙間を見つけることを強制しました。

「代替」マップ: 元の書物は、2 つの点が近いかどうかをチェックする方法を記述していました。しかし、著者がコードを書こうとしたとき、本の手法は「一方通行の道」のようなものであることに気づきました。点が近いことを証明することはできても、なぜそうなのかを逆方向に簡単にたどることはできませんでした。著者は、コンピュータが実際に答えを計算できるようにする、逆ギアとして機能する第 2 の「計算用」マップ（代替関係と呼ばれる）を構築する必要がありました。
欠落した成分: 書物は、コンピュータが元の近似値のリストを「記憶」できるかのように、関数（乗算など）を構築する規則を記述していました。著者の最初のコードバージョンはこの記憶を失っていました。コンピュータはそれを拒否しました。著者は、規則を書き直し、記憶を明示的に引き継ぐようにしなければなりませんでした。これにより、元のテキストが機械にとってはあまりにも曖昧であったことに気づきました。
多変数のパズル: 書物は、単一の数に対する規則が、数値のペアやトリプルにも容易に適用できることをほのめかしていました。しかし、コンピュータは納得しませんでした。著者は、ある規則が 1 つの変数に対して機能すれば、それらを 1 つずつチェックする限り、2 つの変数に対しても機能することを示す、新しい特定の補題を証明する必要がありました。

結果
最終的な成果物は、HoTT 書の実数が完璧に機能することを証明する、大規模なオープンソースのコードライブラリ（13,000 行以上）です。

これらの数が完備された順序体（加減乗除と比較が可能）を形成することを証明します。
定規が「アルキメデス的」であることを証明します（つまり、どれだけ小さな隙間があっても、その中に収まる分数を常に発見できることを意味します）。
最も重要なのは、これらすべてが不正行為なしで行われたことです。コンピュータはすべてのステップを検証し、コードは「魔法の仮定」なしで実行されます。

まとめ
この論文は、美しく高水準な数学的なアイデアを、厳格で文字通りのコンピュータ検証の世界で生き残らせるための物語です。それによって、著者は単にデジタル定規を構築しただけでなく、設計図そのものを磨き上げ、隠れた詳細を明らかにし、理論を以前よりも強固で精密なものにしました。このコードは、将来の数学的発見のための確固たる基盤として、誰でも利用できるようになっています。

ジャクソン・ブラウフによる学位論文「Cubical Agda におけるホモトピー型理論での実数の形式化」の詳細な技術的要約を以下に示す。

1. 問題提起

構成主義的数学は、数学的証明に対して計算的解釈を提供することを目指しているが、実数（ $\mathbb{R}$ ）の構成は歴史的に重大な妥協を必要としてきた：

古典的コーシー構成： コーシー列の同値類から代表元を選択してコーシー完全性を証明するために、可算選択公理を必要とする。これは非構成主義的である。
ビショップのセトイド構成： 明示的な同値関係（セトイド）を備えたコーシー列を扱うことで選択を回避する。しかし、これは永続的な管理オーバーヘッドをもたらす。すべての演算と定理に対して明示的な合同証明を必要とし、代数構造を複雑にする。
デデキント切断： 述語的型理論において、デデキント切断は宇宙レベルの追跡を必要とする（実数はその切断より一つ上のレベルに存在する）ため、展開が煩雑になる。

HoTT 書（ホモトピー型理論）は、実数を**高次帰納的帰納的型（HIIT）**として定義することで解決策を提案している。この構成は選択を回避し、パス構成子を通じて $\epsilon$ -近接な実数を同一視することでセトイドのオーバーヘッドを排除し、宇宙レベルの追跡を不要にする。しかし、ギルバートによる Rocq での以前の形式化などは不完全であった。なぜなら、証明支援系が HIIT をネイティブにサポートしていなかったため、著者はパス構成子とその計算則を導出するのではなく、**仮定（postulate）**せざるを得なかったからである。

2. 手法

本論文は、Cubical 型理論に基づく証明支援系Cubical Agdaを用いた、HoTT 書の実数に関する完全な機械検証形式化を提示する。

ネイティブサポート： Cubical Agda は高次帰納的型（HIT）と帰納的帰納的定義をネイティブにサポートしている。これにより、著者はパス構成子の計算則がネイティブに存在することを確認しつつ、仮定なしで実数と近接関係を同時に定義できる。
形式化の範囲： この作業は 13,000 行以上のコードを形式化しており、以下の項目を網羅する：
1. $\mathbb{R}$ の HIIT 定義と近接関係（ $\sim_\epsilon$ ）。
2. 帰納原理と再帰原理。
3. 近接関係の性質（反射律、対称律、三角不等式、丸め性）。
4. リプシッツ連続かつ非拡大写像に対する拡張原理。
5. 代数演算の構成（加法、否定、最小/最大、乗法、逆数）。
6. 順序論（厳密/非厳密不等式、分離性）。
7. $\mathbb{R}$ がアルキメデス順序体をなすことの証明。
ツール： 著者は、大規模な Cubical Agda 標準ライブラリのナビゲーションと、非公式な証明スケッチを形式的な Agda 項への変換を支援するために、Claude Code（Anthropic の AI エージェント）を活用した。これにより、逆数の構成のような複雑な証明の開発が大幅に加速された。

3. 主要な貢献

A. HoTT 実数の最初の完全な形式化

これは、仮定に依存しないHoTT 書の実数の最初の形式化である。以前の試みはパス構成子の存在を仮定せざるを得なかったが、本研究は Cubical Agda 型理論から直接それらを導出しており、すべての計算則が定義的に成り立つことを保証する。

B. 形式化のギャップの解消

形式化のプロセスは、HoTT 書の非公式な提示における微妙な問題を検出し、数学的な洗練を必要とした：

代替的な近接関係： 近接（ $\sim$ ）の帰納的定義は、証人を抽出するための十分条件を提供するが、必要条件ではない。形式化は、構成子上で計算する補助関係（ $\approx$ ）を厳密に構成し、 $\sim \iff \approx$ を証明することで、近接の仮定に対する場合分けを可能にした。
強化された再帰原理： 非公式テキストにおける再帰原理の記法は、帰納的仮説内でドメイン近似（ $x_\epsilon$ ）へのアクセスを暗黙的に仮定していた。形式化では、近似と値域割り当ての両方を運ぶように再帰原理を明示的に再定式化する必要があり、これは当初の単純な転写では見落とされていた。
多変数の連続性： HoTT 書は、恒等式を多変数へ拡張するために個別の連続性で十分であることを示唆している。形式化はこれを明示的に証明し（補題 2.3.4）、個別の連続性が $\mathbb{Q}$ から $\mathbb{R}$ への二変数および三変数の恒等式の拡張に十分であることを示した。

C. 乗法と逆数の構成

乗法と逆数は大域的にリプシッツ連続ではないため、単純な拡張原理を通じて定義できない。本論文はギルバートの局所から大域への戦略を採用する：

リプシッツ境界が存在する制限されたドメイン上で演算を定義する（例：一方の因子の境界を固定する）。
これらの局所的定義が重なり部分で一致することを証明する。
クラウスの定理（命題的切断から集合への写像）を用いて、特定の境界への依存性を排除し、大域的な定義を得る。
このアプローチは、Cubical Agda 標準ライブラリの SetElim モジュールを用いて実装された。

D. 計算効率

Lean における古典的商構成（実数における $2+2=4$ が定義的真ではない）とは異なり、Cubical Agda における HoTT 構成は、有理数入力に対する算術を定義的に計算可能にする。例えば、rational(2) + rational(2) = rational(4)は、型チェッカー内で直接refl（反射律）に簡約される。

4. 結果

アルキメデス順序体： 形式化は、構成された型 $\mathbb{R}$ が、ゼロから分離した要素の逆元の存在を含む、アルキメデス順序体のすべての公理を満たすことを成功裏に証明した。
コードの入手可能性： 完全なコードベース（約 13,500 行）はオープンソースであり、最新の Cubical Agda 標準ライブラリを用いて、穴や仮定なしに型チェックされる。
AI 支援開発： 本論文は、大規模ライブラリのナビゲーションと、高レベルの証明戦略から低レベルの依存型項への翻訳において、LLM ベースのコーディングエージェントを形式数学に利用する有効性を示している。

5. 意義

構成主義的解析の基盤： この作業は、ユニバレント基礎プログラム内における構成主義的解析のための堅牢で機械検証された基盤を提供する。それはセトイドの「管理」負担と、古典的商の「選択」負担を取り除く。
証明支援系の進化： NATIVE HIT サポートを欠く Rocq（Coq）などのシステムと比較して、HIT ベースの数学にとって Cubical Agda が優れている環境であることを実証する。
今後の課題： この形式化は、リーマン積分や微分方程式など、より複雑な構造への構成主義的解析の拡張や、ロケーター（実数上で計算を可能にする構造）のような概念をより一般的な距離空間へ一般化するための舞台を設定する。
方法的洞察： 本論文は、形式化が単なる検証作業ではなく、非公式な読書だけでは発見できない暗黙の仮定を明らかにし、定理を洗練させる数学的活動であることを浮き彫りにしている。

要約すると、ジャクソン・ブラウフの学位論文は、HoTT 書の実数の理論的優雅さと、実用的で実行可能な数学との間のギャップを埋め、型理論における実解析のための検証済み、計算効率的、かつ仮定のない基盤を提供している。