|
===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。 ・ 型 ： [かた] 【名詞】 1. mold 2. mould 3. model 4. style 5. shape 6. data type ・ 理 ： [り] 【名詞】 1. reason ・ 理論 ： [りろん] 【名詞】 1. theory ・ 論 ： [ろん] 【名詞】 1. (1) argument 2. discussion 3. dispute 4. controversy 5. discourse 6. debate 7. (2) theory 8. doctrine 9. (3) essay 10. treatise 1 1. comment
型理論（かたりろん、）は、数理論理学の一分野であり、「型」の階層を構築し、それぞれの型に数学的（あるいはそれ以外の）実体を割り当てるものである。階型理論（かいけいりろん、）とも。ある型のオブジェクトはその前提となる型のオブジェクトから構築される。この場合の「型」とは形而上的な意味での「型」である。バートランド・ラッセルは、彼が発見したラッセルのパラドックスにより素朴集合論の問題が明らかにされたことを受けて、型理論を構築した。型理論の詳細はホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』にある。 型理論は、プログラミング言語の理論における型システムのベースにもなっている。「型システム」と「型理論」の語はほぼ同義として扱われることもあるが、ここでは、この記事では数理論理学の範囲を説明し、プログラミング言語の理論については型システムの記事で説明する。 == 単純階型理論（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’'' ↔ ''y''∈''z’'' * 外延性: ∀''x''↔ ''x''∈''z’'' → ''y’''=''z’'' : ここで、自由変項 ''x'' を含む任意の一階述語論理式を Φ(''x'') で表すものとする。 * 内包性: ∃''z’''∀''x''↔ Φ(''x'') : ''注意'': 同じ型の要素を集めたものは次のレベルの型のオブジェクトを形成する。''内包性''は型に関する公理というだけでなく、Φ(''x'') の公理でもある。 * 無限性: 空でない二項関係 ''R'' が最下層の型の個体要素間に成り立つとき、それは非反射的で推移的であり、強連結である (∀''x, y'' ∨ ''yRx'' )。 : ''注意'': ''無限性'' は純粋に数学的な ST 固有の公理である。これは ''R'' が全順序関係であることを意味している。最下層の型に 0 を割り当てたとき、''R'' の型は 3 となる。''無限性'' が成り立つのは ''R'' の議論領域が無限のときだけであり、結果として無限集合の存在を前提としている。関係を順序対で定義する場合、この公理の前に順序対を定義する必要が生じる。これは ST に Kuratowski の定義を導入することで実現する。ZFCのような他の集合論の無限集合の公理が何故 ST で採用されなかったのかは書籍にも書かれていない。 ST は型理論が公理的集合論と似ていることを明らかにした。さらに、ZFC などの従来の集合論よりも単純な存在論に基づく "iterative conception of set" と呼ばれる ST のより精巧な存在論がもっと簡単な公理（公理型）を構成している。型理論の出発点は集合論だが、その公理、存在論、用語は異なる。型理論には他にも New Foundations や Scott-Potter set theory がある。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「型理論」の詳細全文を読む スポンサード リンク
|