「型理論」の版間の差分

削除された内容追加された内容

インライン

2024年7月16日 (火) 02:59時点における最新版

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

20世紀初頭にバートランド・ラッセルが発見した、ラッセルのパラドックスによるフレーゲの素朴集合論の欠陥を説明する中で提起されたタイプ理論（theories of type）が型理論の起源であり^[1]、後年にAxiom of reducibilityが付随された型理論は、ホワイトヘッドとラッセルの『プリンキピア・マテマティカ』に収録されている^[2]。

単純階型理論（Simple Theory of Types）

→詳細は「ST型理論（英語版）」を参照

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

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

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

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

同一性

x = y \leftrightarrow \forall z' [x \in z' \leftrightarrow y \in z']

外延性

\forall x [x \in y' \leftrightarrow x \in z'] \to y' = z'

ここで、自由変項 x を含む任意の一階述語論理式を

Φ(x)

で表すものとする。

内包性

\exists z' \forall x [x \in z' \leftrightarrow Φ(x)]

注意: 同じ型の要素を集めたものは次のレベルの型のオブジェクトを形成する。内包性は型に関する公理というだけでなく、 $Φ(x)$ の公理でもある。

無限性

最下層の型の個体要素間についての空でない二項関係

R

で以下を満たすものが存在。

狭義の全順序（非反射的で推移的で、強連結 ( $\forall x, y [''x \neq y''\leftrightarrow[''xRy'' \lor ''yRx'']])$ ) で有り、極小元以外の任意の要素はそれより大きい要素を持つ（余定義域は定義域の部分領域で有る）。
注意: 無限性 は純粋に数学的な ST 固有の公理である。これは R が全順序関係であることを意味している。最下層の型に 0 を割り当てたとき、R の型は 3 となる。無限性 が成り立つのは R の議論領域が無限のときだけであり、結果として無限集合の存在を前提としている。関係を順序対で定義する場合、この公理の前に順序対を定義する必要が生じる。これは ST に Kuratowski の定義を導入することで実現する。ZFCのような他の集合論の無限集合の公理がなぜ ST で採用されなかったのかは書籍にも書かれていない。

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

型システム

→詳細は「型システム」を参照

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

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

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

"hello" + 5

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

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

型理論の他分野への影響

コンピューター

型理論の最も顕著な応用は、プログラミング言語のコンパイラでの意味論解析部での型チェックアルゴリズムの構築である。

型理論は自然言語の意味論の理論構築にもよく使われる。以下ではモンタギュー文法の内包論理（型理論と様相論理を折衷したもの）での型を例として説明する。最も基本的な型として $e$ （entity=もの）と $t$ （truth-value=真理値）があり、以下の規則を帰納的に適用して型の集合を定義する。

$a$ と $b$ が型であるとき、 $\langle a,b\rangle$ も型である。
$a$ が型であるとき、 $\langle s,a\rangle$ も型である。ここで、 $s$ は型ではなく、指標（可能世界と時点の組み合わせ）である。こちらの規則は様相論理（可能世界）や時相論理（時点）も関わってくる。

$\langle a,b\rangle$ という複合型は、ある型 $a$ の要素から $b$ の要素への関数型である。つまり、 $\langle e,t\rangle$ は「もの」から真理値への関数であり、いわば集合の指示関数である。 $\langle \langle e,t\rangle ,t\rangle$ は、指示関数の指す集合から真理値への関数であり、いわば集合の集合である。後者は自然言語で言えば、 every boy とか nobody といった表現に相当する（Montague 1973, Barwise and Cooper 1981）。

言語学

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

脚注

[脚注の使い方]

出典

^ Russell's (1902) Letter to Frege appears, with commentary, in van Heijenoort 1967:124–125.
^ cf. Quine's commentary before Russell (1908) Mathematical Logic as based on the theory of types in van Heijenoort 1967:150

参考文献

Robert L. Constable (ed.). "Computational type theory". 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。

