summary:
型理論は,以下のデータと規則から構成される：
このとき,型付け判断[typing judgment]は次のように記述される：\[\Gamma \vdash t : A\]
これは,文脈[前提] $\Gamma$ の下で,項 $t$ は型 $A$ をもつ,という意味である.
バートランド・ラッセル[Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS,1872-05-18/1970-02-02]は,自己言及的な集合の存在を問題にし,「自分自身を含まない集合」のような集合が存在する場合,矛盾が生じることを示した[ラッセルの逆説,Russell's Paradox].この問題提起は,従来の無限集合に関する扱い方に重大な問題を突きつけ,集合論を基にした数学的理論における体系的な問題点を明らかにするものであった.
ラッセルはこの矛盾を回避するために,タイプ理論[型論,Type Theory]を提案.タイプ理論では,集合が自己参照することを避けるため,集合[または式]を型に分類し,型に基づいて操作を制限する方法を採用した.このアイデアは,後に型理論として発展し,パトリック・マーティン＝ロフやカリー＝ハワード対応のような現代の型理論に影響を与えるに至る.
型理論のルーツの一部は,アロンゾ・チャーチによる$\lambda$計算[$\lambda$-calculus]に遡る.$\lambda$計算は1930年代にチャーチによって導入され,計算の理論的基礎を築くものとして重要な役割を果たした.$\lambda$計算は,関数の定義や適用を形式的に記述する方法であり,現在のプログラム言語の構造に深い影響を与えている.
$\lambda$計算は,数学的な計算を記述するための抽象的な記法として最初に提案された.チャーチは,関数計算を行うための形式的な基盤として$\lambda$計算を使用し,その後,型理論への道を開いた.
型理論の最も初期の形態は,型付き$\lambda$計算[Simply Typed $\lambda$-Calculus, STLC]として現れた.型付き$\lambda$計算は,$\lambda$計算に型の概念を追加することにより,計算の安全性と意味論をより明確にするための試みであった.このように,$\lambda$計算に型を付与するアイデアは,計算を形式的に厳密に扱うための重要なステップであったと言える.
型理論の発展において,重要なもう一人の人物としては,パトリック・マーティン＝ロフを挙げることができよう.1970年代にマーティン＝ロフは,依存型[Dependent Types]という概念を導入した.依存型理論は,型が値に依存することを許すものであり,より強力で柔軟な型システムを提供した.これにより,型理論はプログラムにおける証明と計算を統一するツールとして大きな進展を見せることとなる.
マーティン＝ロフは,型理論を数学の証明とプログラムの構築を一体化するための手段として発展させたが,特にプログラムの正当性を証明する手段としての役割を強調したことで知られる.彼の貢献は,構成的意味論[Constructive Semantics]を基盤にした証明支援系の構築に影響を与えた.
その後,ホモトピー型理論[Homotopy Type Theory, HoTT]という新しい分野が型理論に登場.これは,圏論とトポス理論の考え方を型理論に統合したものであり,タイプの性質をトポロジカルな視点から捉えるものである.
型理論にはいくつかの体系がある.
また,型理論は以下の分野で応用されている.
文脈は,変数とその型の列である.\[\Gamma = (x_1 : A_1, x_2 : A_2, \dots, x_n : A_n)\]
型理論における代表的な型構成子[型形成ルール]には以下のものがある.
型理論の特徴的な性質の一つは,Curry-Howard対応である.これは,命題,証明,プログラムが次のように対応するというものである.
Mathematics is the language with which God has written the universe.