型理論のバージョン
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/07/10 01:05 UTC 版)
「直観主義型理論」の記事における「型理論のバージョン」の解説
ペール・マルティン＝レーフはいくつもの型理論を構成したが、その発表の時期は、それらが記述された査読前論文が専門家（ジャン＝イヴ・ジラールやGiovanni Sambin）に受理されることになったときよりだいぶ後のさまざまな時期に発表された。以下のリストは、印刷された形態で記述された全ての理論を列挙することを試みたものであり、それらを互いに区別するための重要な特徴を素描している。これら理論の全ては依存積（dependent product）、依存和（dependent sum）、分離和（disjoint union）、有限型（finite type）、そして自然数を持つ。全ての理論は、依存積に対するη-簡約が追加されたMLTT79を除いて、依存積か依存和のどちらかに対するη-簡約を含まない同じ簡約規則を持つ。 MLTT71 MLTT71 はペール・マルティン＝レーフによって作られた最初の型理論であり、1971年に査読前原稿の中で登場した。それは一つの宇宙（universe）を持っていたが、この宇宙にはそれ自身名前を持っていた。つまり、今日"Type in Type"と呼ばれるものを持つ型理論であった。ジャン＝イヴ・ジラールは、この体系は矛盾していることを示した。そして、この査読前原稿は一度も出版されていない。
※この「型理論のバージョン」の解説は、「直観主義型理論」の解説の一部です。
「型理論のバージョン」を含む「直観主義型理論」の記事については、「直観主義型理論」の概要を参照ください。
ウィキペディア小見出し辞書の「型理論のバージョン」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 型理論のバージョンのページへのリンク
