Решив, жилье?
Рассмотрим базовую систему простых типов, обычно известную как TAλ. Это можно доказать (как следствие так называемого свойства сокращения объекта и того факта, что любой типизированный член сильно β-нормализует)
If τ has an inhabitant, then it has one in β-normal form.
Отсюда следует, что для заданной проблемы обитания Γ ⊢ X: τ мы можем эффективно построить алгоритм, который недетерминистически угадывает форму нормального решения: либо (i) X равен xY_1...Y_n, либо (ii) X равен λz. Y:
(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.
Кроме того, поскольку все типы в ограничениях на каждом шаге алгоритма являются собственными подтипами исходного ввода, число шагов алгоритма не более чем полиномиально по размеру τ. Следовательно, приведенный выше алгоритм является процедурой решения проблемы проживания.
Мой вопрос заключается в следующем: что не так в рассуждениях выше? Я весь день искал процедуру решения проблемы обитания для простых типов, но все доказательства, которые я могу найти, довольно длинные и используют сложные механизмы (например, длинные нормальные формы, изоморфизм Карри-Ховарда и т. Д.). Должно быть что-то, чего я не вижу.
Извините, я не привык к Unicode и поэтому не поддерживает LaTeX. Я также задавал тот же вопрос на МО https://mathoverflow.net/questions/140045/is-there-an-easy-decision-algorithm-for-the-inhabitation-problem-for-simple-type, но лямбда-исчисление группа не кажется слишком активной там.