3
$\begingroup$

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...)?

$\endgroup$
  • 2
    $\begingroup$ 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? $\endgroup$ – Andrej Bauer Aug 21 '13 at 22:53
  • $\begingroup$ How is what you are talking about different from a decision procedure for provability of formulas in intuitionistic propositional calculus? $\endgroup$ – Andrej Bauer Aug 21 '13 at 22:54
  • $\begingroup$ @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? $\endgroup$ – Alfie Aug 21 '13 at 23:06
  • $\begingroup$ 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? $\endgroup$ – Alfie Aug 21 '13 at 23:08
  • $\begingroup$ @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. $\endgroup$ – Alfie Aug 21 '13 at 23:12
2
$\begingroup$

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".

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.