住性 (型理論)

ウィキペディア

住性 (型理論)

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/06/08 13:41 UTC 版)

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