Find an inhabitant for type $\phi$

Question

I am studying from Sorensen's book (Lectures on the Curry-Howard isomorphism, ed. 2006) and there is a type that is said to be inhabited, but I need to find the inhabitant. However, I can't find it. The type is: $$\phi=[(a\rightarrow b)\rightarrow q]\rightarrow q$$ with $a=(p\rightarrow q)\rightarrow r$, $b=(p\rightarrow r)\rightarrow r$ and $p,q,r$ any variables.

Starting from what I want, I thought that I need some term $\lambda x^{(a\rightarrow b)\rightarrow q}.xN^{a\rightarrow b}$. If I keep up with abstractions I find it hard to mix the variables so that I have a term $\lambda x^{(a\rightarrow b)\rightarrow q}.x\lambda y^{a}\lambda z^{p \rightarrow r}B^r$ for some $B$ (i.e. to find a suitable $B$). So I think there must be an application (or more applications) in the term $N^{a\rightarrow b}$.

I am using the above as an example to explain what troubles me. I don't really want a solution, but some advice on how to proceed with searching for the inhabitant (if any) for a given type in general.

I have seen an example in the book where $\psi=(((((p\rightarrow q)\rightarrow p)\rightarrow p)\rightarrow q)\rightarrow q)$ is inhabited by $\lambda x^{(((p\rightarrow q)\rightarrow p)\rightarrow p)\rightarrow q}.x(\lambda y^{(p\rightarrow q)\rightarrow p}.y(\lambda z^p.x(\lambda.u^{(p\rightarrow q)\rightarrow p}.z)))$, but I can't see how to reach this result, when $\psi$ is given, despite my understanding why it is an inhabitant.

Answer 1

In the first part I solve the exercise as stated, explaining one possible thought process that would lead you to the correct solution. In the second part, I abstract the concrete example into a method that you can follow to solve type inhabitation puzzles, and suggest some problems you can practice on. Finally, in the third part, I briefly touch upon a general algorithm that can solve the type inhabitation problem for the simply-typed lambda calculus.

I. We need to construct a term that inhabits the type $((a \rightarrow b) \rightarrow q) \rightarrow q$. Since this is a function type, we need to construct a function. It seems sensible that our lambda term would have the shape $\lambda f^{(a \rightarrow b) \rightarrow q}. X$, where $X$ itself has to inhabit the type $q$. Note that the variable $f$, with type $(a \rightarrow b) \rightarrow q$, may occur inside $X$.

Now, we just need to construct the term $X$. How can we do that?

Well, we need something of type $q$. This type $q$ is not a function type, so $X$ cannot begin with a lambda. It can only have two shapes: it's either a single bound variable, or a function application $X_1 X_2$.

Can it be a single bound variable? No! The only variable we have in scope is $f$, but $f$ has type $(a \rightarrow b) \rightarrow q$ instead of type $q$. So it must have the shape of a function application $X_1 X_2$. In fact, we have a function $f$ that, when applied to an argument $X_2$ of type $a \rightarrow b$, results in $f X_2$ of type $q$. It's a reasonable guess that our final lambda term should have the shape $\lambda f^{(a \rightarrow b) \rightarrow q}. f X_2$, where the term $X_2$ inhabits the type $a \rightarrow b$.

How can we construct such an $X_2$? Well, this is a good time to get rid of the abbreviations $a,b$: we can see that $X_2$ has to inhabit the type $((p \rightarrow q) \rightarrow r) \rightarrow (p \rightarrow r) \rightarrow r$. This is a function type, so it's a reasonable guess that $X_2$ should have the shape $\lambda g^{(p\rightarrow q) \rightarrow r}. \lambda h^{p \rightarrow r}. X_3$ for some term $X_3$ that inhabits the type $r$.

This type $r$ is not a function type, so $X_3$ will not begin with a lambda. It's either a single bound variable in the current scope, or a function application $X_4 X_5$. Let's take stock of the variables we have in scope:

f: (((p -> q) -> r) -> (p -> r) -> r) -> q
g: (p -> q) -> r
h: p -> r

We need something of type $r$, so none of these bound variables do the job immediately. Thus, we're looking to find a function application $X_4 X_5$, where $X_4$ should return something of type $r$. We have two such choices: $g$ or $h$. Which one should we go with?

Well, if we go with $h$, we'll need to choose $X_5$ to have type $p$. This looks fairly difficult, since we have nothing of type $p$ in scope.

At first glance, choosing $g$ would lead to a similar problem: we'd need to choose $X_5$ to have type $p \rightarrow q$ in this case, and we have nothing of type $p \rightarrow q$. However, we do have a lead: the type of $f$ at least ends in $q$, even though it's quite a bit more complicated than what we need. So $g$ looks a bit more promising. Let's go with it, and fix $X_4$ as $g$!

