通常 TAλ として知られる単純型の基本システムを考えてみましょう。それを証明することができます (いわゆる主語還元特性と、型付け可能な項はすべて強力に β 正規化されているという事実の結果として)
If τ has an inhabitant, then it has one in β-normal form.
居住問題 Γ ⊢ X : τ が与えられると、(i) X が xY_1...Y_n であるか、(ii) X が λz であるかのいずれかである、正規解の形状を段階的に非決定論的に推測するアルゴリズムを効果的に構築できます。よ:
(i) いくつかの n ≥ 0 について、Γ で x : σ_1 → ... → σ_n → τ という判断がある場合、非決定論的にそれを選択し、X = xY_1...Y_n を設定し、(n > 0 の場合のみ) 並列問題を検討します。 Γ ⊢ Y_1 : σ_1,...,Γ ⊢ Y_n : σ_n
(ii) τ が τ_1 → τ_2 の場合、新しい変数 z に対して、X = λz.Y を設定し、問題 Γ、z : τ_1 ⊢ Y : τ_2 を検討します。
さらに、アルゴリズムの各ステップでの制約内のすべてのタイプは、元の入力の適切なサブタイプであるため、アルゴリズムのステップ数は、多くても τ のサイズの多項式です。したがって、上記のアルゴリズムは居住問題の決定手順です。
私の質問は次のとおりです。上記の推論の何が問題なのですか? 単純型の生息問題の決定手順を一日中探していましたが、見つけることができるすべての証明はかなり長く、複雑な機構を使用しています (例: 長い正規形、Curry-Howard 同型など...)。見えない何かがあるに違いない。
申し訳ありませんが、私はユニコードに慣れておらず、SO は LaTeX をサポートしていません。MO https://mathoverflow.net/questions/140045/is-there-an-easy-decision-algorithm-for-the-inhabitation-problem-for-simple-typeでも同じ質問をしましたが、ラムダ計算はグループはあまり活発ではないようです。