Is there an easy decision algorithm for the inhabitation problem for simple types?

Consider the basic system of simple types usually known as $TA_\lambda$. One can prove that (as a consequence of the Subject Reduction Property and the fact that any typable term is strongly $\beta$-normalising)

• If $\tau$ has an inhabitant, then it has one in $\beta$-normal form.

It follows that given an inhabitation problem $\Gamma \vdash X : \tau$ we can effectively construct an algorithm that nondeterministically guesses step by step the shape of a normal solution: either (i) $X \equiv xY_1 \dots Y_n$ or (ii) $X \equiv \lambda z.Y$:

(i) If for some $n \geq 0$ there a judgment $x : \sigma_1 \to \dots \to \sigma_n \to \tau$ in $\Gamma$, then nondeterministically select it, set $X \equiv xY_1\dots Y_n$ and (only if $n>0$) consider parallel problems $$\Gamma \vdash Y_1 : \sigma_1, \dots, \Gamma \vdash Y_n : \sigma_n$$ (ii) If $\tau \equiv \tau_1 \to \tau_2$, then for a fresh variable $z$, set $X \equiv \lambda z.Y$ and consider the problem $$\Gamma, z : \tau_1 \vdash Y : \tau_2.$$

Furthermore, since all types in the constraints at each step of the algorithm are proper subtypes of the original input , the number of steps of the algorithm is at most polynomial in the size of $\tau$. Therefore the algorithm above is a decision procedure for the inhabitation problem.

My question is the following: is there something wrong in the above reasoning? Maybe not, but in this case why I've been searching all day for a decision procedure for the inhabitation problem for simple types, but all the proofs I can find are rather long and use complicated machinery (e.g. long normal forms, Curry-Howard isomorphism, etc...)?

• Can you be a bit more specific about your type theory? Not everyone know what $TA_\lambda$ is supposed to be. Are there basic types? Are there sums and the empty type? – Andrej Bauer Aug 21 '13 at 22:53
• How is what you are talking about different from a decision procedure for provability of formulas in intuitionistic propositional calculus? – Andrej Bauer Aug 21 '13 at 22:54
• @AndrejBauer I'm sorry I mean the basic system of simply typed $\lambda$-terms with just typing rules of arrow introduction, arrow elimination and variable. Do I need to be more specific? – Alfie Aug 21 '13 at 23:06
• Maybe it's not, but why do you need to use the full power of the Curry-Howard isomorphism, when you have this nice syntactical proof? – Alfie Aug 21 '13 at 23:08
• @AndrejBauer Also you usually assume the existence of a countably infinite set of atomic types, but I don't think it's too important for this. – Alfie Aug 21 '13 at 23:12

Your algorithm may not terminate. Consider $x : \alpha \to \alpha \vdash X : \alpha$. If you select $x : \alpha \to \alpha$ according to (i), then $X = xY$ and you end up with the same problem $x : \alpha \to \alpha \vdash Y : \alpha$ to consider recursively. An algorithm to solve the inhabitation problem not much more complex than your incorrect one is by Ben-Yelles and independently by Wajsberg. Search the web, or look into e.g. Hindley "Basic Simple Type Theory".