直観主義型理論
ウィキペディア フリーな encyclopedia
直観主義型理論(ちょっかんしゅぎかたりろん、英: intuitionistic type theory)とは、数学の代替基盤を目指して論理学・哲学者のペール・マルティン=レーフによって開発された型理論を言う。構成的型理論(constructive type theory)、またはマルティン=レーフの型理論(Martin-Löf's type theory)とも呼ばれる。1972年に最初のバージョンが発表された。直観主義型理論には複数のバージョンがある。
マルティン=レーフは当初非可述的な定義が可能な型理論を構築していたが、ジャン=イヴ・ジラール(Jean-Yves Girard)によってパラドックスを起こすことが指摘され一時頓挫した(ジラールのパラドックス)。その後、パラドックスを起こさない可述的なバージョンが発表された。ただし、すべてのバージョンは、依存型を使用した構成的論理のコア設計を維持している。