直観主義型理論

直観主義型理論の概要

直観主義型理論（Intuitionistic Type Theory）は、数学の新たな基盤を目指して論理学者であり哲学者であるペール・マルティン＝レーフによって開発された型理論の一種です。この理論は1972年に最初のバージョンが発表され、以後、構成的型理論（Constructive Type Theory）やマルティン＝レーフの型理論とも呼ばれるようになりました。直観主義型理論にはいくつかの異なるバージョンが存在し、それぞれが独自の特徴を持っています。

設計の背景

マルティン＝レーフは、この型理論を設計するにあたり、数学的な構成主義の原理に基づきました。構成主義は、「証拠」を伴った存在証明が必須であるという考え方を含みます。例えば、「1000より大きい素数が存在する」という証明では、実際に1000を超える具体的な素数を提示する必要があります。この考え方に沿って、直観主義型理論はBHK解釈（Brouwer–Heyting–Kolmogorov interpretation）を内包する形で設計されています。興味深い点は、証明が研究、比較、操作可能な数学的対象として扱われることです。

直観主義型理論における型構築子（type constructor）は、論理演算子と密接に関連して作られています。たとえば、含意という論理演算子（A ⇒ B）は、関数型（A → B）として表現されることになります。このような型と論理の対応関係はカリー＝ハワード同型対応（Curry-Howard Correspondence）と呼ばれています。従来の型理論でもこの同型は存在していましたが、マルティン＝レーフの型理論は依存型（dependent type）を取り入れることで、述語論理を新たに拡張した最初のものです。

型理論の構造

直観主義型理論は、三種類の有限型を特徴としており、これらは五つの異なる型構築子を組み合わせて構成されています。この理論は、第一階述語論理に基づく集合論とは異なるアプローチをとっており、それぞれの型理論が数学及び論理学の特性を兼ね備えた役割を果たしています。型に対する理解が浅い場合には、型は項（term）を含むものであり、項は一つだけの型に属すると言うことができます。

例えば、2 + 2や2 ⋅ 2といった項は計算により4というカノニカルな項に変わることが可能です。型理論に関心がある方は、さらに詳細な情報を探索することをおすすめします。

判断とその役割

直観主義型理論は、判断（judgement）を用いて形式定義が行われます。例えば、「もし A が型であり、B も型であるならば、Σ(a:A)B も型である」という表現は、「型である」「かつ」「もし...ならば」といった判断が組み合わさっています。

ここで、Σ(a:A)Bの表現そのものは定義された型であって、判断ではありません。

型理論の実装と応用

さまざまな形式の型理論は、数多くの証明支援システムのための基盤形式システムとして実装されています。多くのシステムがマルティン＝レーフのアイディアを取り入れていますが、他にも異なる特性や追加の公理、哲学的背景を持つものもあります。例えば、NuPRLシステムは計算型理論に基づいており、Coqは帰納的構成計算に基づいています。また、依存型は、ATS、Cayenne、Epigram、Agda、Idrisといったプログラミング言語の設計でも利用されています。

バージョンの多様性

ペール・マルティン＝レーフは、いくつかの型理論を発表し、それぞれの発表時期は異なります。この素描には、印刷された形で公表された理論の一覧が含まれ、その特徴が描かれています。すべての理論は、依存積（dependent product）、依存和（dependent sum）を持ち、自然数を含む有限型を特徴としています。全ての理論は、依存積に対するη-簡約が追加されたMLTT79を除き、同じ簡約規則を持ちます。

MLTT71

MLTT71は、マルティン＝レーフが1971年に初めて提案した型理論です。この理論は一つの宇宙を持ち、今日「Type in Type」と呼ばれる概念を含んでいますが、ジャン＝イヴ・ジラールによって矛盾が示されたため、出版されることはありませんでした。

このように、直観主義型理論は構成的アプローチを通じて数学の基盤を再考する重要な理論であり、その多様性は数学やプログラミング言語に深く影響を与えています。

もう一度検索