The derivation rules for \(\lambda \underline{\omega}\) are noticably more complex than we've seen so far because the generation of types is more complex. In \(\lambda\rightarrow\), there was no generation of types: the universe of types was fixed a priori as \(\mathbb{T}\). In \(\lambda 2\), things got slightly more complex, and we had to update the (var) rule to require that types be declared in a context before use (i.e. an \(\alpha:\ast\) had to precede an \(x:\alpha\)).

In \(\lambda \underline{\omega}\) the (var) rule becomes more complex again, and we're going to see that it requires some help. Let's work a motivational example: surely, we should have \(\{\alpha:\ast,x:\alpha\}\vdash x:\alpha\) be derivable. Assuming a (var) rule of some form, we would expect that a derviation in tree format might look like this:

Well, a derivation rule that gets us to line (3) would have to look like:

\begin{equation} \textbf{(var-v0) } \frac{\Gamma\vdash A:*}{\Gamma,x:A\vdash x:A}\text{ if }x\not\in\Gamma \end{equation}

However, a derivation rule that gets us to line (2) would have to look like:

\begin{equation} \textbf{(var-v1) } \frac{\Gamma\vdash A:\square}{\Gamma,x:A\vdash x:A}\text{ if }x\not\in\Gamma \end{equation}

If we let \(x\) be either a term variable or a type variable, these two rules differ only by the kind of A in the upper right, so we can write a unified version if we define \(s\) to be one of \(\{\ast,\square\}\). Since this is going to come up again, let's refer to the set \(\{\ast,\square\}\) as sorts (as in "∗ is a sort", or "\(\square\) is a sort."), and write:

\begin{equation} \textbf{(var) } \frac{\Gamma\vdash A:s}{\Gamma,x:A\vdash x:A}\text{ if }x\not\in\Gamma \end{equation}

The intuition here is: if we have a context Γ in which \(A\) is well-formed, we can append \(x:A\) to Γ & derive \(x:A\) from our new context.

But what about that first conclusion on line (2)– we need the premise that in the empty context, \(\ast\) is \(\square\) and we have no obvious way to obtain it. We add it to the system as a derivation rule:

\begin{equation} \textbf{(sort) } \emptyset\vdash\ast:\square \end{equation}

OK– now we have our desired derivation:

but a little pressure-testing shows that we're still not there, yet. We can derive none of the following obviously true judgements using just (var) & (sort):

1. \(\alpha:\ast,x:\alpha\vdash\alpha:\ast\)
2. \(\alpha:\ast,\beta:\ast\vdash\alpha:\ast\)
3. \(\alpha:\ast,\beta:\ast\vdash\beta:\ast\)

Turns out, we also need to add a rule stating that weakening a context by adding statements to it doesn't reduce what can be derived from that context:

\begin{equation} \textbf{(weak) } \frac{\Gamma\vdash A:B \quad \Gamma\vdash C:s}{\Gamma,x:C\vdash A:B}\text{ if }x\not\in\Gamma \end{equation}

In other words, if we've already derived that \(\Gamma\vdash A:B\), an \(C\) is well-formed (in Γ), we can append a declaration that \(x:C\) to Γ, and not affect what we already new about \(A\). Armed with (sort), we can now derive 1) in the list above:

The reader should note here that we're using the same judgement twice in our invocation of the (weak) rule: the first (left-hand) use "carries" the knowledge we want to preserve (i.e. that α is ∗), and the second is the lever that lets us introduce a new declaration of type α.

Let's take a look at the second & third judgements. This may seem pedantic (and available in TTFP), but as I moved on to even more complex derivations in \(\lambda P\) (the subject of the next post in this series) I found it to be important to have good intuitions around these variants of (var) & (weak). I think of this particular pattern as "adding at the next level" to what we already have in a judgement.

Let's show \(\{\alpha:\ast,\beta:\ast\}\vdash\alpha:\ast\):

Here, in the conclusion on the upper-right hand corner of the derivation, we've used that pattern to derive that ∗ is \(\square\) in the context \(\{\alpha:\ast\}\), which is surprisingly useful, as we see in the final conclusion: it lets us append another type declaration to the context while preserving what we know in the left-hand premise.

In comparison, our derivation of 3) is easy:

Finally, Nederpelt & Geuvers combine these three derivations into one in the flag format. The reader is encouraged to work through this for him or herself because the derivations are only going to get more complex going forward:

To be honest, I found it a bit tough to translate between the two formats on this one, I think because the authors mark the conclusions with which rule was used to derive them, whereas I think of the derivation rules in \(\lambda \underline{\omega}\) as permitting both those conclusions and changes to the contexts that preceed them.

That said, line (4) represents the judgement \(\{\alpha:\ast,x:\alpha\vdash\alpha:\ast\}\) (i.e. judgement 1) in our list), line (6) represents the judgement \(\{\alpha:\ast,\beta:\ast\vdash\alpha:\ast\}\) and line (7) \(\{\alpha:\ast,\beta:\ast\vdash\beta:\ast\}\) (i.e. judgements 2) & 3)).

