類型居留問題

在簡單類型lambda演算中，類型居留（Type inhabitation）問題是如下問題：給定一個類型 $\tau$，是否存在一個 $\lambda$-項 M 使得對於某個類型環境 $\Gamma$ 有 $\Gamma \vdash M:\tau$？在空的類型環境中，如果回答是肯定的，則 M 被稱為 $\tau$ 的居留元（inhabitant）。

因為在簡單類型的 lambda 演算中類型對應於極小蘊涵邏輯(參見 Curry-Howard 同構)，一個類型有一個居留元，當且僅當它是極小蘊涵邏輯的重言式。

Richard Statman 證明了在簡單類型λ演算中類型居留問題是 PSPACE-完全性的。