Urzyczyn: Inhabitation in Typed Lambda-Calculi (A syntactic approach) gives a proof that STLC inhabitation problem is in PSPACE (section 2, lemma 1). I don't understand certain aspects of the proof:
Lemma: There is an alternating polynomial time algorithm to determine whether a given type A is inhabited in a given basis $\Gamma$ in the STLC.
Proof.If a type is inhabited, it is inhabited by a term in a long normal form.
Question 1: what is a long normal form.
To determine if there exists a term $M$ in a long normal, satisfying $\Gamma \vdash M:A$ we proceed as follows:
If $A = A_1 \to A_2$ then $M$ must be an abstraction $M = \lambda x:A_1. M'$. Thus, we look for an $M'$ satifying $\Gamma, x:A_1 \vdash M':A_2$.
If $A$ is a type variable, then $M$ is an application of a variable to a sequence of terms.
Question 2: I thought there weren't type variables in the STLC.
We nondeterministically choose a variable z, declared in $\Gamma$ to be of type $A_1 \rightarrow \ldots \rightarrow A_n \rightarrow A$. If there is no such variable , we reject. If $n = 0$ then we accept. If $n > 0$, we answer in parallel the questions if $A_i$ are inhabited in $\Gamma$.
Question 3: it doesn't matter the actual typing of $z$ in $\Gamma$ right? as long as we consume it and don't use it again in this step.
This alternating procedure is repeated as long as there are new questions of the form $\Gamma \vdash ? : A$. We can assume that all types in $\Gamma$ are different. At each step of the procedure, the basis $\Gamma$ either stays the same or expands. Thus the number of steps does not exceed the squared number of subformulas of types in $\Gamma,A$.
Question 4: why? could someone spell out some steps of the reasoning here?
