タイプ居住

数理論理学の一分野である型理論において、与えられた型付き計算における、この計算の型居住問題は次の問題である: ^[1]型と型付け環境が与えられたとき、となる -項 M は存在するか? 型環境が空の場合、そのような M は の居住者であると言われる。 ${\displaystyle \tau}$ ${\displaystyle \ガンマ}$${\displaystyle \lambda}$${\displaystyle \Gamma \vdash M:\tau }$${\displaystyle \tau}$

単純型付きラムダ計算の場合、対応する命題が最小含意論理のトートロジーである場合に限り、型に居住者が存在します。同様に、 System F型には、対応する命題が直観主義 二階論理のトートロジーである場合に限り、居住者が存在します。

ジラールのパラドックスは、型の占有がカリー・ハワード対応による型システムの一貫性に強く関係していることを示しています。健全であるためには、そのようなシステムには占有されていない型がなければなりません。

ほとんどの型付き計算では、型占有問題は非常に困難です。リチャード・スタットマンは、単純に型付けされたラムダ計算では、型占有問題はPSPACE 完全であることを証明しました。System Fなどの他の計算では、問題は決定不能ですらあります。

• カリー・ハワード同型