2
$\begingroup$

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?

$\endgroup$

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.