型理論
型理論（かたりろん、英: Type theory）は、数理論理学の一分野であり、「型」の階層を構築し、それぞれの型に数学的（あるいはそれ以外の）実体を割り当てるものである。階型理論（かいけいりろん、英: Theory of Types）とも。ある型のオブジェクトはその前提となる型のオブジェクトから構築される。この場合の「型」とは形而上的な意味での「型」である。バートランド・ラッセルは、彼が発見したラッセルのパラドックスにより素朴集合論の問題が明らかにされたことを受けて、型理論を構築した。型理論の詳細はホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』にある。
型理論は、プログラミング言語の理論における型システムのベースにもなっている。「型システム」と「型理論」の語はほぼ同義として扱われることもあるが、ここでは、この記事では数理論理学の範囲を説明し、プログラミング言語の理論については型システムの記事で説明する。
単純階型理論（Simple Theory of Types）
ここでは、Mendelson (1997, 289-293）の体系 ST を解説する。量化の議論領域は型の階層に分けられ、個体要素（individuals）には型が割り当てられる。基盤となる論理は一階述語論理であり、量化変数の範囲は型によって限定される。ST は『数学原理』の型理論に比べて単純であり、任意の関係の議論領域は全て同じ型でなければならない。
階層中、最も低い型では、個体要素にはメンバーはなく、それらは2番目に低い型のメンバーとなる。最下層の型の個体要素は、ある集合論の原要素（Ur-elements）に対応する。それぞれの型にはより高位の型があり、ペアノの公理の後者関数（successor function）の記法にも似ている。ST では最高位の型があるかどうかは規定していない。超限数個の型があってもなんら不都合は生じない。このようにペアノの公理と似た性質であるため、各型に自然数を割り当てることが容易で、最下層の型に 0 を割り当てる。ただし、型理論そのものは自然数の定義を前提とはしていない。
ST に固有な記号として、プライム付きの変数と接中辞 ∈ がある。論理式において、プライムのない変数は全て同じ型に属し、プライム付き変数（x' )はその1つ上の型に属する。ST の原子論理式は、x=y （恒等式）か y∈x ’ という形式である。接中辞記号 ∈ は、集合の包含関係を示唆している。
以下にあげる公理に使われている変数は、全て2つの連続する型のいずれかに属する。プライムなしの変数は低位の型の変数であり、'∈' の左辺にのみ出現する（プライムつきは逆）。ST での一階述語論理では、型をまたいだ量化ができない。従って、ある型とそれに隣接する型ごとに外延性と内包性の公理を定義する必要が出てくるが、下記の外延性と内包性の公理を型をまたいで成り立つ公理型（axiom schema）とすればよい。
- 同一性: x=y ↔ ∀z’ [x∈z’ ↔ y∈z’]
- 外延性: ∀x[x∈y’ ↔ x∈z’] → y’=z’
- 内包性: ∃z’∀x[x∈z’ ↔ Φ(x)]
- 注意: 同じ型の要素を集めたものは次のレベルの型のオブジェクトを形成する。内包性は型に関する公理というだけでなく、Φ(x) の公理でもある。
- 注意: 無限性 は純粋に数学的な ST 固有の公理である。これは R が全順序関係であることを意味している。最下層の型に 0 を割り当てたとき、R の型は 3 となる。無限性 が成り立つのは R の議論領域が無限のときだけであり、結果として無限集合の存在を前提としている。関係を順序対で定義する場合、この公理の前に順序対を定義する必要が生じる。これは ST に Kuratowski の定義を導入することで実現する。ZFCのような他の集合論の無限集合の公理が何故 ST で採用されなかったのかは書籍にも書かれていない。
ST は型理論が公理的集合論と似ていることを明らかにした。さらに、ZFC などの従来の集合論よりも単純な存在論に基づく "iterative conception of set" と呼ばれる ST のより精巧な存在論がもっと簡単な公理（公理型）を構成している。型理論の出発点は集合論だが、その公理、存在論、用語は異なる。型理論には他にも New Foundations や Scott-Potter set theory がある。
歴史
型理論の他分野への影響
コンピューター
型理論の最も顕著な応用は、プログラミング言語のコンパイラでの意味論解析部での型チェックアルゴリズムの構築である。
型理論は自然言語の意味論の理論構築にもよく使われる。以下ではモンタギュー文法の内包論理（型理論と様相論理を折衷したもの）での型を例として説明する。最も基本的な型として [math]e[/math]（entity=もの）と [math]t[/math]（truth-value=真理値）があり、以下の規則を帰納的に適用して型の集合を定義する。
- [math]a[/math] と [math]b[/math] が型であるとき、[math]\langle a,b\rangle[/math] も型である。
- [math]a[/math] が型であるとき、[math]\langle s,a\rangle[/math] も型である。ここで、[math]s[/math] は型ではなく、指標（可能世界と時点の組み合わせ）である。こちらの規則は様相論理（可能世界）や時相論理（時点）も関わってくる。
[math]\langle a,b\rangle[/math] という複合型は、ある型 [math]a[/math] の要素から [math]b[/math] の要素への関数型である。つまり、[math]\langle e,t\rangle[/math] は「もの」から真理値への関数であり、いわば集合の指示関数である。[math]\langle\langle e,t\rangle,t\rangle[/math] は、指示関数の指す集合から真理値への関数であり、いわば集合の集合である。後者は自然言語で言えば、 every boy とか nobody といった表現に相当する（Montague 1973, Barwise and Cooper 1981）。
型システム
型システムの定義は様々だが、プログラミング言語理論の世界では Benjamin C. Pierce の定義が一般に受け入れられている。
- （型システムは）プログラムが計算する値の種類に従って句（phrase）を分類することで、そのプログラムがある動作をしないことを証明する扱いやすい文法的手法である。 (Pierce 2002)
換言すれば、型システムはプログラムの値を「型」と呼ばれる集合に分類し（これを「型設定」あるいは「型割り当て」と呼ぶ）、特定のプログラムの動作が不正であることを示す。例えば、"hello" という値を文字列型、5 という値を整数型としたとき、プログラマに "hello" と 5 を加算できないといった制限を課すのである。このような型システムでは、次のプログラム
"hello" + 5
は不正である。もちろん、文字列と整数を加算することを許す型システムもありうる。
型システムの設計と実装は、プログラミング言語そのものと同じ程度に広がりを持った話題である。実際、プログラミング言語の最大の基盤は型システムであるとも言われ、「型システムを正しく設計すれば、言語は自分自身で設計される」と言われている。
関連項目
参考文献
- テンプレート:Scholarpedia
- Per Martin-Löf (1980), Intuitionistic Type Theory
- Bengt Nordström,Kent Petersson,Jan M. Smith (1990), Programming in Martin-Löf's Type Theory
- 『岩波数学辞典 第4版』 日本数学会編、岩波書店、2007年。ISBN 978-4-00-080309-0。