In this chapter, we develop the fundamental theory of the Simply Typed Lambda Calculus -- in particular, the type safety theorem.
As we saw for the simple calculus in the Types chapter, the first step in establishing basic properties of reduction and types is to identify the possible canonical forms (i.e., well-typed closed values) belonging to each type. For Bool, these are the boolean values tru and fls; for arrow types, they are lambda-abstractions.
The progress theorem tells us that closed, well-typed terms are not stuck: either a well-typed term is a value, or it can take a reduction step. The proof is a relatively straightforward extension of the progress proof we saw in the Types chapter. We give the proof in English first, then the formal version.
Proof: By induction on the derivation of |- t \in T.
Show that progress can also be proved by induction on terms instead of induction on typing derivations.
The other half of the type soundness property is the preservation of types during reduction. For this part, we'll need to develop some technical machinery for reasoning about variables and substitution. Working from top to bottom (from the high-level property we are actually interested in to the lowest-level technical lemmas that are needed by various cases of the more interesting proofs), the story goes like this:
inessential changesto the context Gamma -- in particular, changes that do not affect any of the free variables of the term. And finally, for this, we need a careful definition of...
To make Coq happy, of course, we need to formalize the story in the opposite order...
A variable x appears free in a term t if t contains some occurrence of x that is not under an abstraction labeled x. For example:
Formally:
The free variables of a term are just the variables that appear free in it. A term with no free variables is said to be closed.
An open term is one that may contain free variables. (I.e., every
term is an open term; the closed terms are a subset of the open ones.
Open
precisely means possibly containing free variables.
)
In the space below, write out the rules of the appears_free_in relation in informal inference-rule notation. (Use whatever notational conventions you like -- the point of the exercise is just for you to think a bit about the meaning of each rule.) Although this is a rather low-level, technical definition, understanding it is crucial to understanding substitution and its properties, which are really the crux of the lambda-calculus.
To prove that substitution preserves typing, we first need a technical lemma connecting free variables and typing contexts: If a variable x appears free in a term t, and if we know t is well typed in context Gamma, then it must be the case that Gamma assigns a type to x.
Proof: We show, by induction on the proof that x appears free in t, that, for all contexts Gamma, if t is well typed under Gamma, then Gamma assigns some type to x.
From the free_in_context lemma, it immediately follows that any term t that is well typed in the empty context is closed (it has no free variables).
Sometimes, when we have a proof of some typing relation Gamma |- t \in T, we will need to replace Gamma by a different context Gamma'. When is it safe to do this? Intuitively, it must at least be the case that Gamma' assigns the same types as Gamma to all the variables that appear free in t. In fact, this is the only condition that is needed.
Proof: By induction on the derivation of Gamma |- t \in T.
By T_Abs, it suffices to show that y|->T11; Gamma' |- t12 \in T12. By the IH (setting Gamma'' = y|->T11;Gamma'), it suffices to show that y|->T11;Gamma and y|->T11;Gamma' agree on all the variables that appear free in t12.
Any variable occurring free in t12 must be either y or some other variable. y|->T11; Gamma and y|->T11; Gamma' clearly agree on y. Otherwise, note that any variable other than y that occurs free in t12 also occurs free in t = \y:T11. t12, and by assumption Gamma and Gamma' agree on all such variables; hence so do y|->T11; Gamma and y|->T11; Gamma'.
Now we come to the conceptual heart of the proof that reduction preserves types -- namely, the observation that substitution preserves types.
Formally, the so-called substitution lemma says this: Suppose we have a term t with a free variable x, and suppose we've assigned a type T to t under the assumption that x has some type U. Also, suppose that we have some other term v and that we've shown that v has type U. Then, since v satisfies the assumption we made about x when typing t, we can substitute v for each of the occurrences of x in t and obtain a new term that still has type T.
Lemma: If x|->U; Gamma |- t \in T and |- v \in U, then Gamma |- [x:=v]t \in T.
One technical subtlety in the statement of the lemma is that we assume v has type U in the empty context -- in other words, we assume v is closed. This assumption considerably simplifies the T_Abs case of the proof (compared to assuming Gamma |- v \in U, which would be the other reasonable assumption at this point) because the context invariance lemma then tells us that v has type U in any context at all -- we don't have to worry about free variables in v clashing with the variable being introduced into the context by T_Abs.
The substitution lemma can be viewed as a kind of commutation
property.
Intuitively, it says that substitution and typing can
be done in either order: we can either assign types to the terms
t and v separately (under suitable contexts) and then combine
them using substitution, or we can substitute first and then
assign a type to [x:=v] t -- the result is the same either
way.
Proof: We show, by induction on t, that for all T and Gamma, if x|->U; Gamma |- t \in T and |- v \in U, then Gamma |- [x:=v]t \in T.
The substitution in the conclusion behaves differently depending on whether x and y are the same variable.
First, suppose x = y. Then, by the definition of substitution, [x:=v]t = t, so we just need to show Gamma |- t \in T. But we know x|->U; Gamma |- t \in T, and, since y does not appear free in \y:T11. t12, the context invariance lemma yields Gamma |- t \in T.
Second, suppose x <> y. We know x|->U; y|->T11; Gamma |- t12 \in T12 by inversion of the typing relation, from which y|->T11; x|->U; Gamma |- t12 \in T12 follows by the context invariance lemma, so the IH applies, giving us y|->T11; Gamma |- [x:=v]t12 \in T12. By T_Abs, Gamma |- \y:T11. [x:=v]t12 \in T11->T12, and by the definition of substitution (noting that x <> y), Gamma |- \y:T11. [x:=v]t12 \in T11->T12 as required.
Technical note: This proof is a rare case where an induction on
terms, rather than typing derivations, yields a simpler argument.
The reason for this is that the assumption x|->U; Gamma |- t
\in T is not completely generic, in the sense that one of the
slots
in the typing relation -- namely the context -- is not
just a variable, and this means that Coq's native induction tactic
does not give us the induction hypothesis that we want. It is
possible to work around this, but the needed generalization is a
little tricky. The term t, on the other hand, is completely
generic.
We now have the tools we need to prove preservation: if a closed term t has type T and takes a step to t', then t' is also a closed term with type T. In other words, the small-step reduction relation preserves types.
Proof: By induction on the derivation of |- t \in T.
There are again three subcases to consider, depending on how t steps.
An exercise in the Types chapter asked about the subject expansion property for the simple language of arithmetic and boolean expressions. This property did not hold for that language, and it also fails for STLC. That is, it is not always the case that, if t --> t' and has_type t' T, then empty |- t \in T. Show this by giving a counter-example that does not involve conditionals.
You can state your counterexample informally in words, with a brief explanation.
Put progress and preservation together and show that a well-typed term can never reach a stuck state.
Another nice property of the STLC is that types are unique: a given term (in a given context) has at most one type.
Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus (as Coq theorems). You can write Admitted for the proofs.
Suppose we add a new term zap with the following reduction rule
and the following typing rule:
Which of the following properties of the STLC remain true in
the presence of these rules? For each property, write either
remains true
or becomes false.
If a property becomes
false, give a counterexample.
Suppose instead that we add a new term foo with the following reduction rules:
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
remains true
or else becomes false.
If a property becomes
false, give a counterexample.
Suppose instead that we remove the rule ST_App1 from the step
relation. Which of the following properties of the STLC remain
true in the presence of this rule? For each one, write either
remains true
or else becomes false.
If a property becomes
false, give a counterexample.
Suppose instead that we add the following new rule to the reduction relation:
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
remains true
or else becomes false.
If a property becomes
false, give a counterexample.
Suppose instead that we add the following new rule to the typing relation:
Gamma |- t1 \in Bool->Bool->Bool Gamma |- t2 \in Bool
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
remains true
or else becomes false.
If a property becomes
false, give a counterexample.
Suppose instead that we add the following new rule to the typing relation:
Gamma |- t1 \in Bool Gamma |- t2 \in Bool
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
remains true
or else becomes false.
If a property becomes
false, give a counterexample.
Suppose we add the following new rule to the typing relation of the STLC:
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
remains true
or else becomes false.
If a property becomes
false, give a counterexample.
To see how the STLC might function as the core of a real programming language, let's extend it with a concrete base type of numbers and some constants and primitive operators.
To types, we add a base type of natural numbers (and remove booleans, for brevity).
To terms, we add natural number constants, along with successor, predecessor, multiplication, and zero-testing.
Finish formalizing the definition and properties of the STLC extended with arithmetic. This is a longer exercise. Specifically:
1. Copy the core definitions for STLC that we went through, as well as the key lemmas and theorems, and paste them into the file at this point. Do not copy examples, exercises, etc. (In particular, make sure you don't copy any of the comments at the end of exercises, to avoid confusing the autograder.)
You should copy over five definitions:
And five theorems, with their proofs:
It will be helpful to also copy over Reserved Notation
,
Notation
, and Hint Constructors
for these things.
2. Edit and extend the five definitions (subst, value, step, has_type, and appears_free_in) so they are appropriate for the new STLC extended with arithmetic.
3. Extend the proofs of all the five properties of the original STLC to deal with the new syntactic forms. Make sure Coq accepts the whole file.