考虑通常称为 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 → τ in Γ，则非确定性地选择它，设置 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 同构等）。一定有什么我看不到的。
抱歉，我不习惯 unicode，所以不支持 LaTeX。我还在 MO https://mathoverflow.net/questions/140045/is-there-an-easy-decision-algorithm-for-the-inhabitation-problem-for-simple-type上问了同样的问题，但是 lambda 演算小组在那里似乎不太活跃。