This optional chapter is based on [Pierce 2002] Chapter 12, and [Ahmed 2015]. It may be useful to look at those references, since they include some explanations and informal proofs that are not repeated here. In this chapter, we consider another fundamental theoretical property of the simply typed lambda-calculus: the fact that the evaluation of a well-typed program is guaranteed to halt in a finite number of steps---i.e., every well-typed term is normalizable. Unlike the type-safety properties we have considered so far, the normalization property does not extend to full-blown programming languages, because these languages nearly always include features, such as general recursion (see the MoreStlc chapter) or recursive types, that can be used to write nonterminating programs. However, the issue of normalization reappears at the level of types when we consider the metatheory of polymorphic versions of the lambda calculus such as System F-omega: in this system, the language of types effectively contains a copy of the simply typed lambda-calculus, and the termination of the typechecking algorithm thus hinges on the fact that a "normalization" operation on type expressions is guaranteed to terminate. Another reason for studying normalization proofs is that they are some of the most beautiful---and mind-blowing---mathematics to be found in the type theory literature, often (as here) involving the fundamental proof technique of logical relations. To give readers more exposure to this proof technique, we also use it to develop an alternative proof of type safety at the end of this chapter. The calculus we shall consider here is the simply typed lambda-calculus over a single base type bool and with pairs. We'll give most details of the development for the basic lambda-calculus terms treating bool as an uninterpreted base type, and leave the extension to the boolean operators and pairs to the reader. Even for the base calculus, normalization is not trivial to prove, since each reduction of a term can duplicate redexes in subterms.

Exercise: 2 stars, standard (norm_fail)

Where do we fail if we attempt to prove normalization by a straightforward induction on the size of a well-typed term?

The best ways to understand an intricate proof like this is are (1) to help fill it in and (2) to extend it. We've omitted some parts of the following development, including some proofs of lemmas and all the cases involving products and conditionals, and left them as exercises.

Language

