前回は型理論・圏論・論理学の各分野について触れながら、型理論の歴史まで紹介した。
今回はトライアングルの辺の部分、分野同士の対応について説明する。
型理論 ↔ 論理学
1969年にカリー＝ハワード対応の現代形が与えられてから、1970年代に多相型・カインド・依存型など「理論先行」の型が次々と定式化された。1988年に全部乗せの Calculus of Constructions (CoC) が発表。最終的にラムダキューブ（1991年）としてまとめられる。
- 単純型 ↔ 1階命題論理
- 多相型 ↔ 2階命題論理
- 多相型+カインド ↔ 高階命題論理
- 依存型 ↔ 1階述語論理
- CoC ↔ 高階述語論理
※論理の側は全て直観主義論理
これらの型について、より正確には、カリー＝ハワード対応を通した「論理学先行」と言うべきかもしれない。
たとえば多相型は、ジラールが二階論理の証明体系の一部として System F を発見した（1972年）のが最初である。これとは独立に、レイノルズは1974年、計算機科学の側で多相型を発見した*1。
また依存型は、Martin-Löf の1972-75年の仕事が元になっているが、本来は構成的数学の基礎付けを直観主義型理論として行おう、という問題意識であった。
このように、型理論は論理学から多くを持ち帰っている。また、論理学が型理論から得た成果もある。片方で重要なものがもう片方で大した意味を持たず、失敗することも多いが。
カリー＝ハワード対応の教科書として次を挙げておく。
- Jean‑Yves Girard, Yves Lafont, Paul Taylor, Proofs and Types, Cambridge University Press, 1989 (pdf)
- Morten Heine Sørensen, Pawel Urzyczyn, Lectures on the Curry‑Howard Isomorphism, Springer, 2006 (pdf)
多相型・依存型と対応する論理体系、あるいは線形論理や古典論理と対応する型体系について解説している。
定理証明支援系
型理論と論理学のつながりから生まれた応用の一つが、証明の正当性をプログラミングでチェックする証明支援系である。
ラムダキューブの頂点にある CoC にさらに帰納型を加えた Calculus of Inductive Constructions (CIC) が、Coq や Lean のおおよそのベースとして使われている。2020年代に入ってからは特に Lean が流行っており、AIと相性が良いので今後も伸びそうな感じがする。
- 井上亜星 『ゼロから始めるLean言語入門 - 手を動かして学ぶ形式数学ライブラリ開発』ラムダノート、2025年
- イントロダクション - Theorem Proving in Lean 4 日本語訳
- Adam Chlipala, Certified Programming with Dependent Types, The MIT Press, 2013 (pdf)
- Yves Bertot, Pierre Castéran, Interactive Theorem Proving and Program Development, Springer, 2004
- Rob Nederpelt, Herman Geuvers, Type Theory and Formal Proof, Cambridge University Press, 2014
論理学 ↔ 圏論
いわゆる圏論的論理学。主にトポスという圏により、圏の言葉で論理学を行う。
トポスには、大きく分けてグロタンディーク・トポスと初等トポス（Elementary Topos）の2つの流れがある。まず前者について説明しよう。
グロタンディークは1950-60年代、ヴェイユ予想の解決に向けて代数幾何学に様々な変革をもたらした。代数幾何の良いところは、代数でいろんなことがガッチリ決まっており、計算がしやすいことである。悪いところは、幾何をするにはあまりに柔軟性がないことである。そのためグロタンディークは、「代数的に取り扱える十分柔軟な位相」を求めて極度に抽象化された大道具をいくつも開発した。スキームはその一つである。しかしこれも、ヴェイユ予想の解決に必要だと思われていた幾何的不変量（ヴェイユ・コホモロジー）を得るにはまだ不足していた。
そこでグロタンディークは、「位相空間の代わりに、圏と被覆のペア をとり、その上の層（sheaf）の圏
において幾何的操作を行う」ことにしたのだ。
がグロタンディーク・トポスと呼ばれる対象である。このくらいすると、圏の言葉で幾何が行えるようになる。実際、トポス概念に基づいた精密な位相（エタールサイト）と精密な幾何的不変量（エタールコホモロジー）によって、最終的にドリーニュがヴェイユ予想を解決した（1974年）*2。
もう1つのトポス、初等トポスについて。
グロタンディーク・トポスを傍目に見ていたローヴィアとティアニーは、トポスが「有限完備・カルテシアン閉・部分対象分類子」という比較的簡単な圏論的公理で特徴づけられることに気づく。彼らはそれを、初等トポスと名付けた（1968-69年）。
また、初等トポスは幾何的操作や集合論的操作だけでなく、論理学的な操作も行えることが判明する。こうして、初等トポスによって論理学を書き直す圏論的論理学のプロジェクトが始動した。
参考資料：
初等トポスの幾何的側面は、ひとまず忘れて構わない。初等トポスの公理からすぐ明らかになるわけでもないので。
圏論的論理学の文献を紹介しよう。
次は貴重な日本語の教科書だが、古かったり用語法が変だったりするのであまりお勧めはしない。
- 竹内外史『層・圏・トポス』日本評論社、1978年
- 清水義夫『圏論による論理学：高階論理とトポス』東京大学出版会、2007年
- 清水義夫『記号論理学講義：基礎理論 束論と圏論 知識論』東京大学出版会、2013年
Web上の日本語資料は充実している。
- 荒武永史『トポス理論と圏論的論理学への誘い』2019年 (pdf)
- 荒武永史『圏論的論理学』Logic Winter School 2023 (web)
- 上村太一『トポスと高階論理』2018年 (pdf)
- 古賀実／才川隆文「トポスの内部言語について」『The Dark Side of Forcing』2016年、pp.13- (pdf)
ちゃんと勉強したいなら、次から始めるのが良いだろう。
本当に丁寧なので初心者でも安心。ただ簡単な割に厚いので、モチベを保ちにくいし、重要なところを掴みにくいという問題はある。たとえば、理論の圏とモデルとなる圏の間に構築できる随伴関手など。
次は有名なトポスの専門書。それぞれ『SGL』『Elephant』と呼ばれている。
- Saunders MacLane, Ieke Moerdijk, Sheaves In Geometry And Logic: A First Introduction To Topos Theory, Springer, 1994
- Peter Johnstone, Sketches of Elephant: A Topos Theory Compendium (Vol.1/2), Oxford University Press, 2002
これらを読むには、代数幾何学や代数トポロジー（分類空間など）や数理論理学（強制法など）にある程度馴染んでおく必要がある。
型理論 ↔ 圏論
前回、「型付きラムダ計算には3つの意味論（操作的、表示的、公理的）がある」と述べた。圏論的意味論は、計算の不変量を与える表示的意味論の一種と思える。この分野は、カリー＝ハワード対応や圏論的論理学によって、型理論・圏論・論理学の間を自由に行き来する。
歴史を整理しておこう。単純型付きラムダ計算とカルテシアン閉圏の対応は、おおよそ1970年代後半に定式化されたようである。依存型（Martin-Löf 型理論）の局所カルテシアン閉圏によるモデル化は、R. A. G. Seely （1984年）による。多相型+カインドに関しては、Seely（1987年）が「PL圏」なるものでまずモデル化し、その後ファイブレーションで再定式化された。
型システムの圏論的意味論に関する参考書。
- Joachim Lambek, P. J. Scott, Introduction to Higher‑Order Categorical Logic, Cambridge University Press, 1986
- Roy L. Crole , Categories for Types, Cambridge University Press, 1994
- Bart Jacobs , Categorical Logic and Type Theory, Elsevier Science, 1999
- relationship between type theory and category theory - nLab
［Lambek, Scott］は型理論・圏論・論理学をかなり均等に扱うことが特徴的である。［Crole］は多相型+カインドまでを扱う。［Jacobs］は論理学的視点も盛り込みつつ、CoC まで扱った浩瀚な辞書である。
その他日本語資料：
ホモトピー型理論（Homotopy Type Theory）
代数トポロジーや無限圏をベースとして型理論を展開してみよう、というのがホモトピー型理論の試みである。
そもそもの問題意識は、Martin-Löf 型理論（MLTT）にあった。
- 龍田真『型理論』近代科学社、1992年
- Bengt Nordström, Kent Petersson, Jan M. Smith, Programming in Martin‑Löf’s Type Theory: An Introduction, Oxford University Press, 1990 (pdf)
これまでちゃんと説明してこなかったが、 Martin-Löf 型理論と（依存型付きの）ラムダ計算は証明論的に異なる。型付きラムダ計算はβη変換で同値性を処理する。一方Martin-Löf 型理論は、 （型
に属する
と
は等しい）という命題に対して、同一型
という型を付けることができる。さらに
の証明同士の関係（証明の証明）を型
として論じたり、証明の証明の証明を型として扱うことができる。問題は、これらの型をどう圏論的に解釈するかである。
1990年代後半、同一型を groupoid（射がすべて同型射である圏）で意味付ける研究が現れた（Hofmann–Streicher, 1998）。これで証明の証明までは扱えるようになったが、それより高次の関係がまだうまくいかない。
いっそ無限圏（∞-groupoid） にしてしまおう、∞-groupoid なら代数トポロジーの連続変形の理論＝「ホモトピー」だ、という方向に研究が進んでいった（Awodey/Warren, 2009）。この描像では「型＝空間、項＝点、同一性証明＝パス」となる。
∞-groupoid からホモトピーに移るのは、代数トポロジーの血を血で洗う抽象化の歴史が背景としてある*3。代数トポロジーには球面のホモトピー群など、定義は簡単だが計算が異様に難しい幾何的不変量がいくつも存在する。柔らかい幾何を代数で捉える無理を押し通すため、代数トポロジーでは代数的な大道具を積み重ねてきた。代数で幾何を無理やり行おうとする代数幾何とは真逆の方向性で、結果的に似たようなことをしている。
ホモトピー型理論は、数学の側からすると、ホモトピー論や高次圏・無限圏論を最初から扱える内部言語として期待されている。ヴォヴォドスキーは Univalent Foundations を唱え、数学の側からホモトピー型理論の追求を始めた。そのきっかけの1つは、フィールズ賞受賞のもととなった論文に関して、高次圏周りで修正のかなり難しい誤りが見つかったことだという。高次圏・無限圏は概念的にも大変だが、技術的にもチェックすべきことが山ほどある。ホモトピー的な操作に向いた言語を作り、コンピュータで形式的に計算したい、というモチベーションがあった。
- Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge University Press, 2022
- Univalent Foundations Project, Homotopy Type Theory: Univalent Foundations of Mathematics, 2013 (pdf)
前提となる無限圏の参考書も挙げておく。
- Emily Riehl and Dominic Verity, Elements of ∞-Category Theory, Cambridge University Press, 2022 (pdf)
- Jacob Lurie, Higher Topos Theory, 2009 (pdf)
ホモトピー型理論の現状を整理すると、界隈内部では一定の成果がありつつも、界隈外で使われるような分かりやすい結果は出ていないと思う。やっぱり無限圏は難しい。
1つの方向性として注目されているのは、ホモトピー型理論を構成的に行い、計算機との相性を良くするCubical Type Theoryである。
実装面では、Coq の HoTT ライブラリ（univalence は公理として仮定）や Cubical Agda などで、ホモトピー型理論が定理証明支援系に組み込まれている。
意外なところでいくと、バージョン管理システムを抽象化したパッチ理論を、ホモトピー型理論で拡張する話がある。
- 佐藤善紀／三好博之『Homotopy Type Theory によるパッチ理論の拡張』日本ソフトウェア科学会第32回大会(2015年度)講演論文集 (pdf)
その他日本語資料：
- 上村太一『ホモトピー型理論』2023年 (pdf)
- 『Coqと少しの圏論が分かる人向けのhomotopy type theory(その1)』
おわりに
思ったより数学寄りのテキストになってしまった。
数学寄りにしても計算機科学寄りにしても、私より書くのに向いた人間がいただろうと思う。自分の勉強が目的だから構わないが。誤りや不足等あれば、ぜひご指摘いただきたい。
以下、書き終えた感想をメモしておく。
・計算機科学としての型理論
HoTTまで紹介しておいてなんだが、ここまで抽象化された（数理論理学寄りの）型理論に対して、さほど興味がないことに気づいた。どちらかといえば、言語設計やコンパイラの実装にあたって必要な型関連の知見を得たい。まだ紹介していない資料だと、次あたりだろうか。
- Typechecker Zoo
- Ranjit Jhala, Niki Vazou, Refinement Types: A Tutorial, 2020 (arxiv)
Typechecker Zooは良さそうに見える。←読んでいるが、現状テキストとしてはちょっと不親切で、サンプルコードをガン見したり理論部分は別途調べたりする必要がある。
・構成的数学とプログラミング
型理論・圏論・論理学のトライアングルを追う中で、裏で流れ続けていたのは構成的数学のテーマだった。作業的には「排中律や選択公理は対象を構成できなくなるので止めよう」といった感じだが、思想的にはもっと深いものがある。
- Paul Taylor, Practical Foudation of Mathematics, Cambridge University Press, 1999
- 石原哉『構成的数学とその動向』2007年 (pdf)
（変な拡張をしていない）型付きラムダ計算の良いところは、計算の停止を保証することである。安全なプログラミングの土台になるという意味でも、現実的に望ましい性質だ。
しかし裏返せば、停止するもの／構成できるものしか計算／演繹できないという限界がある。
私にとって数学の一番面白いところは、超越や無限を探り当て、その一部をかすめ取るところである*4。数理論理学の中だと集合論が一番好きだし、証明論（構文論）が一番ピンとこない。
今回扱った内容に関しても、根本的なモチベが分かっていない感じがする。
・書き換えシステム
翻訳者は、創作する詩人と異なり、言語そのものを救済しなければならない
（ベンヤミン「翻訳者の使命」1921-23年、摘要）*5
型理論・圏論・論理学の3つの岸辺があり、それらの間に橋をかける方法を本記事では扱ってきた。しかし、こうした翻訳行為によって、私たちの知識はどれほど増えたのだろうか。
尺度の1つは、翻訳の導入によりどれほど古い問題を解決できるようになったかである。もう1つは、どれほど問題を──新しくて良い問題を──作れるようになったか、である。
型・圏・論理の対応は、1980 年代にはかなり見通しが立ち、今となっては当たり前のように扱われることが多い。そのせいもあって、私自身はまだこの翻訳行為がどこまで本質的なものだったのか、判断しきれていない*6。
あるいは、私たちの翻訳行為が創作行為でなかったとすれば、何を救済したかが問われるべきだろう。
あなたは何を救済しましたか。
*1:正確に言うと、ここで「多相型」と呼んでいるのは「パラメトリック多相」のことである。具体的にはC++のテンプレートやJavaのジェネリクスに相当する。これとは別に「アドホック多相」（1967年）という概念も存在し、関数や演算子のオーバーロード（同じ名前で異なる型の引数に対し異なるふるまいができる）に相当する。なおRustのトレイト制約やHaskellの型クラスは制約付き多相だと前回述べたが、もっと分解すると「アドホック多相 + 能力システム」らしい。
*2:なお、グロタンディークはモチーフという更なる大道具でヴェイユ予想が解かれるべきだと考えていたため、モチーフを回避したドリーニュの証明には激怒したという。モチーフは今なお代数幾何の中心課題の一つである。
*3:さらに言うなら、「∞-groupoid = ホモトピー」という描像自体は、グロタンディークがホモトピー仮説として唱えたものである。
*5:正確には中島隆博『ヒューマニティーズ 哲学』（岩波書店、2009年、p.43）からの引用。
*6:一見魅力的だが、（今の人類にとって）無意味な対応関係というものは、存在する。「結び目と素数（knots and primes）」に関するメモ - 古い土地
