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?