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?