住性 (型理論)のソースを表示

{{孤立|date=2017年12月}}
[[型理論]]において 、型住性問題(type inhabitation problem)とは、[[型]]<math>\tau</math>と[[:en:type environment|型環境]]<math>\Gamma</math>が与えられたとき、
<math>\Gamma \vdash t : \tau</math> を満足する[[項]]tが存在するか否かの判定問題である。そのような項tが存在するとき、項tは 型<math>\tau</math>の住人であるといい、 型<math>\tau</math>は有項であるという。


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

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

== 参考文献 ==
{{reflist}}
{{デフォルトソート:しゆうせい}}
[[Category:ラムダ計算]]
[[Category:型理論]]