This material is taken verbatim from Software Foundations V4.0
Copyright (c) 2016
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
Require Import Maps
Require Import Smallstep
Require Import Types
The Simply Typed Lambda-Calculus
The simply typed lambda-calculus (STLC) is a tiny core
calculus embodying the key concept of functional abstraction
which shows up in pretty much every real-world programming
language in some form (functions, procedures, methods, etc.).
We will follow exactly the same pattern as in the previous chapter
when formalizing this calculus (syntax, small-step semantics,
typing rules) and its main properties (progress and preservation).
The new technical challenges arise from the mechanisms of
. It which will take some
work to deal with these.
The STLC is built on some collection of base types
booleans, numbers, strings, etc. The exact choice of base types
doesn't matter much — the construction of the language and its
theoretical properties work out the same no matter what we
choose — so for the sake of brevity let's take just Bool
the moment. At the end of the chapter we'll see how to add more
base types, and in later chapters we'll enrich the pure STLC with
other useful constructs like pairs, records, subtyping, and
Starting from boolean constants and conditionals, we add three
- function abstractions
This gives us the following collection of abstract syntax
constructors (written out first in informal BNF notation — we'll
formalize it below).
::= x variable
| t1 t2 application
| true constant true
| false constant false
| if t1 then t2 else t3 conditional
symbol in a function abstraction \x:T1.t2
written as a Greek letter "lambda" (hence the name of the
calculus). The variable x
is called the parameter
function; the term t2
is its body
. The annotation :T1
specifies the type of arguments that the function can be applied
- \x:Bool. x
The identity function for booleans.
- (\x:Bool. x) true
The identity function for booleans, applied to the boolean true.
- \x:Bool. if x then false else true
The boolean "not" function.
- \x:Bool. true
The constant function that takes every (boolean) argument to
- \x:Bool. \y:Bool. x
A two-argument function that takes two booleans and returns
the first one. (As in Coq, a two-argument function is really
a one-argument function whose body is also a one-argument
- (\x:Bool. \y:Bool. x) false true
A two-argument function that takes two booleans and returns
the first one, applied to the booleans false and true.
As in Coq, application associates to the left — i.e., this
expression is parsed as ((\x:Bool. \y:Bool. x) false) true.
- \f:Bool→Bool. f (f true)
A higher-order function that takes a function f (from
booleans to booleans) as an argument, applies f to true,
and applies f again to the result.
- (\f:Bool→Bool. f (f true)) (\x:Bool. false)
The same higher-order function, applied to the constantly
As the last several examples show, the STLC is a language of
functions: we can write down functions that take
other functions as arguments and/or return other functions as
The STLC doesn't provide any primitive syntax for defining named
functions — all functions are "anonymous." We'll see in chapter
that it is easy to add named functions to what we've
got — indeed, the fundamental naming and binding mechanisms are
exactly the same.
of the STLC include Bool
, which classifies the
boolean constants true
as well as more complex
computations that yield booleans, plus arrow types
- \x:Bool. false has type Bool→Bool
- \x:Bool. x has type Bool→Bool
- (\x:Bool. x) true has type Bool
- \x:Bool. \y:Bool. x has type Bool→Bool→Bool
(i.e., Bool → (Bool→Bool))
- (\x:Bool. \y:Bool. x) false has type Bool→Bool
- (\x:Bool. \y:Bool. x) false true has type Bool
We begin by formalizing the syntax of the STLC.
Note that an abstraction \x:T.t
(formally, tabs x T t
always annotated with the type T
of its parameter, in contrast
to Coq (and other functional languages like ML, Haskell, etc.),
which use type inference
to fill in missing annotations. We're
not considering type inference here.
Hint Unfold x
Hint Unfold y
Hint Unfold z
idB = \x:Bool. x
idBB = \x:Bool→Bool. x
idBBBB = \x:(Bool→Bool) → (Bool→Bool). x
k = \x:Bool. \y:Bool. x
notB = \x:Bool. if x then false else true
(We write these as Notations rather than Definitions to make
things easier for auto.)
To define the small-step semantics of STLC terms, we begin,
as always, by defining the set of values. Next, we define the
critical notions of free variables
, which are
used in the reduction rule for application expressions. And
finally we give the small-step relation itself.
To define the values of the STLC, we have a few cases to consider.
First, for the boolean part of the language, the situation is
are the only values. An if
expression is never a value.
Second, an application is clearly not a value: It represents a
function being invoked on some argument, which clearly still has
work left to do.
Third, for abstractions, we have a choice:
- We can say that \x:T. t1 is a value only when t1 is a
value — i.e., only if the function's body has been
reduced (as much as it can be without knowing what argument it
is going to be applied to).
- Or we can say that \x:T. t1 is always a value, no matter
whether t1 is one or not — in other words, we can say that
reduction stops at abstractions.
Coq, in its built-in functional programming langauge Gallina,
makes the first choice — for example,
⇒ 3 + 4)
yields fun x:bool ⇒ 7
Most real-world functional programming languages make the second
choice — reduction of a function's body only begins when the
function is actually applied to an argument. We also make the
second choice here.
Finally, we must consider what constitutes a complete
Intuitively, a "complete program" must not refer to any undefined
variables. We'll see shortly how to define the free
in a STLC term. A complete program is closed
— that is, it
contains no free variables.
Having made the choice not to reduce under abstractions, we don't
need to worry about whether variables are values, since we'll
always be reducing programs "from the outside in," and that means
relation will always be working with closed terms.
Now we come to the heart of the STLC: the operation of
substituting one term for a variable in another term. This
operation is used below to define the operational semantics of
function application, where we will need to substitute the
argument term for the function parameter in the function's body.
For example, we reduce
. if x then true else x
if false then true else false
by substituting false
for the parameter x
in the body of the
In general, we need to be able to substitute some given term s
for occurrences of some variable x
in another term t
informal discussions, this is usually written [x:=s]t
pronounced "substitute x
Here are some examples:
- [x:=true] (if x then x else false)
yields if true then true else false
- [x:=true] x yields true
- [x:=true] (if x then x else y) yields if true then true else y
- [x:=true] y yields y
- [x:=true] false yields false (vacuous substitution)
- [x:=true] (\y:Bool. if y then x else false)
yields \y:Bool. if y then true else false
- [x:=true] (\y:Bool. x) yields \y:Bool. true
- [x:=true] (\y:Bool. y) yields \y:Bool. y
- [x:=true] (\x:Bool. x) yields \x:Bool. x
The last example is very important: substituting x
yield \x:Bool. true
! The reason for
this is that the x
in the body of \x:Bool. x
abstraction: it is a new, local name that just happens to be
spelled the same as some global name x
Here is the definition, informally...
= y if x
) = \x
) = \y
]t12 if x
) = ([x
](if t1 then t2 else t3
... and formally:
: Substitution becomes trickier to define if we
consider the case where s
, the term being substituted for a
variable in some other term, may itself contain free variables.
Since we are only interested here in defining the step
on closed terms (i.e., terms like \x:Bool. x
binders for all of the variables they mention), we can avoid this
extra complexity here, but it must be dealt with when formalizing
Exercise: 3 stars (substi)
The definition that we gave above uses Coq's Fixpoint
to define substitution as a function
. Suppose, instead, we
wanted to define substitution as an inductive relation substi
We've begun the definition by providing the Inductive
one of the constructors; your job is to fill in the rest of the
constructors and prove that the relation you've defined coincides
with the function given above.
The small-step reduction relation for STLC now follows the
same pattern as the ones we have seen before. Intuitively, to
reduce a function application, we first reduce its left-hand
side (the function) until it becomes an abstraction; then we
reduce its right-hand side (the argument) until it is also a
value; and finally we substitute the argument for the bound
variable in the body of the abstraction. This last rule, written
) v2 ⇒
is traditionally called "beta-reduction".
|(\x:T.t12) v2 ⇒ [x:=v2]t12
|t1 ⇒ t1'
|t1 t2 ⇒ t1' t2
|t2 ⇒ t2'
|v1 t2 ⇒ v1 t2'
... plus the usual rules for booleans:
|(if true then t1 else t2) ⇒ t1
|(if false then t1 else t2) ⇒ t2
|t1 ⇒ t1'
|(if t1 then t2 else t3) ⇒ (if t1' then t2 else t3)
)) ⇒* idB
. if x then false
) ⇒* tfalse
:Bool → Bool
. if x then false
)) ⇒* tfalse
We can use the normalize
tactic defined in the Types
to simplify these proofs.
Exercise: 2 stars (step_example3)
Try to do this one both with and without normalize
Next we consider the typing relation of the STLC.
: What is the type of the term "x y
: It depends on the types of x
I.e., in order to assign a type to a term, we need to know
what assumptions we should make about the types of its free
This leads us to a three-place typing judgment
written Γ ⊢ t ∈ T
, where Γ
"typing context" — a mapping from variables to their types.
Informally, we'll write Γ, x:T
for "extend the partial
to also map x
." Formally, we use the
to add a binding to a partial map.
|Γ x = T
|Γ ⊢ x ∈ T
|Γ , x:T11 ⊢ t12 ∈ T12
|Γ ⊢ \x:T11.t12 ∈ T11->T12
|Γ ⊢ t1 ∈ T11->T12
|Γ ⊢ t2 ∈ T11
|Γ ⊢ t1 t2 ∈ T12
|Γ ⊢ false ∈ Bool
|Γ ⊢ t1 ∈ Bool Γ ⊢ t2 ∈ T Γ ⊢ t3 ∈ T
|Γ ⊢ if t1 then t2 else t3 ∈ T
We can read the three-place relation Γ ⊢ t ∈ T
"to the term t
we can assign the type T
using as types for
the free variables of t
the ones specified in the context
Note that since we added the has_type constructors to the hints
database, auto can actually solve this one immediately.
∈ A →
) → A
Exercise: 2 stars, optional (typing_example_2_full)
Prove the same result without using auto
Exercise: 2 stars (typing_example_3)
Formally prove the following typing derivation holds:
We can also show that terms are not
typable. For example, let's
formally check that there is no typing derivation assigning a type
to the term \x:Bool. \y:Bool, x y
, x y
(tabs x TBool
(tabs y TBool
) (tvar y
. inversion Hc
. clear H
. clear H5
. clear H4
. clear H2
. clear H5
Exercise: 3 stars, optional (typing_nonexample_3)
. x x