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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.