We first saw a formation rule in \(\lambda 2\), again because the set of terms was fixed a priori in \(\lambda\rightarrow\). There, the formation rule governed the addition of types to the context, albeit only by requiring that they were in \(\mathbb{T}2\). Here again, that process becomes more complex in \(\lambda \underline{\omega}\): we need to be sure that new types are well-formed:

\begin{equation} \textbf{(form) } \frac{\Gamma\vdash A:s \enspace \Gamma\vdash B:s}{\Gamma\vdash A\rightarrow B} \end{equation}

where again \(s\) denotes either sort ∗ or \(\square\). This is what allows us to add e.g. \(\alpha\rightarrow\beta\) as a type to the context, assuming \(\alpha\) & \(\beta\) have been added as types previously (and \(\ast\rightarrow\ast\) analagously).

In addition, we'd like our typing to respect β-conversion at the type level. Even though we haven't discussed it, β-reduction works in the natural way for types in \(\lambda \underline{\omega}\): \((\lambda\alpha:\ast.\alpha\rightarrow\alpha)\beta\rightarrow_{\beta}\beta\rightarrow\beta\), for instance. We would like to be able to derive \(\Gamma\vdash A:B^{\prime}\) when we know \(\Gamma\vdash A:B\) and \(B\equiv_{\beta}B^{\prime}\):

\begin{equation} \textbf{(conv) } \frac{\Gamma\vdash A:B \enspace \Gamma\vdash B^{\prime}:s}{\Gamma\vdash A:B^{\prime}}\text{ if }B\equiv_{\beta}B^{\prime} \end{equation}

These two rules now operate at both the level of terms & types, but I trust the generalizations will be obvious:

\begin{align} &\textbf{(appl) } &\frac{\Gamma\vdash M:A\rightarrow B \enspace \Gamma\vdash N:A}{\Gamma\vdash MN:B}\nonumber\\ \nonumber\\ &\textbf{(abst) } &\frac{\Gamma,x:A\vdash M:B \enspace \Gamma\vdash A\rightarrow B:s}{\Gamma\vdash\lambda x:A.M:A\rightarrow B} \end{align}

For convenience, here are the seven derivation rules for \(\lambda \underline{\omega}\):

\begin{align} &\textbf{(sort) } &\emptyset\vdash\ast:\square \nonumber\\ \nonumber\\ &\textbf{(var) } &\frac{\Gamma\vdash A:s}{\Gamma,x:A\vdash x:A}\text{ if }x\not\in\Gamma \nonumber\\ \nonumber\\ &\textbf{(weak) } &\frac{\Gamma\vdash A:B \enspace \Gamma\vdash C:s}{\Gamma,x:C\vdash A:B}\text{ if }x\not\in\Gamma \nonumber\\ \nonumber\\ &\textbf{(form) } &\frac{\Gamma\vdash A:s \enspace \Gamma\vdash B:s}{\Gamma\vdash A\rightarrow B} \nonumber\\ \nonumber\\ &\textbf{(appl) } &\frac{\Gamma\vdash M:A\rightarrow B \enspace \Gamma\vdash N:A}{\Gamma\vdash MN:B}\nonumber\\ \nonumber\\ &\textbf{(abst) } &\frac{\Gamma,x:A\vdash M:B \enspace \Gamma\vdash A\rightarrow B:s}{\Gamma\vdash\lambda x:A.M:A\rightarrow B} \nonumber\\ &\textbf{(conv) } &\frac{\Gamma\vdash A:B \enspace \Gamma\vdash B^{\prime}:s}{\Gamma\vdash A:B^{\prime}}\text{ if }B\equiv_{\beta}B^{\prime} \end{align}

Let's work an example (this is execise 4.5 in TTFP)– let's validate the judgement

\begin{equation} \alpha:\ast,x:\alpha\vdash\lambda y:\alpha.x:(\lambda\beta:\ast.\beta\rightarrow\beta)\alpha \end{equation}

So this is obviously true: the term \(\lambda y:\alpha.x\) has type \(\alpha\rightarrow\alpha\) in a context in which \(x:\alpha\), and \((\lambda\beta:\ast.\beta\rightarrow\beta)\alpha\rightarrow_{\beta}\alpha\rightarrow\alpha\). The question is: how to derive it?

Well, we can see a few things immediately:

As an aside, I've taken a liberty with the step on line (4)– as stated, the weakening rule only allows the newly-added term (to the context) to be of kind ∗ or \(\square\), and I'm adding the term \(y:\alpha\). I have an e-mail out to the author & will update if I hear anything back. I the meantime, I'm not terribly worried since this seems "morally" correct– weakening a context should preserve things we already know.

We know that the type of the term of \(\lambda y:\alpha.x\) on line (5) is β-equivalent to that on line (7), so what do we have to show in order to set ourselves up for an application of (conv)? Well, if we interpret \(B^{\prime}\) as \((\lambda y:\beta:\ast.\beta\rightarrow\beta)\alpha\), we need to show that that type is well-formed in \(\lambda \underline{\omega}\)… but that term can easily be built-up in the familiar manner; it's just that we're operating on types instead of values now: