- 依存型(type theory) は証明オブジェクトを含むが、著者はこれを不要で非効率な構造だと評価している
- AUTOMATH や Martin-Löf型体系 など、過去の依存型ベースのシステムを自ら研究したが、Isabelle は汎用的(generic)な論理フレームワークへと発展した
- 単純型理論(higher-order logic) を基盤とする Isabelle/HOL は、自動化・大規模ライブラリ・可読性に強みを持つ
- ALEXANDRIAプロジェクト を通じて、高階論理だけでも高度な数学定理の形式化が可能であることを実証した
- Lean などの依存型システムが成熟したにもかかわらず、性能問題と複雑さのため、著者は今なお高階論理アプローチの実用性を好んでいる
依存型と証明オブジェクト
- 依存型理論では 証明オブジェクト(proof objects) が必須だが、著者はこれを空間の無駄とみなしている
- LCF 構造では、論理の内部ではなく実装言語レベルの型検査によって、正当な証明ステップだけを実行可能にする
- Robin Milner の洞察により proof kernel の概念が導入され、Isabelle の基盤となった
- 著者は「依存型を使わなかったのか」という問いに対して、「長い間使っていた」と答えている
AUTOMATH の経験
- 1977年に Caltech で N. G. de Bruijn の AUTOMATH 講義を受けたが、システム自体は直接使えなかった
- 当時は Eindhoven 大学のシステムが ARPAnet に接続されておらず、ALGOL 60 ベースのコンピュータが必要だったため
- AUTOMATH は依存型システムだが、Curry–Howard 対応は実装していなかった
- ユーザーが望む論理の記号と推論規則を公理として追加しなければならなかった
- de Bruijn はこれを「あらゆる料理を出す大きなレストラン」にたとえた
- Isabelle はこの発想を引き継ぎ、論理フレームワークとしての一般性を追求した
- しかし de Bruijn は集合論を嫌悪し、数学を本質的に型ベースのものと見ていた
- 著者は AUTOMATH の正当性検証について質問したが、de Bruijn は言語理論書(300ページ) を送ってきただけで、満足のいくものではなかった
Martin-Löf 型理論
- ヨーテボリの Chalmers 大学で Martin-Löf 型理論を研究し、プログラム合成の可能性に魅了された
- Heyting の直観主義論理の原理を直接実装している点で、「正しさ」が明確だと評価した
- 数年にわたり研究を進め、Isabelle の初期バージョンを Martin-Löf 理論で実装した
- 現在も Isabelle/CTT として配布物に含まれている
- しかし Per Martin-Löf 中心の教条的な雰囲気と、強制された内包的同値(intensional equality) への転換によって研究は崩れた
- その後に登場した Calculus of Constructions(CoC)、Rocq、Lean などにも同じ疑問が残った
- CoC は数十年にわたり、さまざまな変種と選択的公理を重ねてきた
研究上の選択と Isabelle の方向性
- 研究者は、新しい形式体系の開発と既存体系の拡張活用のどちらかを選ばなければならない
- Isabelle は一般化されたフレームワークとして設計され、さまざまな論理を受け入れる
- 1985年、Mike Gordon は Church の単純型理論でハードウェア検証を行った
- その後 John Harrison がベクトル次元のエンコーディングを考案した
- Isabelle/HOL は Church 理論に公理的型クラスと locale モジュールシステムを追加した
- Lean コミュニティは CoC ベースで膨大な数学形式化(mathlib) を実現した
ALEXANDRIA プロジェクトと高階論理の限界実験
- ERC 支援の ALEXANDRIA プロジェクトは、Isabelle の自動化・ライブラリ・可読性を強調した
- 当初は高階論理では限界があるだろうと予想していたが、実際には Grothendieck スキーム などの高度な数学も成功裏に形式化された
- Paulo Emílio de Vilhena と Martin Baillon は、すべての体が代数的閉包拡大を持つことを証明した
- プロジェクトは Balog–Szemerédi–Gowers 定理 などの高度な結果にまで拡張された
- 「依存型なしでは数学形式化は不可能だ」という主張は消え、「依存型の方がよりきれいだ」という主張だけが残った
Lean と依存型に対する現在の立場
- Lean のコミュニティ規模と Blueprint ツールはうらやましいが、性能問題と複雑さは依然として残っている
- intensional equality との衝突や、依存型を使うべき時期の判断の難しさが繰り返し報告されている
- 著者は依存型を Tesla の完全自動運転(Full Self-Driving) にたとえ、過剰な期待と現実の不便さを指摘している
付録: 高階論理の理論的限界
- 一部では高階論理は証明論的に弱いと主張されるが、これは ZF 集合論に比べて弱いという意味にすぎない
- ALEXANDRIA の結果によれば、高階論理でも Grothendieck スキームなど複雑な数学構造を扱える
- ただ2つの証明だけが ZF 公理の追加を必要とし、それらは ZF オブジェクトを直接言及する定理だった
脚注
- 直観主義は言語を単なる記録手段とみなす哲学であり、今日の 構成的数学(constructive mathematics) とは異なる
1件のコメント
Hacker Newsの意見
依存型(dependent types) は特定の状況では非常に有用
たとえば Python が「10×5 サイズの float32 行列」を型として表現し、型チェックできたらよいと思う
しかし Curry–Howard 対応のように証明と型を同一視する概念は、人間の立場では混乱しやすい
型エラーは単に修正可能なミスのように感じられるが、証明エラーははるかに複雑で思考を要する問題だ
そのため Lean の本当の強みは型システムではなく、コミュニティと mathlib のオープンソース構造にあると見る
Isabelle の AFP が学術誌のように運営されている一方で、Lean は pull request ベースの協業が活発だ
現在私は新しい定理証明器 Acorn(acornprover.org)を開発中で、Lean と Isabelle の長所を結び付けようとしている
Lean のシンプルな依存型の表現力はよいが、深く使いすぎるとデバッグが難しくなる
ただし実行時にしか分からないインデックスの範囲をコンパイル時に保証することはできない
真の依存型言語は 実行時エラーを型レベルで防止できる
実際、依存型言語でも実行時エラー防止のために依存型を使うことはまれで、
主に データ構造の不変条件やプログラム定義後の検証に使われる
関連参考: division-by-zero in type theory FAQ, Xavier Leroy 発表資料
たとえば このコード の 38 行目のように、型で行列サイズを表現できる
ベクトル型定義 や
行列乗算の結果型 も実装した
ただし個人プロジェクトの範囲で実験中であり、大規模データプロジェクトには向かないかもしれない
これは Propositions as Types の概念と関係している
実行時に依存型がどう動くのか、コンパイル時と実行時の両方で型チェックが必要なのか気になる
実装時に 間接参照が増える複雑さが生じないのかという疑問がある
Dr. Paulson の主張は依存型が悪いということではなく、必須ではないという点だ
Lean の性能問題や 内包的同値(intensional equality) に関する議論がもっとあってもよかった気がする
Isabelle の HEq(リンク) のように、定義的同値でない場合が問題を引き起こす
だから私は依存型を可能な限り少なく使うほうがよいと思う
ACL2 のように静的型のないシステムでも十分に検証は可能だ
結局重要なのは 実用性と検証可能性のバランスだ
Lean や Agda はまだ産業規模の検証ではあまり使われていない
Concrete Semantics(リンク) と Logical Verification 2025(リンク) を比較してみるのも興味深い
現実的には refinement types のほうが実用的かもしれない
例: Rust Creusot, Dafny, LiquidHaskell の leftpad 証明例
しかしプログラム検証では「2つの証明が同じだ」といった 複雑な補題(lemma) が必要になり、これは証明できない場合が多い
重要なのは機能が どれだけ有用かであり、存在の必要性の有無ではない
結局ツール選択は 開発者の好みと効率性の問題だ
現代論理学の論争のかなりの部分が 美的嗜好に帰着するという点が興味深い
実質的な利点が圧倒的なら論争はなかったはずだ
参考までに、Paulson と Lamport の 1999 年の論文 “Typing in Specification Languages” は良い読み物だ
その後、Lamport の TLA+ のような 非形式的形式主義も発展した
コンパイル時保証という利点を得る代わりに、複雑さとビルド時間増加という代償を払う
結局「その交換に価値があるか」が核心だ
HOL（単純型理論）の問題は依存性ではなく、論理的強度の不足だ
これは Zermelo 集合論の制限版と同等であり、現代数学を完全に形式化するには弱い
特に 圏論(category theory) のような分野のサイズ問題を扱いにくい
実際の数学者たちのスタイルとどの程度違うのか気になる
たとえば ‘inaccessible cardinal’ を追加すれば、型理論の ‘universe’ 概念に近くなる
私は形式手法(formal methods) 専攻で、依存型をかっこいいと思っていたが、実際の利用は 常に uphill battle だった
F# を使っていたとき F* 導入を試みたが、同僚たちは数学的な学習曲線を負担に感じていた
結局 数学が入ったツールはエンジニアにあまり学ばれないという皮肉な結論に達した
SMT ベースの制約解決を活用して 軽量な依存型の利用が可能だ
しかし「これが本当に正しいのか」という哲学的な問いには答えられない
数学証明とソフトウェア検証の世界はかなり異なる
結局、時間は限られている
私たちの会社 Phosphor では依存型をデータベース/グラフクエリと組み合わせて実験中だ
RDF の限界を補い、論理ベースのクエリシステムを作ることができた
実際には TypeDB(typedb.com) を使っており、MongoDB より速く、複雑なデータモデリングに有用だ
Palantir の ontology 概念にも似ている
結局、依存型の秘密は いつ使わないべきかを知ることにあるようだ
Lean や Rocq を批判するというより、状況に応じて Isabelle スタイルでアプローチすることもできるのではないかと思う
Paulson 研究チームの 形式化プロジェクト Alexandria(リンク) が印象的だ
特に 量子コンピューティングアルゴリズム形式化研究(論文リンク) が興味深い
以前は依存型が未来だと信じていたが、実際のプロジェクトでは 生産性低下が大きかった
今は明快で保守しやすい解決策をより好む
チームが理解できて拡張可能なツールなら、それが良いツールだ
私は完全な依存型よりも、その 境界にある型システムが好きだ
たとえば Purescript は Haskell より強力な row-type を標準で備え、
型レベルのリスト、文字列、正規表現までサポートしている
これを typeclass ベースの論理プログラミング方式として活用できる