Inhabitation of STLC is in PSPACE

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?