型理論のソースを表示

'''型理論'''（かたりろん、{{lang-en-short|Type theory}}）とは、[[プログラミング]]・[[数学]]・[[言語学]]等に現れる[[データ型|型]]の概念及びそれらが成す[[型システム]]を研究対象とする[[数学]]・[[計算機科学]]の分野である。特定の[[型システム]]のことを型理論と呼ぶこともある。[[集合論]]の代替となる数学の基礎として役立てられる型理論（型システム）も存在する。そのような例として[[アロンゾ・チャーチ]]の[[型付きラムダ計算]]や[[ペール・マルティン＝レーフ|マルティン・レーフ]]の[[直観主義型理論]]が有名である。

20世紀初頭に[[バートランド・ラッセル]]が発見した、[[ラッセルのパラドックス]]による[[ゴットロープ・フレーゲ|フレーゲ]]の[[素朴集合論]]の欠陥を説明する中で提起されたタイプ理論（theories of type）が型理論の起源であり<ref>Russell's (1902) ''Letter to Frege'' appears, with commentary, in van Heijenoort 1967:124–125.</ref>、後年にAxiom of reducibilityが付随された型理論は、[[アルフレッド・ノース・ホワイトヘッド|ホワイトヘッド]]と[[バートランド・ラッセル|ラッセル]]の 『[[プリンキピア・マテマティカ]]』に収録されている<ref>cf. Quine's commentary before Russell (1908) ''Mathematical Logic as based on the theory of types'' in van Heijenoort 1967:150</ref>。

