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


論理との関係

編集

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

Formal properties

編集

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

参考文献

編集