住性 (型理論)

型理論において 、型住性問題(type inhabitation problem)とは、型${\displaystyle \tau }$と型環境${\displaystyle \Gamma }$が与えられたとき、 ${\displaystyle \Gamma \vdash t:\tau }$ を満足する項tが存在するか否かの判定問題である。そのような項tが存在するとき、項tは 型${\displaystyle \tau }$の住人であるといい、 型${\displaystyle \tau }$は有項であるという。

単純型付きラムダ計算においては、型が有項であることとminimal implicative logicにおいてその型と対応する命題が恒真であることは同値である。同様に、System F の型が有項であることと二階述語論理においてその型と対応する命題が恒真であることは同値である。

多くの計算体系において、型住性問題は大変困難である。単純型付きラムダ計算においては型住性問題はPSPACE完全であることが Richard Statmanにより示されている。System Fにおいては決定不能である。