型理論

型理論（かたりろん、）とは、プログラミング・数学・言語学等に現れる型の概念及びそれらが成す型システムを研究対象とする数学・計算機科学の分野である。特定の型システムのことを型理論と呼ぶこともある。集合論の代替となる数学の基礎として役立てられる型理論（型システム）も存在する。そのような例としてアロンゾ・チャーチの型付きラムダ計算やマルティン・レーフの直観主義型理論が有名である。
20世紀初頭にバートランド・ラッセルが発見した、ラッセルのパラドックスによるフレーゲの素朴集合論の欠陥を説明する中で提起されたtheories of typeが型理論の起源であり、後年にAxiom of reducibilityが付随された型理論は、ホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』に収録されている。
単純階型理論（Simple Theory of Types）.
ここでは、Mendelson (1997, 289-293）の体系 ST を解説する。量化の議論領域は型の階層に分けられ、個体要素（individuals）には型が割り当てられる。基盤となる論理は一階述語論理であり、量化変数の範囲は型によって限定される。ST は『数学原理』の型理論に比べて単純であり、任意の関係の議論領域は全て同じ型でなければならない。
階層中、最も低い型では、個体要素にはメンバーはなく、それらは2番目に低い型のメンバーとなる。最下層の型の個体要素は、ある集合論の原要素 (Ur-elements) に対応する。それぞれの型にはより高位の型があり、ペアノの公理の後者関数 (successor function) の記法にも似ている。ST では、最高位の型があるかどうかは規定していない。超限数個の型があってもなんら不都合は生じない。このようにペアノの公理と似た性質であるため、各型に自然数を割り当てることが容易で、最下層の型に 0 を割り当てる。ただし、型理論そのものは自然数の定義を前提とはしていない。
ST に固有な記号として、プライム付きの変数と接中辞 ∈ がある。論理式において、プライムのない変数は全て同じ型に属し、プライム付き変数 ("x′") はその1つ上の型に属する。ST の原子論理式は、（恒等式）か という形式である。接中辞記号 ∈ は、集合の所属関係を示唆している。
以下にあげる公理に使われている変数は、全て2つの連続する型のいずれかに属する。プライムなしの変数は低位の型の変数であり、 ∈ の左辺にのみ出現する（プライムつきは逆）。ST での一階述語論理では、型をまたいだ量化ができない。従って、ある型とそれに隣接する型ごとに外延性と内包性の公理を定義する必要が出てくるが、下記の外延性と内包性の公理を型をまたいで成り立つ公理型 (axiom schema) とすればよい。
ST は型理論が公理的集合論と似ていることを明らかにした。さらに、ZFC などの従来の集合論よりも単純な存在論に基づく "iterative conception of set" と呼ばれる ST のより精巧な存在論がもっと簡単な公理（公理型）を構成している。型理論の出発点は集合論だが、その公理、存在論、用語は異なる。型理論には他にも や がある。
型システム.
型システムの定義は様々だが、プログラミング言語理論の世界では Benjamin C. Pierce の定義が一般に受け入れられている。
換言すれば、型システムはプログラムの値を「型」と呼ばれる集合に分類し（これを「型設定」あるいは「型割り当て」と呼ぶ）、特定のプログラムの動作が不正であることを示す。例えば、"hello" という値を文字列型、5 という値を整数型としたとき、プログラマに "hello" と 5 を加算できないといった制限を課すのである。このような型システムでは、次のプログラム
は不正である。もちろん、文字列と整数を加算することを許す型システムもありうる。
型システムの設計と実装は、プログラミング言語そのものと同じ程度に広がりを持った話題である。実際、プログラミング言語の最大の基盤は型システムであるとも言われ、「型システムを正しく設計すれば、言語は自分自身で設計される」と言われている。
型理論の他分野への影響.
コンピューター.
型理論の最も顕著な応用は、プログラミング言語のコンパイラでの意味論解析部での型チェックアルゴリズムの構築である。
型理論は自然言語の意味論の理論構築にもよく使われる。以下ではモンタギュー文法の内包論理（型理論と様相論理を折衷したもの）での型を例として説明する。最も基本的な型として formula_1（entity=もの）と formula_2（truth-value=真理値）があり、以下の規則を帰納的に適用して型の集合を定義する。
formula_5 という複合型は、ある型 formula_3 の要素から formula_4 の要素への関数型である。つまり、formula_12 は「もの」から真理値への関数であり、いわば集合の指示関数である。formula_13 は、指示関数の指す集合から真理値への関数であり、いわば集合の集合である。後者は自然言語で言えば、" every boy" とか " nobody" といった表現に相当する（Montague 1973, Barwise and Cooper 1981）。
言語学.
言語学の分野では自然言語の形式意味論の研究に用いられている。モンタギュー文法が代表的である。