3 added 10 characters in body

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 = xY_1\dots Y_n$$$$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 = \lambda z.Y$$$$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...)?

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

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

2 deleted 58 characters in body

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

• If $$\tau$$ has an inhabitant (i.e. $$\varnothing \vdash M : \tau$$ for some $$M$$), 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 = 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 = \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: what'sis 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...). There must be something that I don't see.?

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

• If $$\tau$$ has an inhabitant (i.e. $$\varnothing \vdash M : \tau$$ for some $$M$$), 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 = 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 = \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: what's wrong in the above reasoning? 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...). There must be something that I don't see.

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

1

# 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 so called Subject Reduction Property and the fact that any typable term is strongly $$\beta$$-normalising)

• If $$\tau$$ has an inhabitant (i.e. $$\varnothing \vdash M : \tau$$ for some $$M$$), 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 = 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 = \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: what's wrong in the above reasoning? 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...). There must be something that I don't see.