We begin by repeating the definition of our STLC variant, which is similar to those in the MoreStlc chapter, plus supporting results including type preservation and step determinism. (We won't need progress.) You may just wish to skip down to the Normalization section...

Syntax and Operational Semantics

Substitution

Reduction

Aside: As a reminder, putting curly braces around one ore more parameters in a lemma statement means that the parameters are to be inferred from the remaining parameters. For example, in the above lemma, Rocq can infer t from the provided value t. This is entirely analogous to inference of type arguments in ordinary polymorphic functions, and it can remove clutter from explicit applications of the lemma. We use this style for most lemma statements in the remainder of this chapter.

Typing

Weakening

The weakening lemma is proved as in pure STLC.

Substitution

Preservation

Free Variables and Closed Terms

Determinism

To prove determinism, we introduce a helpful tactic that identifies cases in which a value takes a step and solves them using value__normal.

Normalization

Now for the actual normalization proof. Our goal is to prove that every well-typed term reduces to a normal form. In the terminology of Chapter Smallstep, we want to show normalizing step. In fact, it turns out to be convenient to prove something slightly stronger, namely that every well-typed term reduces to a value. This follows from the weaker property via progress (why?) but otherwise we don't need progress, and we didn't bother re-proving it above. Here's the key definition:

Exercise: 2 stars, standard (value_halts)

Complete the proof of the this simple but useful fact:

☐

Exercise: 3 stars, standard (step_preserves_halting)

Another useful and suggestive fact: the property of halting is preserved by taking a reduction step or "undoing" a reduction step. Complete the proof of this lemma. (The proof does not depend on the precise details of the step relation, but in one direction you will want to use value__normal and step_deterministic. The lemma might still be true for nondeterministic languages, but the proof would be harder!)

☐

First Proof Attempt

The normalization proof is quite complicated, and it requires several different kinds of auxiliary mechanisms. To understand the motivation for these, it is instructive to look at some failed proof attempts. First of all, let's try to prove normalization directly using just induction on the typing judgments. We wouldn't expect this to succeed, but it is useful to see just where it goes wrong.

The N relation

The key issue in the normalization proof (as in many proofs by induction) is finding a strong enough induction hypothesis. To this end, we begin by defining, for each type T, a set N_T of closed terms of type T, where N stands for "normalizing." We will specify these sets using a relation N and write N T t when t is in N_T. (The sets N_T are sometimes called saturated sets or reducibility candidates.) Here is the definition of N for the base language:

• N bool t iff t is a closed term of type bool and t halts in a value
• N (T₁ → T₂) t iff t is a closed term of type T₁ → T₂ and t halts in a value and, for any term s such that N T₁ s, we have N T₂ (t s).

This definition gives us the strengthened induction hypothesis that we need. Our primary goal is to show that all programs ---i.e., all closed terms of base type---halt. But closed terms of base type can contain subterms of functional type, so we need to know something about these as well. Moreover, it is not enough to know that these subterms halt, because the application of a normalized function to a normalized argument involves a substitution, which may enable more reduction steps. So we need a stronger condition for terms of functional type: not only should they halt themselves, but, when applied to halting arguments, they should yield halting results. We also have to define the predicate for any other types in the language---in our case, products. (Even though the cases of the proof attempt above that deal with products are not problematic, once we choose to introduce N to handle functions properly, we have to consider its interaction with all other types -- think about products of functions, for example.) This part of the N definition, and the subsequent proof cases that involve it, are left as an exercise for you. The form of N is characteristic of the logical relations proof technique. If we want to prove some property P of all closed terms of type A, we proceed by proving, by induction on types, that all terms of type A possess property P, all terms of type A→A preserve property P, all terms of type (A→A)->(A→A) preserve the property of preserving property P, and so on. We do this by defining a family of predicates, indexed by types. For the base type A, the predicate just enforces property P. For functional types, it says that the function should map values satisfying the property at the input type to values satisfying the property at the output type. A warning about terminology: "logical relations" refers to relations that are "logical" in a very special sense; "type-indexed inductive relations" might be a better name. In general, one can study logical relations between two or more terms, but here we are only considering single terms, so we should more properly say logical predicates. (Confusingly, since these predicates are indexed by types, they have the form of a relation between types and terms---but this is not a "logical" relation!) In addition to using the logical predicates technique to prove normalization, we will also apply it to give an alternative proof of type safety at the end of this chapter. See [Ahmed 2015] and [Mitchell 1996] for more details and applications of logical relations. When we come to formalize the definition of N in Rocq, we hit a problem. The most obvious formulation would be as a parameterized Inductive proposition like this:
      Inductive N : ty → tm → Prop :=
      | N_bool : ∀ b t, empty |-- t \in <{ Bool }> →
                      halts t →
                      N <{ Bool }> t
      | N_arrow : ∀ T₁ T₂ t, empty |-- t \in <{ T₁ → T₂ }> →
                      halts t →
                      (∀ s, N T₁ s → N T₂ <{t s}>) →
                      N <{ T₁ → T₂ }> t. Unfortunately, Rocq rejects this definition because it violates the strict positivity requirement for inductive definitions, which says that the type being defined must not occur to the left of an arrow in the type of a constructor argument. Here, it is the third argument to N_arrow, namely (∀ s, N T₁ s → N T₂ <{t s}>), and specifically the N T₁ s part, that violates this rule. (The outermost arrows separating the constructor arguments don't count when applying this rule; if they did, we could never have genuinely inductive properties at all!) The reason for the rule is that types defined with non-positive recursion can be used to build non-terminating functions, which as we know would be a disaster for Rocq's logical soundness. Even though the relation we want in this case might be perfectly innocent, Rocq still rejects it because it fails the positivity test. Fortunately, it turns out that we can define N using a Fixpoint, as shown below.

Exercise: 3 stars, standard, especially useful (N_products)

Fix the product case for this definition. Note 1: There is more than one valid way to do this; if your first attempt does not work out well when you come to the later proofs, try another! Note 2: you can skip this exercise until you are ready to start extending the later proofs.

As immediate consequences of this definition, we have that every element of every set N_T halts in a value and is closed with type T :

Membership in N_T Is Invariant Under Reduction

There's a deeper property of N_T that will turn out to be essential for the normalization proof, namely that membership in N_T is invariant under reduction. We will need this property in both directions, i.e., both to show that a term in N_T stays in N_T when it takes a forward step, and to show that any term that ends up in N_T after a step must have been in N_T to begin with. This means that, if any term in a chain of reductions is in N_T, then so is every other (well-typed) term. We will use this to establish that well-typed abstraction terms are indeed in N_T. This lemma is similar to the step_preserves_halting property we gave above, but the proof is more complicated because it makes fundamental use of the structure of types. Each direction of the lemma proceeds by induction on the type T. One requirement for staying in N_T is to stay in type T. In the forward direction, we get this from ordinary type preservation. The product case is left as an exercise for you.

Exercise: 3 stars, standard (step_preserves_N)

☐ The generalization to multiple steps is trivial:

In the reverse direction, we must add the fact that t has type T before stepping as an additional hypothesis, because subject expansion does not hold for this language (see StlcProp).

Exercise: 4 stars, standard, especially useful (step_preserves_N')

☐

Second Proof Attempt

Given the N_halts lemma, the task of proving normalization reduces to proving that every well-typed closed term of type T is a member of N_T. So let's attempt to prove that fact, again by induction on the typing derivation. We'll ultimately get stuck again, but the failed proof sketch will again be instructive. Unlike our previous attempt, the difficult part of this proof will be in the Abs case, while the App case will fall out directly from the definition of N_T.

Closing Multi-substitutions and Instantiations

The upshot of this failed proof attempt is that we need another generalization to state and prove typable_N properly. To recap: Since we are arguing by induction, the demonstration that a term \x : T₁, t₂ belongs to N_(T₁→T₂) should involve applying the induction hypothesis to show that t₂ belongs to N_T₂. But N_T₂ is defined to be a set of closed terms, while t₂ may contain x free, so this does not make sense. We resolve this problem by using a standard trick to suitably generalize the induction hypothesis: instead of proving a statement involving a closed term, we generalize it to cover all closed instances of an open term t that satisfy N. Informally, the statement of the lemma will look like this: If x₁:T₁,..xn:Tn |-- t : T and v₁,...,vn are values such that N T₁ v₁, N T₂ v₂, ..., N Tn vn, then N T ([x₁:=v₁][x₂:=v₂]...[xn:=vn]t). The proof will proceed by induction on the typing derivation x₁:T₁,..xn:Tn |-- t : T; the most interesting case will be the one for abstraction. However, before we can proceed to formalize the statement and proof of the lemma, we'll need to take a detour to build some (rather tedious) machinery to deal with the fact that we are performing multiple substitutions on term t and multiple extensions of the typing context. In particular, we must be precise about the order in which the substitutions occur and how they act on each other. Often these details are simply elided in informal paper proofs, but of course Rocq won't let us do that. Since here we are substituting closed terms, we don't need to worry about how one substitution might affect the term put in place by another. But we still do need to worry about the order of substitutions, because it is quite possible for the same variable name to appear multiple times among the x₁,...xn with different associated vi and Ti. To make everything precise, we will assume that typing context updates are performed from right to left, and multiple term substitutions are performed from left to right. To see that this is consistent, suppose we have a type assignment written as ...,y:Bool,...,y:Bool×Bool,... and a corresponding term substitution written as ...[y:=true]...[y:=(false,false)]...t. Since contexts are extended from right to left, the binding y:Bool hides the binding y:Bool×Bool; since substitutions are performed left to right, we do the substitution y:=true first, so the substitution y:=(false,false) has no effect. Substitution thus correctly preserves the type of the term. With these points in mind, the following definitions should make sense. A multi-substitution is the result of applying a list of substitutions, which we call an environment.

We need similar machinery to talk about repeated extension of a typing context using a list of (variable, type) pairs, which we call a type assignment. This is a more concrete representation of typing contexts than the partial maps (developed in Maps) that we have used up to this point. Representing maps as functions is appealingly simple for many purposes, but it has one major drawback: we cannot enumerate the domain of a map or perform induction over it. We can do induction over type assignments, and this turns out to be very useful.

A type assignment is readily converted into a typing context.

Finally, we describe the combination of a type assignment and a value environment that have the same domain and where corresponding type and value elements are related. We call this an instantiation. We parameterize the definition over an arbitrary type-indexed predicate R over closed terms, since many properties of instantiations don't depend on the specific choice of R. (This will allow us to reuse these definitions and properties on other logical predicates besides N later in the chapter.)

We now proceed to prove various properties of these definitions.

More Substitution Facts

First we need some additional lemmas on (ordinary) substitution. These will ultimately support lemmas about how single substitutions and multi-substitutions commute.

Exercise: 3 stars, standard, optional (vacuous_substitution)

Show that substituting for a variable which doesn't appear (free) has no effect.

☐ Substituting over a closed term has no effect.

Exercise: 3 stars, standard, optional (subst_not_afi)

Show that after substituting for a variable (with a closed term), that variable is no longer free. Proof is by induction on t.

☐ Substituting for the same variable twice has no effect.

Exercise: 3 stars, standard (swap_subst)

Changing the order of two (closed) substitutions for different variables has no effect. Complete the following proof.

☐

Properties of Multi-Substitutions

We can distribute msubst over subst provided that all substituted terms are closed. But we need to adjust the environment on the right-hand side to account for the possibility that the multi-substitution has duplicate variable names.

Exercise: 3 stars, standard, especially useful (msubst_subst)

Complete the following proof by induction on e. Hint: Use the lemmas about substitution proved above!

☐ Multi-substituting into a closed term has no effect.

Next come a series of easy lemmas characterizing how msubst distributes over each term form

Exercise: 2 stars, standard, especially useful (msubst_app)

☐ To complete the product cases of the main lemma below, you'll want similar results on all the other term constructors; the proofs are extremely similar to msubst_app.

General Properties of Instantiations

These don't depend on the underlying predicate R, and their proofs are straightforward.

Exercise: 3 stars, standard, especially useful (instantiation_msubst)

Applying the multi-substitution from an instantiation of R to a variable of type T yields a term t such that R T t.

☐

Exercise: 2 stars, standard (instantiation_env_closed)

The environment of an instantiation is always closed.

☐

Properties of N Instantiations

The key lemma about preservation of typing under substitution can be lifted to N-specific instantiations.

Exercise: 3 stars, standard (N_instantiation_preserves_typing)

☐

Congruence Lemmas on Multistep

Exercise: 2 stars, standard, especially useful (multistep_App2)

If we can reduce the right-hand side of an application, we can reduce the whole application.

☐ To complete the conditional and product cases of the main lemma below, you'll want similar lemmas; add them as the demand arises (the proofs are essentially identical).

Completed Proof using N

Exercise: 5 stars, standard, especially useful (typable_N)

At long last, the main lemma! The conditional and product cases are left for you.

☐ And the final theorem:

Type Safety via a Logical Predicate (Optional)

In this section, we further illustrate the proof technique of logical predicates by developing a proof of type safety for the simply typed lambda calculus which works rather differently than the standard one based on progress and preservation that we studied in StlcProp. In this alternative approach, we define a notion of semantic type safety as a logical predicate over terms that trivially implies the property that evaluation cannot get stuck. Then we prove that syntactically well-typed terms obey this predicate. The overall shape of this proof will be similar to that of the normalization proof. The logical predicate definition will again give us a stronger induction hypothesis for reasoning about functions (and booleans and pairs), although the technical details will be a bit different. To deal with open terms, we will be able to re-use the machinery of multi-substitutions and instantiations that we developed earlier in this chapter. Studying and completing the proof should give you an deeper understanding of how logical predicates (and, more generally, logical relations) can be used. In addition, this proof provides an introduction to the idea of "semantic typing," Semantic typing allows us to type many terms that don't have valid syntactic types; we'll see some examples below. And while the semantic safety proof for STLC is undoubtedly more complicated than the standard syntactic one using progress and preservation, it may generalize better to complex real-world languages, such as Rust, that support encapsulated unsafe computations (although these are beyond the scope of this chapter). We begin by giving a compact characterization of what it means for a term to be safe, namely that it never gets stuck.

First Proof Attempt

Our ultimate goal is to show that every syntactically well-typed term is safe in this sense. We know this can be done by alternating uses of progress and preservation, but it is once again instructive to attempt a direct inductive proof and see where the argument fails to go through. Actually, we'll temporarily assume we have separately proved preservation, so really this theorem can be viewed as an alternative to the progress lemma which deals with entire normalizing sequences of steps rather than just a single step at a time.