15 Properties

The important properties of the simply-typed lambda calculus that are proved in this chapter show that types behave in a useful way with respect to evaluation. The progress theorem states that a closed, well-typed term is either a value or can take a step. The preservation theorem states that in the latter case, the type before a step is the same as the type after the step. Together, these theorems show that "well-typed terms do not get stuck"; if evaluation of a term terminates, it terminates in a value of the same type. At the end of the file, we put these two theorems together to provide an evaluator.

These proofs are larger and more intricate than the ones we’ve seen so far, though amazingly enough, one can develop them by livecoding without too much trouble, knowing where one is at all times, with readable proofs. Unfortunately, Agda (like Coq) requires all helper functions to be at least declared before proofs that use them. So, when looking at a completed development such as shown in PLFA, we start with helper functions whose utility is not yet apparent. To deal with this inversion, let’s start by sketching the main results and how they might be proved, and see what issues might give rise to helpers. It’s important to keep the big picture in mind at all times, and perhaps this sketch will help.

The premise of the progress theorem is that we have a term that can be typed in the empty context (thus it is closed). To make the proof more readable, PLFA introduces the inductive datatype Progress, which wraps up either a proof that a term is a value or a proof that it can step. The conclusion of the theorem is that we have Progress for this term. The proof is by induction on the typing derivation of the term (which is like derivation on the term structure itself, but with more helpful information). The cases where the top-level typing constructor is ⊢ƛ or ⊢zero are easiest, as the terms involved are clearly values. For an application L · M, we need to recursively apply the theorem (use induction) on L and possibly M as well. If one of these steps, then by the corresponding xi-rule, the application steps. If both are values, then the typing rule tells us that L has a function type; we need a helper theorem to conclude that it’s a lambda, after which we can show that the application steps using a beta-rule.

This motivates the main helper for the progress theorem, called the canonical lemma, which characterizes values and their types. The other cases in the progress theorem use the same ideas.

The premises of the preservation theorem are that we have a closed, well-typed term, and a step that it takes. We want to show that the result of the step has the same type. The two premises are not independent; the top-level typing rule used will restrict the stepping rule, and vice-versa. The two categories of stepping rules are xi-rules and beta-rules. If a xi-rule is used, we can use recursion/induction on the subterm that is rewritten; if a beta-rule is used, then substitution takes place in the step (except for β-zero).

This motivates the substitution lemma, which says that substitution preserves types. What does this mean, exactly? If we want to do the substitution \(N [ x ~\colon = V ]\) in a beta-rule, then \(x\) is free in \(N\), and \(V\) can be typed as some type \(A\) in the empty context. \(N\) can be typed as some type \(B\) in a context that includes a type for \(x\) (which should be \(A\)). Since substitution is recursively defined, and several binders may have been pulled off, there could be other free variables in \(N\). So we have to postulate a context \(Γ\) such that \(N\) can be typed as \(B\) in context \(Γ, x\colon A\), and the conclusion of the substitution lemma should be that \(N [ x ~\colon = V ]\) can be typed as \(B\) in context \(Γ\).

The implementation of substitution does no recursion in the case of zero and variables. When the variable we arrive at is the same as the one being substituted for, we need to type it as \(A\) in the current context, knowing it can be typed as \(A\) in the empty context. This is called "weakening", and is a helper theorem.

When substitution is recursive, the substitution lemma is also recursive. Substitution involves terms and not types, but in the substitution lemma, there is an associated type judgment which involves a context. When the recursion passes over a binder, a variable-type binding is added to the context, which complicates the proof. Consider the lambda case (mu, and the case construct for naturals, are handled similarly).

If the variable of the lambda is the same as the one being substituted, then substitution stops at this point. But the body of the lambda is typed using a new type for the variable, added to the context and shadowing the old type. That old type needs to be removed in order to be able to build the judgment needed for the lemma recursion. So a "drop" helper theorem is needed, which says that a shadowed variable can be removed.

If the variable of the lambda is different than the one being substituted for, then substitution continues into the body. But the lambda variable and its type are added to the context in front of the binding for the variable being substituted for, which needs to be at the end to build the judgment for the lemma recursion. So a "swap" helper theorem is needed, which says that two different variables in a context can be swapped.