@@ 1行目: / 1行目: @@
+'''型理論'''（かたりろん、{{lang-en-short|Type theory}}）とは、[[プログラミング]]・[[数学]]・[[言語学]]等に現れる[[データ型|型]]の概念及びそれらが成す[[型システム]]を研究対象とする[[数学]]・[[計算機科学]]の分野である。特定の[[型システム]]のことを型理論と呼ぶこともある。[[集合論]]の代替となる数学の基礎として役立てられる型理論（型システム）も存在する。そのような例として[[アロンゾ・チャーチ]]の[[型付きラムダ計算]]や[[ペール・マルティン＝レーフ|マルティン・レーフ]]の[[直観主義型理論]]が有名である。
-'''型理論'''（かたりろん、{{lang-en-short|Type theory}}）は、[[数理論理学]]の一分野であり、「型」の階層を構築し、それぞれの型に数学的（あるいはそれ以外の）実体を割り当てるものである。'''階型理論'''（かいけいりろん、{{lang-en-short|Theory of Types}}）とも。ある型のオブジェクトはその前提となる型のオブジェクトから構築される。この場合の「型」とは形而上的な意味での「型」である。[[バートランド・ラッセル]]は、彼が発見した[[ラッセルのパラドックス]]により[[素朴集合論]]の問題が明らかにされたことを受けて、型理論を構築した。型理論の詳細は[[アルフレッド・ノース・ホワイトヘッド|ホワイトヘッド]]と[[バートランド・ラッセル|ラッセル]]の 『[[プリンキピア・マテマティカ]]』にある。
+世紀初頭に[[バートランド・ラッセル]]が発見した、[[ラッセルのパラドックス]]による[[ゴットロープ・フレーゲ|フレーゲ]]の[[素朴集合論]]の欠陥を説明する中で提起されたタイプ理論（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 を割り当てる。ただし、型理論そのものは自然数の定義を前提とはしていない。
+階層中、最も低い型では、個体要素にはメンバーはなく、それらは2番目に低い型のメンバーとなる。最下層の型の個体要素は、ある集合論の原要素 (Ur-elements) に対応する。それぞれの型にはより高位の型があり、[[ペアノの公理]]の後者関数 (successor function) の記法にも似ている。'''ST''' では、最高位の型があるかどうかは規定していない。超限数個の型があってもなんら不都合は生じない。このようにペアノの公理と似た性質であるため、各型に[[自然数]]を割り当てることが容易で、最下層の型に 0 を割り当てる。ただし、型理論そのものは自然数の定義を前提とはしていない。
-'''ST''' に固有な記号として、プライム付きの変数と[[接中辞]] ∈ がある。[[論理式]]において、プライムのない変数は全て同じ型に属し、プライム付き変数（''x' '')はその1つ上の型に属する。'''ST''' の[[原子論理式]]は、''x=y'' （[[恒等式]]）か ''y''∈''x ’'' という形式である。接中辞記号 ∈ は、[[集合]]の包含関係を示唆している。
+'''ST''' に固有な記号として、プライム付きの変数と[[接中辞]] ∈ がある。[[論理式 (数学)|論理式]]において、プライムのない変数は全て同じ型に属し、プライム付き変数 (''x′'') はその1つ上の型に属する。'''ST''' の[[原子論理式]]は、{{math|''x {{=}} y''}}（[[恒等式]]）か {{math|''y'' ∈ ''x′''}} という形式である。接中辞記号 ∈ は、[[集合]]の所属関係を示唆している。
-以下にあげる公理に使われている変数は、全て2つの連続する型のいずれかに属する。プライムなしの変数は低位の型の変数であり、'∈' の左辺にのみ出現する（プライムつきは逆）。'''ST''' での一階述語論理では、型をまたいだ量化ができない。従って、ある型とそれに隣接する型ごとに外延性と内包性の公理を定義する必要が出てくるが、下記の外延性と内包性の公理を型をまたいで成り立つ[[公理型]]（axiom schema）とすればよい。
+以下にあげる公理に使われている変数は、全て2つの連続する型のいずれかに属する。プライムなしの変数は低位の型の変数であり、 ∈ の左辺にのみ出現する（プライムつきは逆）。'''ST''' での一階述語論理では、型をまたいだ量化ができない。従って、ある型とそれに隣接する型ごとに外延性と内包性の公理を定義する必要が出てくるが、下記の外延性と内包性の公理を型をまたいで成り立つ[[公理図式]] (axiom schema) とすればよい。
-* '''同一性''': ''x''=''y'' ↔ ∀''z’'' [''x''&isin;''z’'' &harr; ''y''&isin;''z’'']
+; 同一性 : {{math|''x'' {{=}} ''y'' ↔ ∀''z′'' [''x''&isin;''z′'' &harr; ''y''&isin;''z′'']}}
-* '''外延性''': ∀''x''[''x''&isin;''y’'' &harr; ''x''&isin;''z’''] → ''y’''=''z’''
+; 外延性 : {{math|∀''x''[''x''&isin;''y′'' &harr; ''x''&isin;''z′''] → ''y′'' {{=}} ''z′''}}
-: ここで、[[自由変項]] ''x'' を含む任意の[[一階述語論理]]式を Φ(''x'') で表すものとする。
+: ここで、[[自由変項]] ''x'' を含む任意の[[一階述語論理]]式を {{math|Φ(''x'')}} で表すものとする。
-* '''内包性''': ∃''z’''∀''x''[''x''&isin;''z’'' &harr; &Phi;(''x'')]
+; 内包性 : {{math|∃''z′''∀''x''[''x''&isin;''z′'' &harr; &Phi;(''x'')]}}
-: ''注意'': 同じ型の要素を集めたものは次のレベルの型のオブジェクトを形成する。''内包性''は型に関する公理というだけでなく、Φ(''x'') の公理でもある。
+:; 注意 : 同じ型の要素を集めたものは次のレベルの型のオブジェクトを形成する。''内包性''は型に関する公理というだけでなく、 {{math|Φ(''x'')}} の公理でもある。
-* '''無限性''': 空でない[[二項関係]] ''R'' が最下層の型の個体要素間に成り立つとき、それは非[[反射関係|反射的]]で[[推移関係|推移的]]であり、強連結である (∀''x, y'' [''xRy'' &or; ''yRx''])。<!-- [It looks like &or; ''x=y'' is missing.] -->
+; 無限性 : 最下層の型の個体要素間についての空でない[[二項関係]] {{math|''R''}} で以下を満たすものが存在。
-: ''注意'': ''無限性'' は純粋に数学的な '''ST''' 固有の公理である。これは ''R'' が全順序関係であることを意味している。最下層の型に 0 を割り当てたとき、''R'' の型は 3 となる。''無限性'' が成り立つのは ''R'' の議論領域が無限のときだけであり、結果として無限集合の存在を前提としている。関係を順序対で定義する場合、この公理の前に順序対を定義する必要が生じる。これは '''ST''' に Kuratowski の定義を導入することで実現する。[[公理的集合論#ZF 公理系|ZFC]]のような他の集合論の無限集合の公理が何故 '''ST''' で採用されなかったのかは書籍にも書かれていない。
+:: 狭義の全順序（非[[反射関係|反射的]]で[[推移関係|推移的]]で、強連結 ({{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]] がある。
+'''ST''' は型理論が[[公理的集合論]]と似ていることを明らかにした。さらに、ZFC などの従来の集合論よりも単純な[[存在論]]に基づく "iterative conception of set" と呼ばれる '''ST''' のより精巧な存在論がもっと簡単な公理（公理図式）を構成している。型理論の出発点は集合論だが、その公理、[[存在論]]、用語は異なる。型理論には他にも [[:en:New Foundations|New Foundations]] や [[:en:Scott-Potter set theory|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）。
 == 型システム ==
@@ 50行目: / 38行目: @@
 型システムの設計と実装は、プログラミング言語そのものと同じ程度に広がりを持った話題である。実際、プログラミング言語の最大の基盤は型システムであるとも言われ、「型システムを正しく設計すれば、言語は自分自身で設計される」と言われている{{要出典|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/>
 == 参考文献 ==
@@ 59行目: / 66行目: @@
 == 関連項目 ==
 {{ウィキポータルリンク|数学}}
-* [[ペール・マルティン＝レーフ]]
+* [[バートランド・ラッセル]]
+*[[ペール・マルティン＝レーフ]]
-* [[型システム]]
+*[[アロンゾ・チャーチ]]
+* [[型付きラムダ計算]]
+*[[直観主義型理論]]
+*[[型システム]]
 * [[データ型]]
 * [[領域理論]]
 * [[圏論]]
-* [[型付きラムダ計算]]
-* [[バートランド・ラッセル]]
 {{Mathlogic-stub}}