跳至內容

類型居留問題

維基百科,自由的百科全書

簡單類型lambda演算中,類型居留(Type inhabitation)問題是如下問題:給定一個類型 ,是否存在一個 -項 M 使得對於某個類型環境 ?在空的類型環境中,如果回答是肯定的,則 M 被稱為 的居留元(inhabitant)。

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

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