We could prove each of these three helper lemmas (weakening, dropping, swapping) separately, but we would discover that the proofs look very similar. (TaPL has them as separate lemmas, but the proofs shown are little more than the statement "by induction".) It’s better to do one proof (as done in SF; called "rename" in PLFA) and then derive these as corollaries. Each of the lemmas wants to take a type judgment in a particular context and extend it to a slightly different context where the differences (entries not used, entries in a different location, shadowed variables) are irrelevant to the particular judgment.

Here’s the general framework into which these can be fit. If we have two contexts Γ and Δ such that every successful lookup in Γ can be mapped (constructively) to a successful lookup in Δ with the same result, then type judgments can also be mapped. The lemmas are then special cases with particular mappings.

The general rename lemma is proved by induction on the type judgment being remapped, but again, in the case of binders, the context changes. A variable binding added to Γ needs to be added to Δ in order to construct the mapping of the type judgment. But in order to use recursion/induction in the proof of the renaming lemma, we need to be able to lift the lookup mapping from Γ to Δ by adding the new variable binding to both. This is the last helper, the extension lemma ext (which of course shows up early in the file’s approach to preservation).

Having proved the renaming lemma, the three corollaries we need follow by constructing the appropriate mappings.

Now that we understand where the helpers would arise in a derivation from scratch, we can work through the proofs of each of the helpers and main theorems.

15.1 Values do not reduce

The current version of Agda will not generate the absurd cases here and in the Canonical section which immediately follows, so the proofs look a little cleaner.

15.2 Progress

The main theorem is not too hard to prove given the helpers, but we can’t do it quite as automatically and quickly as with some earlier theorems. We have to, for each case, think about what is going on. Agda will not make the choice of step or done for us, and it can often not tell what the evidence for a step is. We have to know what we’re doing, and remember which helpers to use. The Emacs Agda command C-c C-o can be of assistance. Applied to the name of a module (which includes datatypes and record types), it will generate a brief description.

15.3 Prelude to preservation

The Emacs Agda command C-c C-h is useful for the three special cases (weaken, drop, swap) that we need from the general rename theorem. If the name of a helper function and possibly some arguments are typed into a hole, followed by this command, Agda mode responds with a type signature, and copies it into the Emacs kill ring and system clipboard so that it can be yanked/pasted.

This command (like others in Agda mode) can occasionally do the wrong thing in a complex situation. This will happen in the swap lemma, where there is an additional argument (the proof that the two variables are different). The helper command generates implicit arguments that shadow the variables and make the proof useless. Some manual editing is needed to get things back on track.

The asciicast below contains an example of deriving one of the helpers; I’ve left the others undone in the starter in case you want to practice. For subst, I’ve only done a few of the cases to give you an idea. Again, you might consider doing some more of them yourself. When watching, or doing it yourself, you can see where in the main proof the need for the helpers arises. Remember that we’re using a more recent library version of Dec than PLFA. Refer back to the end of the Decidable notes if necessary.

The implementations of rename and preserve are fairly straightforward proofs by induction.

15.4 Evaluation

As a particularly nice use of the "proofs are programs" idea, we can use the progress and preservation theorems to write an evaluator, provided that we have a typing judgment for the term we wish to evaluate. The progress theorem either says we’re done or we can take a step (and constructively provides the resulting term); the preservation theorem gives us the typing judgment on that term that we need to repeat the process anew. We can’t, however, say "repeat until done", because Agda won’t be able to see that this process terminates, and in fact it might not, since, as we’ve seen, we can write infinite loops in the source language.

I’ve commented out the long trace in the local code because it can lead to slowdowns in Emacs. Compiling the file on the command line seems to help.

15.5 Reduction is deterministic

Wadler has expressed frustration with this proof, which is fairly straightforward, but a bit tedious. You would think that the impossible cases could be taken care of, but it is not so simple. SF handles it by defining a custom automation, and Agda does have facilities that might do something similar, but this seems too advanced for an introductory course. Perhaps we should be grateful for a system where eighteen lines of code is seen as excessive.