== 単純階型理論（Simple Theory of Types） ==
{{Main|{{仮リンク|ST型理論|en|ST type theory}}}}
ここでは、Mendelson (1997, 289-293）の体系 '''ST''' を解説する。[[量化]]の[[議論領域]]は型の階層に分けられ、個体要素（individuals）には型が割り当てられる。基盤となる論理は[[一階述語論理]]であり、量化変数の範囲は型によって限定される。'''ST''' は『数学原理』の型理論に比べて単純であり、任意の関係の議論領域は全て同じ型でなければならない。

階層中、最も低い型では、個体要素にはメンバーはなく、それらは2番目に低い型のメンバーとなる。最下層の型の個体要素は、ある集合論の原要素 (Ur-elements) に対応する。それぞれの型にはより高位の型があり、[[ペアノの公理]]の後者関数 (successor function) の記法にも似ている。'''ST''' では、最高位の型があるかどうかは規定していない。超限数個の型があってもなんら不都合は生じない。このようにペアノの公理と似た性質であるため、各型に[[自然数]]を割り当てることが容易で、最下層の型に 0 を割り当てる。ただし、型理論そのものは自然数の定義を前提とはしていない。

'''ST''' に固有な記号として、プライム付きの変数と[[接中辞]] ∈ がある。[[論理式 (数学)|論理式]]において、プライムのない変数は全て同じ型に属し、プライム付き変数 (''x′'') はその1つ上の型に属する。'''ST''' の[[原子論理式]]は、{{math|''x {{=}} y''}}（[[恒等式]]）か {{math|''y'' ∈ ''x′''}} という形式である。接中辞記号 ∈ は、[[集合]]の所属関係を示唆している。

以下にあげる公理に使われている変数は、全て2つの連続する型のいずれかに属する。プライムなしの変数は低位の型の変数であり、 ∈ の左辺にのみ出現する（プライムつきは逆）。'''ST''' での一階述語論理では、型をまたいだ量化ができない。従って、ある型とそれに隣接する型ごとに外延性と内包性の公理を定義する必要が出てくるが、下記の外延性と内包性の公理を型をまたいで成り立つ[[公理図式]] (axiom schema) とすればよい。

; 同一性 : {{math|''x'' {{=}} ''y'' ↔ ∀''z′'' [''x''&isin;''z′'' &harr; ''y''&isin;''z′'']}}
; 外延性 : {{math|∀''x''[''x''&isin;''y′'' &harr; ''x''&isin;''z′''] → ''y′'' {{=}} ''z′''}}
: ここで、[[自由変項]] ''x'' を含む任意の[[一階述語論理]]式を {{math|Φ(''x'')}} で表すものとする。
; 内包性 : {{math|∃''z′''∀''x''[''x''&isin;''z′'' &harr; &Phi;(''x'')]}}
:; 注意 : 同じ型の要素を集めたものは次のレベルの型のオブジェクトを形成する。''内包性''は型に関する公理というだけでなく、 {{math|Φ(''x'')}} の公理でもある。
; 無限性 : 最下層の型の個体要素間についての空でない[[二項関係]] {{math|''R''}} で以下を満たすものが存在。
:: 狭義の全順序（非[[反射関係|反射的]]で[[推移関係|推移的]]で、強連結 ({{math|∀''x, y''<nowiki>[''x &ne; y''&harr;[''xRy'' &or; ''yRx'']]</nowiki>)}}) で有り、極小元以外の任意の要素はそれより大きい要素を持つ（余定義域は定義域の部分領域で有る）。
:; 注意 : ''無限性'' は純粋に数学的な '''ST''' 固有の公理である。これは ''R'' が全順序関係であることを意味している。最下層の型に 0 を割り当てたとき、''R'' の型は 3 となる。''無限性'' が成り立つのは ''R'' の議論領域が無限のときだけであり、結果として無限集合の存在を前提としている。関係を順序対で定義する場合、この公理の前に順序対を定義する必要が生じる。これは '''ST''' に Kuratowski の定義を導入することで実現する。[[公理的集合論#ツェルメロ＝フレンケル集合論（ZF公理系）|ZFC]]のような他の集合論の無限集合の公理がなぜ '''ST''' で採用されなかったのかは書籍にも書かれていない。

'''ST''' は型理論が[[公理的集合論]]と似ていることを明らかにした。さらに、ZFC などの従来の集合論よりも単純な[[存在論]]に基づく "iterative conception of set" と呼ばれる '''ST''' のより精巧な存在論がもっと簡単な公理（公理図式）を構成している。型理論の出発点は集合論だが、その公理、[[存在論]]、用語は異なる。型理論には他にも [[:en:New Foundations|New Foundations]] や [[:en:Scott-Potter set theory|Scott-Potter set theory]] がある。

== 型システム ==
{{main|型システム}}

型システムの定義は様々だが、プログラミング言語理論の世界では Benjamin C. Pierce の定義が一般に受け入れられている。

:（型システムは）プログラムが計算する値の種類に従って句（phrase）を分類することで、そのプログラムがある動作をしないことを証明する扱いやすい文法的手法である。 (Pierce 2002)

換言すれば、型システムはプログラムの[[値 (情報工学)|値]]を「型」と呼ばれる集合に分類し（これを「型設定」あるいは「型割り当て」と呼ぶ）、特定のプログラムの動作が不正であることを示す。例えば、"hello" という値を[[文字列]]型、5 という値を[[整数]]型としたとき、プログラマに "hello" と 5 を加算できないといった制限を課すのである。このような型システムでは、次のプログラム

:<code>"hello" + 5</code>

は不正である。もちろん、文字列と整数を加算することを許す型システムもありうる。

型システムの設計と実装は、プログラミング言語そのものと同じ程度に広がりを持った話題である。実際、プログラミング言語の最大の基盤は型システムであるとも言われ、「型システムを正しく設計すれば、言語は自分自身で設計される」と言われている{{要出典|date=2011年5月|}}。

== 型理論の他分野への影響 ==
=== コンピューター ===
型理論の最も顕著な応用は、プログラミング言語の[[コンパイラ]]での意味論解析部での型チェックアルゴリズムの構築である。

型理論は[[自然言語]]の[[意味論 (論理学)|意味論]]の理論構築にもよく使われる。以下では[[モンタギュー文法]]の[[内包論理]]（型理論と[[様相論理]]を折衷したもの）での型を例として説明する。最も基本的な型として <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）。

===言語学===
[[言語学]]の分野では[[自然言語]]の[[形式意味論]]の研究に用いられている。[[モンタギュー文法]]が代表的である。

== 脚注 ==
{{脚注ヘルプ}}
=== 出典 ===
<references/>

== 参考文献 ==
*{{scholarpedia|title=Computational type theory|urlname=Computational_type_theory|curator=Robert L. Constable}}
*{{Citation | author=Per Martin-Löf | title=Intuitionistic Type Theory| year=1980 | url=http://www.csie.ntu.edu.tw/~b94087/ITT.pdf}}
*{{Citation | author=Bengt Nordström,Kent Petersson,Jan M. Smith | title=Programming in Martin-Löf's Type Theory| year=1990 | url=http://www.cse.chalmers.se/research/group/logic/book/}}
*{{Cite book|和書|editor=日本数学会編|year=2007|title=岩波数学辞典 第4版|publisher=岩波書店|isbn=978-4-00-080309-0}}

== 関連項目 ==
{{ウィキポータルリンク|数学}}
* [[バートランド・ラッセル]]
*[[ペール・マルティン＝レーフ]]
*[[アロンゾ・チャーチ]]
* [[型付きラムダ計算]]
*[[直観主義型理論]]
*[[型システム]]
* [[データ型]]
* [[領域理論]]
* [[圏論]]

{{Mathlogic-stub}}
{{DEFAULTSORT:かたりろん}}
[[Category:数理論理学]]
[[Category:型理論|*]]
[[Category:数学に関する記事]]