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