← 戻る ライブラリ › 数学の基礎 › 計算可能性と証明 数学の基礎
型理論 すべての項が型を持つ、数学と計算のための基礎理論で、証明支援系に用いられる。
直観 すべての値にはラベルがある ほとんどのプログラミング言語では、3 3 3 型理論 はこの日常的な発想を数学全体の基礎へと変える:集合と所属関係(x ∈ A x \in A x ∈ A 項と型 (t : A t : A t : A t t t A A A 型 が数学的な命題 を符号化でき、その型の項 が証明 になる——プログラムと証明が同じ種類の対象になるのである。
型付け導出を木として表す:各頂点は判断 Γ ⊢ t : A \Gamma \vdash t : A Γ ⊢ t : A 大学 単純型付きラムダ計算 定義: 型判断
型判断 Γ ⊢ t : A \Gamma \vdash t : A Γ ⊢ t : A Γ \Gamma Γ x 1 : A 1 , … , x n : A n x_1:A_1,\dots,x_n:A_n x 1 : A 1 , … , x n : A n t t t A A A 抽象 λ x : A . t \lambda x{:}A.\,t λ x : A . t x : A x:A x : A t t t B B B A → B A\to B A → B 適用 f u f\,u f u f : A → B f:A\to B f : A → B u : A u:A u : A B B B
Γ , x : A ⊢ t : B Γ ⊢ λ x : A . t : A → B Γ ⊢ f : A → B Γ ⊢ u : A Γ ⊢ f u : B \dfrac{\Gamma, x{:}A \vdash t : B}{\Gamma \vdash \lambda x{:}A.\,t : A\to B} \qquad \dfrac{\Gamma \vdash f : A\to B \quad \Gamma \vdash u : A}{\Gamma \vdash f\,u : B} Γ ⊢ λ x : A . t : A → B Γ , x : A ⊢ t : B Γ ⊢ f u : B Γ ⊢ f : A → B Γ ⊢ u : A マルティン゠レーフの依存型理論はこれをさらに一般化する:関数の結果 の型が引数の値 に依存しうる。**Π \Pi Π ∏ x : A B ( x ) \prod_{x:A} B(x) ∏ x : A B ( x ) x : A x:A x : A B ( x ) B(x) B ( x ) B B B x x x A → B A\to B A → B Σ \Sigma Σ ∑ x : A B ( x ) \sum_{x:A} B(x) ∑ x : A B ( x ) a : A a:A a : A b : B ( a ) b:B(a) b : B ( a ) ⟨ a , b ⟩ \langle a,b\rangle ⟨ a , b ⟩ 第2成分の型 が第1成分に依存する対である;B B B x x x A × B A\times B A × B
∏ x : A B ( x ) , ∑ x : A B ( x ) \prod_{x:A} B(x), \qquad \sum_{x:A} B(x) x : A ∏ B ( x ) , x : A ∑ B ( x ) 依存型とそのCurry–Howard的解釈 型構成子 非依存な特殊な場合 Curry–Howard的解釈 ∏ x : A B ( x ) \prod_{x:A} B(x) ∏ x : A B ( x ) A → B A\to B A → B B B B ∀ x : A , B ( x ) \forall x{:}A,\ B(x) ∀ x : A , B ( x ) ∑ x : A B ( x ) \sum_{x:A} B(x) ∑ x : A B ( x ) A × B A\times B A × B B B B ∃ x : A , B ( x ) \exists x{:}A,\ B(x) ∃ x : A , B ( x ) univalence: ( A ≃ B ) ≃ ( A = U B ) (A\simeq B) \simeq (A =_{\mathcal U} B) ( A ≃ B ) ≃ ( A = U B ) — 同値な型は同一視される
単純型付きラムダ計算において Γ ⊢ t : A \Gamma \vdash t : A Γ ⊢ t : A t t t 強正規化可能 である:t t t β \beta β
なぜ正しいのか? これが、単純型付きラムダ計算が関数適用や再帰的な入れ子を持つにもかかわらずチューリング完全ではない 理由である——型付けされた項は決して無限に走ることができず、これこそがこの断片における型検査器が常に停止することを保証する。
証明 (タイトの被還元性の方法。)型の構造に関する帰納法により、各型 A A A R E D A \mathrm{RED}_A RED A o o o R E D o \mathrm{RED}_o RED o S N SN S N R E D A → B = { t : for every u ∈ R E D A , t u ∈ R E D B } \mathrm{RED}_{A\to B} = \{t : \text{for every } u \in \mathrm{RED}_A,\ t\,u \in \mathrm{RED}_B\} RED A → B = { t : for every u ∈ RED A , t u ∈ RED B }
まず A A A R E D A \mathrm{RED}_A RED A R E D A \mathrm{RED}_A RED A β \beta β t ∈ R E D A t\in\mathrm{RED}_A t ∈ RED A t → t ′ t\to t' t → t ′ t ′ ∈ R E D A t'\in\mathrm{RED}_A t ′ ∈ RED A R E D A \mathrm{RED}_A RED A R E D A \mathrm{RED}_A RED A S N SN S N R E D A → B \mathrm{RED}_{A\to B} RED A → B A A A B B B
次に、自由変数に被還元項を代入したとき、あらゆる型付けされた項が被還元であることを示す:Γ ⊢ t : A \Gamma \vdash t:A Γ ⊢ t : A σ \sigma σ Γ \Gamma Γ x x x σ ( x ) ∈ R E D Γ ( x ) \sigma(x)\in\mathrm{RED}_{\Gamma(x)} σ ( x ) ∈ RED Γ ( x ) t σ ∈ R E D A t\sigma \in \mathrm{RED}_A t σ ∈ RED A R E D A → B \mathrm{RED}_{A\to B} RED A → B ( λ x . t ) σ (\lambda x.\,t)\sigma ( λ x . t ) σ u ∈ R E D A u\in\mathrm{RED}_A u ∈ RED A β \beta β t ( σ , x : = u ) t(\sigma,x{:=}u) t ( σ , x := u ) R E D B \mathrm{RED}_B RED B ( λ x . t ) σ u (\lambda x.\,t)\sigma\,u ( λ x . t ) σ u R E D B \mathrm{RED}_B RED B ( λ x . t ) σ ∈ R E D A → B (\lambda x.\,t)\sigma \in \mathrm{RED}_{A\to B} ( λ x . t ) σ ∈ RED A → B
最後に、これを恒等代入に適用する:各変数 x : A x{:}A x : A R E D A \mathrm{RED}_A RED A Γ ⊢ t : A \Gamma \vdash t:A Γ ⊢ t : A σ \sigma σ x x x t = t σ ∈ R E D A t = t\sigma \in \mathrm{RED}_A t = t σ ∈ RED A R E D A ⊆ S N \mathrm{RED}_A \subseteq SN RED A ⊆ S N t ∈ S N t \in SN t ∈ S N ■ \blacksquare ■
発展 Curry–Howard対応 A → B A\to B A → B A A A B B B A × B A\times B A × B A A A B B B 証明 は対応する型の型付けされたプログラム になる——これが命題は型である、証明はプログラムである という対応である。証明の検査は項の型検査に帰着し、証明の構成は正しい型のプログラムを書くことに帰着する。
原子、∧ \wedge ∧ → \to → φ \varphi φ ∧ \wedge ∧ × \times × → \to → → \to → A φ A_\varphi A φ φ \varphi φ A φ A_\varphi A φ 住人を持つ こと(閉じた項 t t t ⊢ t : A φ \vdash t : A_\varphi ⊢ t : A φ
なぜ正しいのか? これは「証明支援系は単なる型検査器である」という言葉の背後にある正確な主張である:Coq、Agda、Leanは、対応する型の項を受理するときにちょうど、定理の機械検査済み証明を受理する。そして型検査は(一般の定理証明とは異なり)小さく高速で機械的、かつ極めて信頼できるアルゴリズムである。
証明 (証明はプログラムになる。)⊢ φ \vdash \varphi ⊢ φ → \to → ψ \psi ψ χ \chi χ φ = ψ → χ \varphi=\psi\to\chi φ = ψ → χ x : A ψ ⊢ t : A χ x{:}A_\psi \vdash t : A_\chi x : A ψ ⊢ t : A χ t t t x x x λ x : A ψ . t \lambda x{:}A_\psi.\,t λ x : A ψ . t A ψ → A χ = A φ A_\psi\to A_\chi=A_\varphi A ψ → A χ = A φ ψ → χ \psi\to\chi ψ → χ ψ \psi ψ → \to → t 1 : A ψ → A χ t_1 : A_\psi\to A_\chi t 1 : A ψ → A χ t 2 : A ψ t_2 : A_\psi t 2 : A ψ t 1 t 2 : A χ t_1\,t_2 : A_\chi t 1 t 2 : A χ ∧ \wedge ∧ ∧ \wedge ∧ ⟨ t 1 , t 2 ⟩ \langle t_1,t_2\rangle ⟨ t 1 , t 2 ⟩ A φ A_\varphi A φ
(プログラムは証明になる。)逆に、型付け導出 ⊢ t : A \vdash t : A ⊢ t : A → \to → → \to → ∧ \wedge ∧ ∧ \wedge ∧ φ \varphi φ A = A φ A=A_\varphi A = A φ
2つの翻訳(証明 → \to → → \to → φ \varphi φ A φ A_\varphi A φ ■ \blacksquare ■
大学 実世界での応用と具体例 豊かな型システムは、プログラムが実行される前にバグの一群全体を捕らえる:Rustの所有権型はコンパイル時に解放後使用やデータ競合を防ぎ、依存型付き言語は「このリストはちょうど n n n 表現不可能 にする。最も深い応用は証明支援系 そのものの内部にある:Coq、Agda、Leanは、項の型検査だけを行う小さく注意深く監査されたカーネルを持つ——Curry–Howard対応により、定理の型の項を受理することは機械検査済みの証明を受理することそのもの であるため、Feit–Thompsonの定理や四色定理ほどの規模の数学的結果を信頼することは、証明項を構築した(はるかに大きく監査がはるかに難しい)タクティクではなく、わずか数百行の型検査コードを信頼することに帰着する。
例: 通常の関数型では表現できない Π \Pi Π
V e c A n \mathrm{Vec}\,A\,n Vec A n A A A n n n ∏ n : N ( V e c A n → V e c A n ) \prod_{n:\mathbb N} (\mathrm{Vec}\,A\,n \to \mathrm{Vec}\,A\,n) ∏ n : N ( Vec A n → Vec A n ) n n n n n n Π \Pi Π
解答 項 λ n : N . λ v : V e c A n . v \lambda n{:}\mathbb N.\,\lambda v{:}\mathrm{Vec}\,A\,n.\,v λn : N . λ v : Vec A n . v n n n n n n v v v v : V e c A n v : \mathrm{Vec}\,A\,n v : Vec A n n n n V e c A n \mathrm{Vec}\,A\,n Vec A n
これが通常の関数型ではなく Π \Pi Π 第2引数の型 (V e c A n \mathrm{Vec}\,A\,n Vec A n n n n 値 に言及しているからである。単純型付きラムダ計算では、関数の引数の型と結果の型は一度きり固定される——A , B A,B A , B A A A A → B A\to B A → B n n n → \to → n n n V e c A n \mathrm{Vec}\,A\,n Vec A n V e c \mathrm{Vec} Vec
具体的に、通常の関数型でこれを書こうとすると、せいぜい1つの固定されたプレースホルダー長についての N → ( V e c A ? → V e c A ? ) \mathbb N \to (\mathrm{Vec}\,A\,? \to \mathrm{Vec}\,A\,?) N → ( Vec A ? → Vec A ?) Π \Pi Π ∏ n : N ( ⋯ ) \prod_{n:\mathbb N}(\cdots) ∏ n : N ( ⋯ ) n n n
例: 関数合成に対するCurry–Howard
論理式 ( A → B ) → ( ( B → C ) → ( A → C ) ) (A\to B)\to((B\to C)\to(A\to C)) ( A → B ) → (( B → C ) → ( A → C )) λ \lambda λ
解答 その項は t = λ f : A → B . λ g : B → C . λ x : A . g ( f x ) t = \lambda f{:}A\to B.\,\lambda g{:}B\to C.\,\lambda x{:}A.\,g\,(f\,x) t = λ f : A → B . λ g : B → C . λ x : A . g ( f x ) x x x g ∘ f g\circ f g ∘ f
内側から外側へ型を導出する。文脈 f : A → B , g : B → C , x : A f{:}A\to B,\,g{:}B\to C,\,x{:}A f : A → B , g : B → C , x : A f : A → B f:A\to B f : A → B x : A x:A x : A f x : B f\,x:B f x : B g : B → C g:B\to C g : B → C f x : B f\,x:B f x : B g ( f x ) : C g\,(f\,x):C g ( f x ) : C
次に内側から外側へ抽象を解消する。λ x : A . g ( f x ) \lambda x{:}A.\,g\,(f\,x) λ x : A . g ( f x ) f : A → B , g : B → C f{:}A\to B,\,g{:}B\to C f : A → B , g : B → C A → C A\to C A → C λ g : B → C . ( ⋯ ) \lambda g{:}B\to C.\,(\cdots) λ g : B → C . ( ⋯ ) f : A → B f{:}A\to B f : A → B ( B → C ) → ( A → C ) (B\to C)\to(A\to C) ( B → C ) → ( A → C ) λ f : A → B . ( ⋯ ) \lambda f{:}A\to B.\,(\cdots) λ f : A → B . ( ⋯ ) ( A → B ) → ( ( B → C ) → ( A → C ) ) (A\to B)\to((B\to C)\to(A\to C)) ( A → B ) → (( B → C ) → ( A → C ))
したがって ⊢ t : ( A → B ) → ( ( B → C ) → ( A → C ) ) \vdash t : (A\to B)\to((B\to C)\to(A\to C)) ⊢ t : ( A → B ) → (( B → C ) → ( A → C )) t t t A A A B B B B B B C C C A A A C C C
よくある誤り. Π x : A B ( x ) \Pi_{x:A}B(x) Π x : A B ( x ) Σ x : A B ( x ) \Sigma_{x:A}B(x) Σ x : A B ( x ) 型形成操作 であり、それらの非依存な特殊な場合(Π → \Pi\to Π → Σ → \Sigma\to Σ → ( A ≃ B ) ≃ ( A = U B ) (A\simeq B)\simeq(A=_{\mathcal U}B) ( A ≃ B ) ≃ ( A = U B ) 命題的 等式 = U =_{\mathcal U} = U 定義上の (判断的な)等式についてではない——univalenceは呼び出す 必要があり、型付け規則だけから自動的に得られるものではない。歴史的ノート
アロンゾ・チャーチは1940年、型なしラムダ計算のパラドックスを避けるために単純型を導入した。クルト・ゲーデルの1958年の「Dialectica解釈」は、原始再帰関数汎関数の型付き計算——型付き証明解釈の直接の祖先——を用いて、算術の構成的無矛盾性証明を与えた。1972年、ペール・マルティン゠レーフは、Π \Pi Π Σ \Sigma Σ
クルト・ゲーデル
研究 現在の研究 研究の最前線 2026年時点
ホモトピー型理論とVoevodskyのUnivalent Foundationsプログラムは、ZFC集合論を(まだ置き換えるのではなく)並走する数学の候補基礎として発展し続けており、キュービカル型理論 (おおよそ2015年以降)は、区間型から直接型の等式を構築することで、univalence公理に真の計算的内容を与えている——長年の未解決問題だった——そしてこの計算的な扱いは2026年現在もなお洗練され、より豊かな型構成子へと拡張され続けている。大規模な形式化の取り組みは、作業用数学インフラとしての型理論の力を実証している:Leanベースの`mathlib`ライブラリは形式化された数学の最大級の集積の一つへと成長し、Peter ScholzeとDustin Clausenによる2020〜2022年の「Liquid Tensor Experiment」はLeanを用いて凝縮数学の難しい定理を形式的に検証し、(Kevin Buzzardが主導するものを含む)フェルマーの最終定理の完全な形式化を目指すコミュニティの取り組みは2020年代半ば現在も活発である。別途、高次帰納型と総合的ホモトピー論(型理論の内部で球面のホモトピー群を直接計算する)に関する研究や、決定可能な型検査を犠牲にすることなく通常の数学的実践をより多く支えるよう依存型理論を強化する研究も続いている。
単純型付きラムダ計算において、f : A → B f : A \to B f : A → B a : A a : A a : A f a f\,a f a
A A A B B B A → B A \to B A → B A × B A \times B A × B Coq、Agda、Leanのような証明支援系は、なぜ数千行にわたる機械検査済みの証明を信頼できるのか?
証明の検査は、小さく信頼できるカーネルによって行われる、定理の型に対する項の型検査に帰着するから 証明はその都度AIモデルによって再導出されるから 証明は多くの異なる証明器の多数決によって検査されるから 定理の主張は証明なしに単に仮定されるから
B ( x ) B(x) B ( x ) x x x ∏ x : A B ( x ) \prod_{x:A} B(x) ∏ x : A B ( x )
A × B A \times B A × B A → B A \to B A → B A A A B B B univalence公理 ( A ≃ B ) ≃ ( A = U B ) (A\simeq B) \simeq (A =_{\mathcal U} B) ( A ≃ B ) ≃ ( A = U B )
同値な(同型な)型は命題的に等しいものとして扱える すべての型は有限である すべての関数は定数時間で計算可能である 型検査は決定不可能である