直観主義型理論

直観主義型理論（ちょっかんしゅぎかたりろん、英: intuitionistic type theory）とは、数学の代替基盤を目指して論理学・哲学者のペール・マルティン＝レーフによって開発された型理論を言う。構成的型理論（constructive type theory）、またはマルティン＝レーフの型理論（Martin-Löf's type theory）とも呼ばれる。1972年に最初のバージョンが発表された。直観主義型理論には複数のバージョンがある。

マルティン＝レーフは当初非可述的な定義が可能な型理論を構築していたが、ジャン＝イヴ・ジラール（Jean-Yves Girard）によってパラドックスを起こすことが指摘され一時頓挫した（ジラールのパラドックス）。その後、パラドックスを起こさない可述的なバージョンが発表された。ただし、すべてのバージョンは、依存型を使用した構成的論理のコア設計を維持している。

設計方針[編集]

マルティン＝レーフは、この型理論を数学における構成主義の原理に基づいて設計をおこなった。構成主義は、「証拠」を含んだ存在証明を必要とする。すなわち、「１０００より大きい素数が存在する」という証明においては、１０００よりも大きくかつ素数である特定の数を確定しなければならない。直観主義型理論は、BHK解釈（Brouwer–Heyting–Kolmogorov interpretation）を内部化するという設計方針を達成している。興味深い点として、証明（proof）が、調査、比較、そして操作できる数学的対象になるというところがある。

直観主義型理論の型構築子（type constructor）は、論理演算子（logical connective）と一対一で対応するように作られている。例えば、含意と呼ばれる論理演算子（ $A\implies B$ ）は、関数型（ $A\to B$ ）に対応する。この対応はカリー＝ハワード同型対応と呼ばれる。かつての型理論もこの同型対応に従っていたが、現在のマルティン＝レーフの型理論は依存型（dependent type）を導入することによって述語論理をそのように拡張した最初のものである。

型理論[編集]

直観主義型理論は３つの有限型を持つ。その有限型は５つの異なる型構築子（type constructor）を組み合わせたものである。集合論とは異なり、型理論は第一階述語論理のような論理学をベースに構築されてはいない。だから、それぞれの型理論の特徴は、数学と論理学両方の特徴としての役割を果たす。

型理論に親しんでいないが、集合論を知っているという人に対する簡単な要約は次のとおりである。集合が元を含むのと同じように型は項（term）を含む。項は一つそしてただ一つだけの型に属する。 $2+2$ や $2\cdot 2$ のような項は計算（簡約）すると4のようなカノニカルな項（canonical term）になる。さらに知りたい場合は型理論の記事を参照せよ

判断（judgement）[編集]

直観主義型理論の形式定義は判断（judgement）を用いて書かれる。例えば、"if $A$ is a type and $B$ is a type then $\textstyle \sum _{a:A}B$ is a type" の中には "is a type", "and", そして "if ... then ..." という判断が混ざっている。 $\textstyle \sum _{a:A}B$ という表現は判断ではない。それは定義されている型である。

型理論の実装[編集]

さまざまな形式の型理論が、多数の証明支援系の基盤の形式システムとして実装されている。多くがマルティン＝レーフのアイディアに基づいている一方、多くは別の特徴、さらなる公理、もしくは異なる哲学的背景が追加されている。具体的には、NuPRLシステムは、計算型理論（computational type theory）に基づいており^[1]、Coqは（余）帰納的構成計算（calculus of (co)inductive constructions）に基づいている。依存型は、ATS、Cayenne、Epigram、Agda^[2]、Idris^[3]などのプログラム言語の設計にも使用される。

型理論のバージョン[編集]

ペール・マルティン＝レーフはいくつもの型理論を構成したが、その発表の時期は、それらが記述された査読前論文が専門家（ジャン＝イヴ・ジラールやGiovanni Sambin）に受理されることになったときよりだいぶ後のさまざまな時期に発表された。以下のリストは、印刷された形態で記述された全ての理論を列挙することを試みたものであり、それらを互いに区別するための重要な特徴を素描している。これら理論の全ては依存積（dependent product）、依存和（dependent sum）、分離和（disjoint union）、有限型（finite type）、そして自然数を持つ。全ての理論は、依存積に対するη-簡約が追加されたMLTT79を除いて、依存積か依存和のどちらかに対するη-簡約を含まない同じ簡約規則を持つ。

MLTT71: MLTT71 はペール・マルティン＝レーフによって作られた最初の型理論であり、1971年に査読前原稿の中で登場した。それは一つの宇宙（universe）を持っていたが、この宇宙にはそれ自身名前を持っていた。つまり、今日"Type in Type"と呼ばれるものを持つ型理論であった。ジャン＝イヴ・ジラールは、この体系は矛盾していることを示した。そして、この査読前原稿は一度も出版されていない。

脚注[編集]

^ Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. (2006). “Innovations in computational type theory using Nuprl”. Journal of Applied Logic 4 (4): 428–469. doi:10.1016/j.jal.2005.10.005.
^ Norell, Ulf (2009). Dependently Typed Programming in Agda. TLDI '09. New York, NY, USA: ACM. 1–2. doi:10.1145/1481861.1481862. ISBN 9781605584201
^ Brady, Edwin (2013). “Idris, a general-purpose dependently typed programming language: Design and implementation”. Journal of Functional Programming 23 (5): 552–593. doi:10.1017/S095679681300018X. ISSN 0956-7968.

参考文献　[編集]

外部リンク[編集]

EU Types Project: Tutorials – 型についての夏の学校2005の講義録及びスライド
n-Categories - Sketch of a Definition – 1995年11月２９日付のジョン・バエズとJames Dolanからロス・ストリートへの手紙

[1] Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. (2006). “Innovations in computational type theory using Nuprl”. Journal of Applied Logic 4 (4): 428–469. doi:10.1016/j.jal.2005.10.005.

[2] Norell, Ulf (2009). Dependently Typed Programming in Agda. TLDI '09. New York, NY, USA: ACM. 1–2. doi:10.1145/1481861.1481862. ISBN 9781605584201

[3] Brady, Edwin (2013). “Idris, a general-purpose dependently typed programming language: Design and implementation”. Journal of Functional Programming 23 (5): 552–593. doi:10.1017/S095679681300018X. ISSN 0956-7968.

[1]

[2]

[3]