All that's left is to construct an $X_5$ of type $p \rightarrow q$. It will probably have the shape $\lambda i^p. X_6$ for some $X_6$ of type $q$.

What should $X_6$ look like? Since $q$ is not a function type, it should either be an application, or a single variable. Let's take stock of our variables again:

f: (((p -> q) -> r) -> (p -> r) -> r) -> q
g: (p -> q) -> r
h: p -> r
i: p

Well, none of our variables have the right type $q$ at this point, so we have to use a function type again. The only function that returns something of type $q$ is $f$, so we'll go with the shape $f X_7$, where $X_7$ has the type $((p \rightarrow q) \rightarrow r) \rightarrow (p \rightarrow r) \rightarrow r$.

This looks bad at first: we seemingly came back to where we started when we attempted to construct $X$ itself. But in fact the situation is not quite identical: when we started out, we only had one variable in scope, and now we have four! We need to construct a function that has type $((p \rightarrow q) \rightarrow r) \rightarrow (p \rightarrow r) \rightarrow r$, and in this new context, we can do that quite easily. Why? Because if we glance at the four variables above, we see that we can construct something of type $r$, namely the application $h i$. And since we can construct something of type $r$, we can construct functions of any type $x \rightarrow y \rightarrow r$, simply as $\lambda j^x. \lambda k^y. h i$.

At this point we can set $X_7$ to $\lambda j. \lambda k. h i$, which has the required type $((p \rightarrow q) \rightarrow r) \rightarrow (p \rightarrow r) \rightarrow r$.

Since $X_6$ had the shape $f X_7$, we now know that it is $f(\lambda j. \lambda k. h i)$.

And $X_5$ has the shape $\lambda i^p. X_6$, which is now $\lambda i^p. f(\lambda j. \lambda k. h i)$.

We keep moving back: $X_3$ was $g X_5$, which is now $g (\lambda i^p. f(\lambda j. \lambda k. h i))$, $X_2$ was $\lambda g^{(p\rightarrow q) \rightarrow r}. \lambda h^{p \rightarrow r}. X_3$, which is now $\lambda g^{(p\rightarrow q) \rightarrow r}. \lambda h^{p \rightarrow r}. g (\lambda i^p. f(\lambda j. \lambda k. h i))$, and our final term had the shape $\lambda f^{(a \rightarrow b) \rightarrow q}. f X_2$, which now becomes $$\lambda f^{(a \rightarrow b) \rightarrow q}. f (\lambda g^{(p\rightarrow q) \rightarrow r}. \lambda h^{p \rightarrow r}. g (\lambda i^p. f(\lambda j. \lambda k. h i))),$$ a closed lambda term of type $((a \rightarrow b) \rightarrow q) \rightarrow q$, the one that we sought.

II. How could we summarize the heuristics that we followed to obtain the solution in the previous section?

1. Let the types guide you! When you're trying to construct a term of function type $a \rightarrow b$, you'll almost always want to start with a $\lambda x^a$.
2. Take stock of what you have in scope. When you're trying to construct a term of non-function type $b$, you cannot start with a $\lambda$, so take stock of the variables you have, and see if you can combine them using applications to get something of type $b$.
3. When you have multiple choices, use common sense to try the most promising, least redundant ones first. E.g. if you're looking for something of shape $X_1 X_2$, you don't have to consider the shape $\lambda x.X_3$ for $X_1$. If it had that shape, you could perform the $\beta$-reduction/substitution and have $X_3[x:=X_2]$ instead.

The rest is practice. The problem above is quite difficult, so I advise you start practicing much simpler ones, until you get the method down. E.g. can you apply the method to inhabit the types below:

1. $(A \rightarrow A \rightarrow B) \rightarrow A \rightarrow B$;
2. $(A \rightarrow (B \rightarrow A) \rightarrow B) \rightarrow A \rightarrow B$;
3. $((B \rightarrow A) \rightarrow B) \rightarrow ((B \rightarrow B) \rightarrow A) \rightarrow B$?

III. Is there an algorithm for deciding when a type of the simply-typed lambda calculus is inhabited?

Yes! Through the Curry-Howard isomorphism, terms of type $T$ in the simply-typed lambda calculus correspond to proofs of the proposition $T$ in the implication-only fragment of Intuitionistic Propositional Logic.

Provability in intuitionistic propositional logic is decidable: in fact, there are algorithms which find such proofs. One of the best such algorithms is proof search in Dyckhoff's LJT sequent calculus. You can learn more about sequent calculi on the Logitext website, and use their online implementation of the LJT calculus to decide which types have inhabitants. At this stage, this won't help you find inhabitants directly: your book does not fully cover how to translate between sequent calculus proofs, natural deduction proofs and lambda calculus terms until Chapter 7.