About: 型理論

型理論（かたりろん、英: Type theory）は、集合論を数学基礎論の視点から代替する理論である。階型理論（かいけいりろん、英: Theory of Types）とも呼ばれる。アロンゾ・チャーチの型付きラムダ計算と、マルティン・レーフの直観主義型理論が有名である。計算機科学やコンピュータプログラミングで用いられる型システムの学術研究として知られる。 20世紀初頭にバートランド・ラッセルが発見した、ラッセルのパラドックスによるフレーゲの素朴集合論の欠陥を説明する中で提起されたtheories of typeが型理論の起源であり、後年にAxiom of reducibilityが付随された型理論は、ホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』に収録されている。