StlcNew first draft
This commit is contained in:
wadler
parent
bcd2172337
commit
6252085f2d
4 changed files with 1777 additions and 4 deletions
910
src/StlcNew.lagda
Normal file
910
src/StlcNew.lagda
Normal file
|
|
@ -0,0 +1,910 @@
|
|||
---
|
||||
title : "StlcNew: The Simply Typed Lambda-Calculus"
|
||||
layout : page
|
||||
permalink : /StlcNew
|
||||
---
|
||||
|
||||
The _lambda-calculus_, first published by the logician Alonzo Church in
|
||||
1932, is a core calculus with only three syntactic constructs:
|
||||
variables, abstraction, and application. It embodies the concept of
|
||||
_functional abstraction_, which shows up in almost every programming
|
||||
language in some form (as functions, procedures, or methods).
|
||||
The _simply-typed lambda calculus_ (or STLC) is a variant of the
|
||||
lambda calculus published by Church in 1940. It has just the three
|
||||
constructs above for function types, plus whatever else is required
|
||||
for base types. Church had a minimal base type with no operations;
|
||||
we will be slightly more pragmatic and choose booleans as our base type.
|
||||
|
||||
This chapter formalises the simply-typed lambda calculus, giving its
|
||||
syntax, small-step semantics, and typing rules.
|
||||
The [next chapter](StlcNewProp) reviews its main properties,
|
||||
including progress and preservation.
|
||||
The most challenging new concepts will be
|
||||
_variable binding_ and _substitution_.
|
||||
|
||||
We choose booleans as our base type for simplicity. In later
|
||||
chapters we'll enrich lambda calculus with types including naturals,
|
||||
products, sums, and lists.
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
module StlcNew where
|
||||
|
||||
open import Data.String using (String; _≟_)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Relation.Nullary using (Dec; yes; no; ¬_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
|
||||
\end{code}
|
||||
|
||||
## Syntax
|
||||
|
||||
We have just two types.
|
||||
|
||||
* Functions, `A ⇒ B`
|
||||
* Booleans, `𝔹`
|
||||
|
||||
We require some form of base type, because otherwise the set of types
|
||||
would be empty. Church used a trivial base type `o` with no operations.
|
||||
For us, it is more convenient to use booleans. Later we will consider
|
||||
numbers as a base type.
|
||||
|
||||
Here is the syntax of types in BNF.
|
||||
|
||||
A, B, C ::= A ⇒ B | 𝔹
|
||||
|
||||
And here it is formalised in Agda.
|
||||
|
||||
\begin{code}
|
||||
infixr 20 _⇒_
|
||||
|
||||
data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
𝔹 : Type
|
||||
\end{code}
|
||||
|
||||
Terms have six constructs. Three are for the core lambda calculus:
|
||||
|
||||
* Variables, `# x`
|
||||
* Abstractions, `ƛ x ⇒ N`
|
||||
* Applications, `L · M`
|
||||
|
||||
and three are for the base type, booleans:
|
||||
|
||||
* True, `true`
|
||||
* False, `false`
|
||||
* Conditions, `if L then M else N`
|
||||
|
||||
Abstraction is also called lambda abstraction, and is the construct
|
||||
from which the calculus takes its name.
|
||||
|
||||
With the exception of variables, each term form either constructs
|
||||
a value of a given type (abstractions yield functions, true and
|
||||
false yield booleans) or deconstructs it (applications use functions,
|
||||
conditionals use booleans). We will see this again when we come
|
||||
to the rules for assigning types to terms, where constructors
|
||||
correspond to introduction rules and deconstructors to eliminators.
|
||||
|
||||
Here is the syntax of terms in BNF.
|
||||
|
||||
L, M, N ::= # x | λ x ⇒ N | L · M | true | false | if L then M else N
|
||||
|
||||
And here it is formalised in Agda.
|
||||
|
||||
\begin{code}
|
||||
infix 30 #_
|
||||
infixl 20 _·_
|
||||
infix 15 ƛ_⇒_
|
||||
infix 15 if_then_else_
|
||||
|
||||
Id : Set
|
||||
Id = String
|
||||
|
||||
data Term : Set where
|
||||
#_ : Id → Term
|
||||
ƛ_⇒_ : Id → Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
true : Term
|
||||
false : Term
|
||||
if_then_else_ : Term → Term → Term → Term
|
||||
\end{code}
|
||||
|
||||
|
||||
### Formal vs informal
|
||||
|
||||
In informal presentation of formal semantics, one uses choice of
|
||||
variable name to disambiguate and writes `x` rather than `# x`
|
||||
for a term that is a variable. Agda requires we distinguish.
|
||||
Often researchers use `var x` rather than `# x`, but we chose
|
||||
the latter since it is less noisy.
|
||||
|
||||
Similarly, informal presentation often use the same notation for
|
||||
function types, lambda abstraction, and function application in
|
||||
both the object language (the language one is describing) and the
|
||||
meta-language (the language in which the description is written),
|
||||
trusting readers can use context to distinguish the two. Agda is
|
||||
is not quite so forgiving, so here we use `A ⇒ B`, `ƛ x ⇒ N`,
|
||||
and `L · M` for the object language, as compared to `A → B`, `λ x → N`,
|
||||
and `L M` in our meta-language, Agda.
|
||||
|
||||
|
||||
### Examples
|
||||
|
||||
Here are a couple of example terms, `not` of type
|
||||
`𝔹 ⇒ 𝔹`, which complements its argument, and `two` of type
|
||||
`(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` which takes a function and a boolean
|
||||
and applies the function to the boolean twice.
|
||||
|
||||
\begin{code}
|
||||
not two : Term
|
||||
not = ƛ "x" ⇒ if # "x" then false else true
|
||||
two = ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x")
|
||||
\end{code}
|
||||
|
||||
|
||||
### Bound and free variables
|
||||
|
||||
In an abstraction `ƛ x ⇒ N` we call `x` the _bound_ variable
|
||||
and `N` the _body_ of the abstraction. One of the most important
|
||||
aspects of lambda calculus is that names of bound variables are
|
||||
irrelevant. Thus the five terms
|
||||
|
||||
* `` ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") ``
|
||||
* `` ƛ "g" ⇒ ƛ "y" ⇒ # "g" · (# "g" · # "y") ``
|
||||
* `` ƛ "fred" ⇒ ƛ "xander" ⇒ # "fred" · (# "fred" · # "xander") ``
|
||||
* `` λ[ 😇 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😈 ∶ 𝔹 ] ` 😇 · (` 😇 · ` 😈 ) ``
|
||||
* `` ƛ "x" ⇒ ƛ "f" ⇒ # "x" · (# "x" · # "f") ``
|
||||
|
||||
are all considered equivalent. This equivalence relation
|
||||
is often called _alpha renaming_.
|
||||
|
||||
As we descend from a term into its subterms, variables
|
||||
that are bound may become free. Consider the following terms.
|
||||
|
||||
* `` ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") ``
|
||||
Both variable `f` and `x` are bound.
|
||||
|
||||
* `` ƛ "x" ⇒ # "f" · (# "f" · # "x") ``
|
||||
has `x` as a bound variable but `f` as a free variable.
|
||||
|
||||
* `` # "f" · (# "f" · # "x") ``
|
||||
has both `f` and `x` as free variables.
|
||||
|
||||
We say that a term with no free variables is _closed_; otherwise it is
|
||||
_open_. Of the three terms above, the first is closed and the other
|
||||
two are open. A formal definition of bound and free variables will be
|
||||
given in the next chapter.
|
||||
|
||||
Different occurrences of a variable may be bound and free.
|
||||
In the term
|
||||
|
||||
(ƛ "x" ⇒ # "x") · # "x"
|
||||
|
||||
the inner occurrence of `x` is bound while the outer occurrence is free.
|
||||
Note that by alpha renaming, the term above is equivalent to
|
||||
|
||||
(ƛ "y" ⇒ # "y") · # "x"
|
||||
|
||||
in which `y` is bound and `x` is free. A common convention, called the
|
||||
Barendregt convention, is to use alpha renaming to ensure that the bound
|
||||
variables in a term are distinct from the free variables, which can
|
||||
avoid confusions that may arise if bound and free variables have the
|
||||
same names.
|
||||
|
||||
|
||||
### Precedence
|
||||
|
||||
As in Agda, functions of two or more arguments are represented via
|
||||
currying. This is made more convenient by declaring `_⇒_` to
|
||||
associate to the right and `_·_` to associate to the left.
|
||||
Thus,
|
||||
|
||||
* `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` abbreviates `(𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)`
|
||||
* `two · not · true` abbreviates `(two · not) · true`.
|
||||
|
||||
We choose the binding strength for abstractions and conditionals
|
||||
to be weaker than application. For instance,
|
||||
|
||||
* `` ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") ``
|
||||
- denotes `` (ƛ "f" ⇒ (ƛ "x" ⇒ (# "f" · (# "f" · # "x")))) ``
|
||||
- and not `` (ƛ "f" ⇒ (ƛ "x" ⇒ # "f")) · (# "f" · # "x") ``
|
||||
|
||||
\begin{code}
|
||||
_ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)
|
||||
_ = refl
|
||||
|
||||
_ : two · not · true ≡ (two · not) · true
|
||||
_ = refl
|
||||
|
||||
_ : ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x")
|
||||
≡ (ƛ "f" ⇒ (ƛ "x" ⇒ (# "f" · (# "f" · # "x"))))
|
||||
_ = refl
|
||||
\end{code}
|
||||
|
||||
### Quiz
|
||||
|
||||
* What is the type of the following term?
|
||||
|
||||
ƛ "f" ⇒ # "f" · (# "f" · true)
|
||||
|
||||
1. `𝔹 ⇒ (𝔹 ⇒ 𝔹)`
|
||||
2. `(𝔹 ⇒ 𝔹) ⇒ 𝔹`
|
||||
3. `𝔹 ⇒ 𝔹 ⇒ 𝔹`
|
||||
4. `𝔹 ⇒ 𝔹`
|
||||
5. `𝔹`
|
||||
|
||||
Give more than one answer if appropriate.
|
||||
|
||||
* What is the type of the following term?
|
||||
|
||||
(ƛ "f" ⇒ # "f" · (# "f" · true)) · not
|
||||
|
||||
1. `𝔹 ⇒ (𝔹 ⇒ 𝔹)`
|
||||
2. `(𝔹 ⇒ 𝔹) ⇒ 𝔹`
|
||||
3. `𝔹 ⇒ 𝔹 ⇒ 𝔹`
|
||||
4. `𝔹 ⇒ 𝔹`
|
||||
5. `𝔹`
|
||||
|
||||
Give more than one answer if appropriate.
|
||||
|
||||
## Values
|
||||
|
||||
We only consider reduction of _closed_ terms,
|
||||
those that contain no free variables. We consider
|
||||
a precise definition of free variables in
|
||||
[StlcPropNew](StlcPropNew).
|
||||
|
||||
A term is a value if it is fully reduced.
|
||||
For booleans, the situation is clear: `true` and
|
||||
`false` are values, while conditionals are not.
|
||||
For functions, applications are not values, because
|
||||
we expect them to further reduce, and variables are
|
||||
not values, because we focus on closed terms.
|
||||
Following convention, we treat all abstractions
|
||||
as values.
|
||||
|
||||
The predicate `Value M` holds if term `M` is a value.
|
||||
|
||||
\begin{code}
|
||||
data Value : Term → Set where
|
||||
value-λ : ∀ {x N} → Value (ƛ x ⇒ N)
|
||||
value-true : Value true
|
||||
value-false : Value false
|
||||
\end{code}
|
||||
|
||||
We let `V` and `W` range over values.
|
||||
|
||||
|
||||
### Formal vs informal
|
||||
|
||||
In informal presentations of formal semantics, using
|
||||
`V` as the name of a metavariable is sufficient to
|
||||
indicate that it is a value. In Agda, we must explicitly
|
||||
invoke the `Value` predicate.
|
||||
|
||||
### Other approaches
|
||||
|
||||
An alternative is not to focus on closed terms,
|
||||
to treat variables as values, and to treat
|
||||
`ƛ x ⇒ N` as a value only if `N` is a value.
|
||||
Indeed, this is how Agda normalises terms.
|
||||
We consider this approach in a [later chapter](Untyped).
|
||||
|
||||
## Substitution
|
||||
|
||||
The heart of lambda calculus is the operation of
|
||||
substituting one term for a variable in another term.
|
||||
Substitution plays a key role in defining the
|
||||
operational semantics of function application.
|
||||
For instance, we have
|
||||
|
||||
(ƛ "f" ⇒ # "f" · (# "f" · true)) · not
|
||||
⟹
|
||||
not · (not · true)
|
||||
|
||||
where we substitute `not` for `` `f `` in the body
|
||||
of the function abstraction.
|
||||
|
||||
We write substitution as `N [ x := V ]`, meaning
|
||||
"substitute term `V` for free occurrences of variable `x` in term `N`",
|
||||
or, more compactly, "substitute `V` for `x` in `N`".
|
||||
Substitution works if `V` is any closed term;
|
||||
it need not be a value, but we use `V` since we
|
||||
always substitute values.
|
||||
|
||||
Here are some examples.
|
||||
|
||||
* `` # "f" [ "f" := not ] `` yields `` not ``
|
||||
* `` true [ "f" := not ] `` yields `` true ``
|
||||
* `` (# "f" · true) [ "f" := not ] `` yields `` not · true ``
|
||||
* `` (# "f" · (# "f" · true)) [ "f" := not ] `` yields `` not · (not · true) ``
|
||||
* `` (ƛ "x" ⇒ # "f" · (# "f" · # "x")) [ "f" := not ] `` yields `` ƛ "x" ⇒ not · (not · # "x") ``
|
||||
* `` (ƛ "y" ⇒ # "y") [ "x" := true ] `` yields `` ƛ "y" ⇒ # "y" ``
|
||||
* `` (ƛ "x" ⇒ # "x") [ "x" := true ] `` yields `` ƛ "x" ⇒ # "x" ``
|
||||
|
||||
The last example is important: substituting `true` for `x` in
|
||||
`` ƛ "x" ⇒ # "x" `` does _not_ yield `` ƛ "x" ⇒ true ``.
|
||||
The reason for this is that `x` in the body of `` ƛ "x" ⇒ # "x" ``
|
||||
is _bound_ by the abstraction. An important feature of abstraction
|
||||
is that the choice of bound names is irrelevant: both
|
||||
`` ƛ "x" ⇒ # "x" `` and `` ƛ "y" ⇒ # "y" `` stand for the
|
||||
identity function. The way to think of this is that `x` within
|
||||
the body of the abstraction stands for a _different_ variable than
|
||||
`x` outside the abstraction, they both just happen to have the same
|
||||
name.
|
||||
|
||||
Here is the formal definition in Agda.
|
||||
|
||||
\begin{code}
|
||||
infix 25 _[_:=_]
|
||||
|
||||
_[_:=_] : Term → Id → Term → Term
|
||||
(# x) [ w := V ] with w ≟ x
|
||||
... | yes _ = V
|
||||
... | no _ = # x
|
||||
(ƛ x ⇒ N) [ w := V ] with w ≟ x
|
||||
... | yes _ = ƛ x ⇒ N
|
||||
... | no _ = ƛ x ⇒ (N [ w := V ])
|
||||
(L · M) [ w := V ] = (L [ w := V ]) · (M [ w := V ])
|
||||
(true) [ w := V ] = true
|
||||
(false) [ w := V ] = false
|
||||
(if L then M else N) [ w := V ] =
|
||||
if L [ w := V ] then M [ w := V ] else N [ w := V ]
|
||||
\end{code}
|
||||
|
||||
The two key cases are variables and abstraction.
|
||||
|
||||
* For variables, we compare `w`, the variable we are substituting for,
|
||||
with `x`, the variable in the term. If they are the same,
|
||||
we yield `V`, otherwise we yield `x` unchanged.
|
||||
|
||||
* For abstractions, we compare `w`, the variable we are substituting for,
|
||||
with `x`, the variable bound in the abstraction. If they are the same,
|
||||
we yield the abstraction unchanged, otherwise we subsititute inside the body.
|
||||
|
||||
In all other cases, we push substitution recursively into
|
||||
the subterms.
|
||||
|
||||
|
||||
|
||||
#### Examples
|
||||
|
||||
Here is confirmation that the examples above are correct.
|
||||
|
||||
\begin{code}
|
||||
_ : # "f" [ "f" := not ] ≡ not
|
||||
_ = refl
|
||||
|
||||
_ : true [ "f" := not ] ≡ true
|
||||
_ = refl
|
||||
|
||||
_ : (# "f" · true) [ "f" := not ] ≡ not · true
|
||||
_ = refl
|
||||
|
||||
_ : (# "f" · (# "f" · true)) [ "f" := not ] ≡ not · (not · true)
|
||||
_ = refl
|
||||
|
||||
_ : (ƛ "x" ⇒ # "f" · (# "f" · # "x")) [ "f" := not ] ≡ ƛ "x" ⇒ not · (not · # "x")
|
||||
_ = refl
|
||||
|
||||
_ : (ƛ "y" ⇒ # "y") [ "x" := true ] ≡ ƛ "y" ⇒ # "y"
|
||||
_ = refl
|
||||
|
||||
_ : (ƛ "x" ⇒ # "x") [ "x" := true ] ≡ ƛ "x" ⇒ # "x"
|
||||
_ = refl
|
||||
\end{code}
|
||||
|
||||
#### Quiz
|
||||
|
||||
What is the result of the following substitution?
|
||||
|
||||
(ƛ "y" ⇒ # "x" · (ƛ "x" ⇒ # "x")) [ "x" := true ]
|
||||
|
||||
1. `` (ƛ "y" ⇒ # "x" · (ƛ "x" ⇒ # "x")) ``
|
||||
2. `` (ƛ "y" ⇒ # "x" · (ƛ "x" ⇒ true)) ``
|
||||
3. `` (ƛ "y" ⇒ true · (ƛ "x" ⇒ # "x")) ``
|
||||
4. `` (ƛ "y" ⇒ true · (ƛ "x" ⇒ true)) ``
|
||||
|
||||
|
||||
## Reduction
|
||||
|
||||
We give the reduction rules for call-by-value lambda calculus. To
|
||||
reduce an application, first we reduce the left-hand side until it
|
||||
becomes a value (which must be an abstraction); then we reduce the
|
||||
right-hand side until it becomes a value; and finally we substitute
|
||||
the argument for the variable in the abstraction. To reduce a
|
||||
conditional, we first reduce the condition until it becomes a value;
|
||||
if the condition is true the conditional reduces to the first
|
||||
branch and if false it reduces to the second branch.
|
||||
|
||||
In an informal presentation of the formal semantics,
|
||||
the rules for reduction are written as follows.
|
||||
|
||||
L ⟹ L′
|
||||
--------------- ξ·₁
|
||||
L · M ⟹ L′ · M
|
||||
|
||||
M ⟹ M′
|
||||
--------------- ξ·₂
|
||||
V · M ⟹ V · M′
|
||||
|
||||
--------------------------------- βλ·
|
||||
(ƛ x ⇒ N) · V ⟹ N [ x := V ]
|
||||
|
||||
L ⟹ L′
|
||||
----------------------------------------- ξif
|
||||
if L then M else N ⟹ if L′ then M else N
|
||||
|
||||
-------------------------- βif-true
|
||||
if true then M else N ⟹ M
|
||||
|
||||
--------------------------- βif-false
|
||||
if false then M else N ⟹ N
|
||||
|
||||
As we will show later, the rules are deterministic, in that
|
||||
at most one rule applies to every term. As we will also show
|
||||
later, for every well-typed term either a reduction applies
|
||||
or it is a value.
|
||||
|
||||
The rules break into two sorts. Compatibility rules
|
||||
direct us to reduce some part of a term.
|
||||
We give them names starting with the Greek letter xi, `ξ`.
|
||||
Once a term is sufficiently
|
||||
reduced, it will consist of a constructor and
|
||||
a deconstructor, in our case `λ` and `·`, or
|
||||
`if` and `true`, or `if` and `false`.
|
||||
We give them names starting with the Greek letter beta, `β`,
|
||||
and indeed such rules are traditionally called beta rules.
|
||||
|
||||
Here are the above rules formalised in Agda.
|
||||
|
||||
\begin{code}
|
||||
infix 10 _⟹_
|
||||
|
||||
data _⟹_ : Term → Term → Set where
|
||||
|
||||
ξ·₁ : ∀ {L L′ M}
|
||||
→ L ⟹ L′
|
||||
-----------------
|
||||
→ L · M ⟹ L′ · M
|
||||
|
||||
ξ·₂ : ∀ {V M M′}
|
||||
→ Value V
|
||||
→ M ⟹ M′
|
||||
-----------------
|
||||
→ V · M ⟹ V · M′
|
||||
|
||||
βλ· : ∀ {x N V}
|
||||
→ Value V
|
||||
------------------------------------
|
||||
→ (ƛ x ⇒ N) · V ⟹ N [ x := V ]
|
||||
|
||||
ξif : ∀ {L L′ M N}
|
||||
→ L ⟹ L′
|
||||
-------------------------------------------
|
||||
→ if L then M else N ⟹ if L′ then M else N
|
||||
|
||||
βif-true : ∀ {M N}
|
||||
----------------------------
|
||||
→ if true then M else N ⟹ M
|
||||
|
||||
βif-false : ∀ {M N}
|
||||
-----------------------------
|
||||
→ if false then M else N ⟹ N
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Quiz
|
||||
|
||||
What does the following term step to?
|
||||
|
||||
(ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") ⟹ ???
|
||||
|
||||
1. `` (ƛ "x" ⇒ # "x") ``
|
||||
2. `` (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") ``
|
||||
3. `` (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") ``
|
||||
|
||||
What does the following term step to?
|
||||
|
||||
(ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") ⟹ ???
|
||||
|
||||
1. `` (ƛ "x" ⇒ # "x") ``
|
||||
2. `` (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") ``
|
||||
3. `` (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") ``
|
||||
|
||||
What does the following term step to? (Where `not` is as defined above.)
|
||||
|
||||
not · true ⟹ ???
|
||||
|
||||
1. `` if # "x" then false else true ``
|
||||
2. `` if true then false else true ``
|
||||
3. `` true ``
|
||||
4. `` false ``
|
||||
|
||||
What does the following term step to? (Where `two` and `not` are as defined above.)
|
||||
|
||||
two · not · true ⟹ ???
|
||||
|
||||
1. `` not · (not · true) ``
|
||||
2. `` (ƛ "x" ⇒ not · (not · # "x")) · true ``
|
||||
3. `` true ``
|
||||
4. `` false ``
|
||||
|
||||
## Reflexive and transitive closure
|
||||
|
||||
A single step is only part of the story. In general, we wish to repeatedly
|
||||
step a closed term until it reduces to a value. We do this by defining
|
||||
the reflexive and transitive closure `⟹*` of the step function `⟹`.
|
||||
In an informal presentation of the formal semantics, the rules
|
||||
are written as follows.
|
||||
|
||||
------- done
|
||||
M ⟹* M
|
||||
|
||||
L ⟹ M
|
||||
M ⟹* N
|
||||
------- step
|
||||
L ⟹* N
|
||||
|
||||
Here it is formalised in Agda, along similar lines to what
|
||||
we used for reasoning about [Equality](Equality).
|
||||
|
||||
\begin{code}
|
||||
infix 2 _⟹*_
|
||||
infix 1 begin_
|
||||
infixr 2 _⟹⟨_⟩_
|
||||
infix 3 _∎
|
||||
|
||||
data _⟹*_ : Term → Term → Set where
|
||||
_∎ : ∀ M
|
||||
---------
|
||||
→ M ⟹* M
|
||||
|
||||
_⟹⟨_⟩_ : ∀ L {M N}
|
||||
→ L ⟹ M
|
||||
→ M ⟹* N
|
||||
---------
|
||||
→ L ⟹* N
|
||||
|
||||
begin_ : ∀ {M N} → (M ⟹* N) → (M ⟹* N)
|
||||
begin M⟹*N = M⟹*N
|
||||
\end{code}
|
||||
|
||||
We can read this as follows.
|
||||
|
||||
* From term `M`, we can take no steps, giving `M ∎` of type `M ⟹* M`.
|
||||
|
||||
* From term `L` we can take a single step `L⟹M` of type `L ⟹ M`
|
||||
followed by zero or more steps `M⟹*N` of type `M ⟹* N`,
|
||||
giving `L ⟨ L⟹M ⟩ M⟹*N` of type `L ⟹* N`.
|
||||
|
||||
The names have been chosen to allow us to lay
|
||||
out example reductions in an appealing way.
|
||||
|
||||
\begin{code}
|
||||
_ : not · true ⟹* false
|
||||
_ =
|
||||
begin
|
||||
not · true
|
||||
⟹⟨ βλ· value-true ⟩
|
||||
if true then false else true
|
||||
⟹⟨ βif-true ⟩
|
||||
false
|
||||
∎
|
||||
|
||||
_ : two · not · true ⟹* true
|
||||
_ =
|
||||
begin
|
||||
two · not · true
|
||||
⟹⟨ ξ·₁ (βλ· value-λ) ⟩
|
||||
(ƛ "x" ⇒ not · (not · # "x")) · true
|
||||
⟹⟨ βλ· value-true ⟩
|
||||
not · (not · true)
|
||||
⟹⟨ ξ·₂ value-λ (βλ· value-true) ⟩
|
||||
not · (if true then false else true)
|
||||
⟹⟨ ξ·₂ value-λ βif-true ⟩
|
||||
not · false
|
||||
⟹⟨ βλ· value-false ⟩
|
||||
if false then false else true
|
||||
⟹⟨ βif-false ⟩
|
||||
true
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
|
||||
|
||||
|
||||
## Typing
|
||||
|
||||
While reduction considers only closed terms, typing must
|
||||
consider terms with free variables. To type a term,
|
||||
we must first type its subterms, and in particular in the
|
||||
body of an abstraction its bound variable may appear free.
|
||||
|
||||
In general, we use typing _judgements_ of the form
|
||||
|
||||
Γ ⊢ M ⦂ A
|
||||
|
||||
to assert in type environment `Γ` that term `M` has type `A`.
|
||||
Environment `Γ` provides types for all the free variables in `M`.
|
||||
|
||||
Here are three examples.
|
||||
|
||||
* `` ∅ , "f" ⦂ 𝔹 ⇒ 𝔹 , "x" ⦂ 𝔹 ⊢ # "f" · (# "f" · # "x") ⦂ 𝔹 ``
|
||||
* `` ∅ , "f" ⦂ 𝔹 ⇒ 𝔹 ⊢ (ƛ "x" ⇒ # "f" · (# "f" · # "x")) ⦂ 𝔹 ⇒ 𝔹 ``
|
||||
* `` ∅ ⊢ ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x")) ⦂ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ``
|
||||
|
||||
Environments are partial maps from identifiers to types, built using `∅`
|
||||
for the empty map, and `Γ , x ⦂ A` for the map that extends
|
||||
environment `Γ` by mapping variable `x` to type `A`.
|
||||
|
||||
*It's redundant to have two versions of the rules*
|
||||
|
||||
*Need text to explain `Γ ∋ x ⦂ A`*
|
||||
|
||||
In an informal presentation of the formal semantics,
|
||||
the rules for typing are written as follows.
|
||||
|
||||
Γ x ≡ A
|
||||
----------- Ax
|
||||
Γ ⊢ ` x ⦂ A
|
||||
|
||||
Γ , x ⦂ A ⊢ N ⦂ B
|
||||
------------------------ ⇒-I
|
||||
Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B
|
||||
|
||||
Γ ⊢ L ⦂ A ⇒ B
|
||||
Γ ⊢ M ⦂ A
|
||||
-------------- ⇒-E
|
||||
Γ ⊢ L · M ⦂ B
|
||||
|
||||
------------- 𝔹-I₁
|
||||
Γ ⊢ true ⦂ 𝔹
|
||||
|
||||
-------------- 𝔹-I₂
|
||||
Γ ⊢ false ⦂ 𝔹
|
||||
|
||||
Γ ⊢ L : 𝔹
|
||||
Γ ⊢ M ⦂ A
|
||||
Γ ⊢ N ⦂ A
|
||||
-------------------------- 𝔹-E
|
||||
Γ ⊢ if L then M else N ⦂ A
|
||||
|
||||
As we will show later, the rules are deterministic, in that
|
||||
at most one rule applies to every term.
|
||||
|
||||
The proof rules come in pairs, with rules to introduce and to
|
||||
eliminate each connective, labeled `-I` and `-E`, respectively. As we
|
||||
read the rules from top to bottom, introduction and elimination rules
|
||||
do what they say on the tin: the first _introduces_ a formula for the
|
||||
connective, which appears in the conclusion but not in the premises;
|
||||
while the second _eliminates_ a formula for the connective, which appears in
|
||||
a premise but not in the conclusion. An introduction rule describes
|
||||
how to construct a value of the type (abstractions yield functions,
|
||||
true and false yield booleans), while an elimination rule describes
|
||||
how to deconstruct a value of the given type (applications use
|
||||
functions, conditionals use booleans).
|
||||
|
||||
Here are the above rules formalised in Agda.
|
||||
|
||||
\begin{code}
|
||||
infix 4 _∋_⦂_
|
||||
infix 4 _⊢_⦂_
|
||||
infixl 5 _,_⦂_
|
||||
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_,_⦂_ : Context → Id → Type → Context
|
||||
|
||||
data _∋_⦂_ : Context → Id → Type → Set where
|
||||
|
||||
Z : ∀ {Γ x A}
|
||||
------------------
|
||||
→ Γ , x ⦂ A ∋ x ⦂ A
|
||||
|
||||
S : ∀ {Γ w x A B}
|
||||
→ w ≢ x
|
||||
→ Γ ∋ w ⦂ B
|
||||
------------------
|
||||
→ Γ , x ⦂ A ∋ w ⦂ B
|
||||
|
||||
data _⊢_⦂_ : Context → Term → Type → Set where
|
||||
|
||||
Ax : ∀ {Γ x A}
|
||||
→ Γ ∋ x ⦂ A
|
||||
-------------
|
||||
→ Γ ⊢ # x ⦂ A
|
||||
|
||||
⇒-I : ∀ {Γ x N A B}
|
||||
→ Γ , x ⦂ A ⊢ N ⦂ B
|
||||
--------------------
|
||||
→ Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B
|
||||
|
||||
⇒-E : ∀ {Γ L M A B}
|
||||
→ Γ ⊢ L ⦂ A ⇒ B
|
||||
→ Γ ⊢ M ⦂ A
|
||||
--------------
|
||||
→ Γ ⊢ L · M ⦂ B
|
||||
|
||||
𝔹-I₁ : ∀ {Γ}
|
||||
-------------
|
||||
→ Γ ⊢ true ⦂ 𝔹
|
||||
|
||||
𝔹-I₂ : ∀ {Γ}
|
||||
--------------
|
||||
→ Γ ⊢ false ⦂ 𝔹
|
||||
|
||||
𝔹-E : ∀ {Γ L M N A}
|
||||
→ Γ ⊢ L ⦂ 𝔹
|
||||
→ Γ ⊢ M ⦂ A
|
||||
→ Γ ⊢ N ⦂ A
|
||||
---------------------------
|
||||
→ Γ ⊢ if L then M else N ⦂ A
|
||||
\end{code}
|
||||
|
||||
#### Example type derivations
|
||||
|
||||
Here are a couple of typing examples. First, here is how
|
||||
they would be written in an informal description of the
|
||||
formal semantics.
|
||||
|
||||
Derivation of `not`:
|
||||
|
||||
------------ Z
|
||||
Γ₀ ∋ "x" ⦂ B
|
||||
-------------- Ax -------------- 𝔹-I₂ ------------- 𝔹-I₁
|
||||
Γ₀ ⊢ # "x" ⦂ 𝔹 Γ₀ ⊢ false ⦂ 𝔹 Γ₀ ⊢ true ⦂ 𝔹
|
||||
------------------------------------------------------ 𝔹-E
|
||||
Γ₀ ⊢ if # "x" then false else true ⦂ 𝔹
|
||||
--------------------------------------------------- ⇒-I
|
||||
∅ ⊢ ƛ "x" ⇒ if # "x" then false else true ⦂ 𝔹 ⇒ 𝔹
|
||||
|
||||
where `Γ₀ = ∅ , x ⦂ 𝔹`.
|
||||
|
||||
Derivation of `two`:
|
||||
|
||||
∋f ∋f ∋x
|
||||
------------------- Ax ------------------- Ax --------------- Ax
|
||||
Γ₂ ⊢ # "f" ⦂ 𝔹 ⇒ 𝔹 Γ₂ ⊢ # "f" ⦂ 𝔹 ⇒ 𝔹 Γ₂ ⊢ # "x" ⦂ 𝔹
|
||||
------------------- Ax ------------------------------------------ ⇒-E
|
||||
Γ₂ ⊢ # "f" ⦂ 𝔹 ⇒ 𝔹 Γ₂ ⊢ # "f" · # "x" ⦂ 𝔹
|
||||
-------------------------------------------------- ⇒-E
|
||||
Γ₂ ⊢ # "f" · (# "f" · # "x") ⦂ 𝔹
|
||||
---------------------------------------------- ⇒-I
|
||||
Γ₁ ⊢ ƛ "x" ⇒ # "f" · (# "f" · # "x") ⦂ 𝔹 ⇒ 𝔹
|
||||
---------------------------------------------------------- ⇒-I
|
||||
∅ ⊢ ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") ⦂ 𝔹 ⇒ 𝔹
|
||||
|
||||
Where `∋f` and `∋x` abbreviate the two derivations:
|
||||
|
||||
|
||||
---------------- Z
|
||||
"f" ≢ "x" Γ₁ ∋ "f" ⦂ B ⇒ B
|
||||
----------------------------- S ------------- Z
|
||||
Γ₂ ∋ "f" ⦂ B ⇒ B Γ₂ ∋ "x" ⦂ 𝔹
|
||||
|
||||
where `Γ₁ = ∅ , f ⦂ 𝔹 ⇒ 𝔹` and `Γ₂ = ∅ , f ⦂ 𝔹 ⇒ 𝔹 , x ⦂ 𝔹`.
|
||||
|
||||
Here are the above derivations formalised in Agda.
|
||||
|
||||
\begin{code}
|
||||
_≠_ : ∀ (x y : Id) → x ≢ y
|
||||
x ≠ y with x ≟ y
|
||||
... | no x≢y = x≢y
|
||||
... | yes _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
|
||||
⊢not : ∅ ⊢ not ⦂ 𝔹 ⇒ 𝔹
|
||||
⊢not = ⇒-I (𝔹-E (Ax Z) 𝔹-I₂ 𝔹-I₁)
|
||||
|
||||
⊢two : ∅ ⊢ two ⦂ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
|
||||
⊢two = ⇒-I (⇒-I (⇒-E (Ax ⊢f) (⇒-E (Ax ⊢f) (Ax ⊢x))))
|
||||
where
|
||||
⊢f = S ("f" ≠ "x") Z
|
||||
⊢x = Z
|
||||
\end{code}
|
||||
|
||||
#### Interaction with Agda
|
||||
|
||||
Construction of a type derivation is best done interactively.
|
||||
Start with the declaration:
|
||||
|
||||
⊢not : ∅ ⊢ not ⦂ 𝔹 ⇒ 𝔹
|
||||
⊢not = ?
|
||||
|
||||
Typing C-l causes Agda to create a hole and tell us its expected type.
|
||||
|
||||
⊢not = { }0
|
||||
?0 : ∅ ⊢ not ⦂ 𝔹 ⇒ 𝔹
|
||||
|
||||
Now we fill in the hole by typing C-c C-r. Agda observes that
|
||||
the outermost term in `not` in a `λ`, which is typed using `⇒-I`. The
|
||||
`⇒-I` rule in turn takes one argument, which Agda leaves as a hole.
|
||||
|
||||
⊢not = ⇒-I { }0
|
||||
?0 : ∅ , x ⦂ 𝔹 ⊢ if ` x then false else true ⦂ 𝔹
|
||||
|
||||
Again we fill in the hole by typing C-c C-r. Agda observes that the
|
||||
outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The
|
||||
`𝔹-E` rule in turn takes three arguments, which Agda leaves as holes.
|
||||
|
||||
⊢not = ⇒-I (𝔹-E { }0 { }1 { }2)
|
||||
?0 : ∅ , x ⦂ 𝔹 ⊢ ` x ⦂
|
||||
?1 : ∅ , x ⦂ 𝔹 ⊢ false ⦂ 𝔹
|
||||
?2 : ∅ , x ⦂ 𝔹 ⊢ true ⦂ 𝔹
|
||||
|
||||
Again we fill in the three holes by typing C-c C-r in each. Agda observes
|
||||
that `` ` x ``, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and
|
||||
`𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show
|
||||
that `(∅ , x ⦂ 𝔹) x = just 𝔹`, which can in turn be specified with a
|
||||
hole. After filling in all holes, the term is as above.
|
||||
|
||||
The entire process can be automated using Agsy, invoked with C-c C-a.
|
||||
|
||||
#### Non-examples
|
||||
|
||||
We can also show that terms are _not_ typeable. For example, here is
|
||||
a formal proof that it is not possible to type the term `` true ·
|
||||
false ``. In other words, no type `A` is the type of this term. It
|
||||
cannot be typed, because doing so requires that the first term in the
|
||||
application is both a boolean and a function.
|
||||
|
||||
\begin{code}
|
||||
¬⊢₁ : ∀ {A} → ¬ (∅ ⊢ true · false ⦂ A)
|
||||
¬⊢₁ (⇒-E () _)
|
||||
\end{code}
|
||||
|
||||
As a second example, here is a formal proof that it is not possible to
|
||||
type `` ƛ "x" ⇒ # "x" · # "x" `` It cannot be typed, because
|
||||
doing so requires some types `A` and `B` such that `A ⇒ B ≡ A`.
|
||||
|
||||
\begin{code}
|
||||
contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A)
|
||||
contradiction ()
|
||||
|
||||
∋-injective : ∀ {Γ x A₁ A₂} → Γ ∋ x ⦂ A₁ → Γ ∋ x ⦂ A₂ → A₁ ≡ A₂
|
||||
∋-injective Z Z = refl
|
||||
∋-injective Z (S w≢ _) = ⊥-elim (w≢ refl)
|
||||
∋-injective (S w≢ _) Z = ⊥-elim (w≢ refl)
|
||||
∋-injective (S _ ∋w₁) (S _ ∋w₂) = ∋-injective ∋w₁ ∋w₂
|
||||
|
||||
¬⊢₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ # "x" · # "x" ⦂ A)
|
||||
¬⊢₂ (⇒-I (⇒-E (Ax ∋x₁) (Ax ∋x₂))) = contradiction (∋-injective ∋x₁ ∋x₂)
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Quiz
|
||||
|
||||
For each of the following, given a type `A` for which it is derivable,
|
||||
or explain why there is no such `A`.
|
||||
|
||||
1. `` ∅ , y ⦂ A ⊢ λ[ x ⦂ 𝔹 ] ` x ⦂ 𝔹 ⇒ 𝔹 ``
|
||||
2. `` ∅ ⊢ λ[ y ⦂ 𝔹 ⇒ 𝔹 ] λ[ x ⦂ 𝔹 ] ` y · ` x ⦂ A ``
|
||||
3. `` ∅ ⊢ λ[ y ⦂ 𝔹 ⇒ 𝔹 ] λ[ x ⦂ 𝔹 ] ` x · ` y ⦂ A ``
|
||||
4. `` ∅ , x ⦂ A ⊢ λ[ y : 𝔹 ⇒ 𝔹 ] `y · `x : A ``
|
||||
|
||||
For each of the following, give type `A`, `B`, `C`, and `D` for which it is derivable,
|
||||
or explain why there are no such types.
|
||||
|
||||
1. `` ∅ ⊢ λ[ y ⦂ 𝔹 ⇒ 𝔹 ⇒ 𝔹 ] λ[ x ⦂ 𝔹 ] ` y · ` x ⦂ A ``
|
||||
2. `` ∅ , x ⦂ A ⊢ x · x ⦂ B ``
|
||||
3. `` ∅ , x ⦂ A , y ⦂ B ⊢ λ[ z ⦂ C ] ` x · (` y · ` z) ⦂ D ``
|
||||
|
||||
|
||||
|
||||
## Unicode
|
||||
|
||||
This chapter uses the following unicode
|
||||
|
||||
⇒ U+21D2: RIGHTWARDS DOUBLE ARROW (\=>)
|
||||
ƛ U+019B: LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-)
|
||||
⦂ U+2982: Z NOTATION TYPE COLON (\:)
|
||||
· U+00B7: MIDDLE DOT (\cdot)
|
||||
😇 U+1F607: SMILING FACE WITH HALO
|
||||
😈 U+1F608: SMILING FACE WITH HORNS
|
||||
′ U+2032: PRIME (\')
|
||||
⟹ U+27F9: LONG RIGHTWARDS DOUBLE ARROW (\r6)
|
||||
ξ U+03BE: GREEK SMALL LETTER XI (\Gx or \xi)
|
||||
β U+03B2: GREEK SMALL LETTER BETA (\Gb or \beta)
|
||||
|
||||
Note that ′ (U+2032: PRIME) is not the same as ' (U+0027: APOSTROPHE).
|
||||
854
src/StlcPropNew.lagda
Normal file
854
src/StlcPropNew.lagda
Normal file
|
|
@ -0,0 +1,854 @@
|
|||
---
|
||||
title : "StlcPropNew: Properties of STLC"
|
||||
layout : page
|
||||
permalink : /StlcPropNew
|
||||
---
|
||||
|
||||
In this chapter, we develop the fundamental theory of the Simply
|
||||
Typed Lambda Calculus---in particular, the type safety
|
||||
theorem.
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
module StlcPropNew where
|
||||
|
||||
open import Function using (_∘_)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Maybe using (Maybe; just; nothing)
|
||||
open import Data.Product using (_×_; ∃; ∃₂; _,_; ,_)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym)
|
||||
open import Maps using (Id; _≟_; PartialMap)
|
||||
open Maps.PartialMap using (∅; apply-∅; update-permute; just≢nothing; just-injective)
|
||||
renaming (_,_↦_ to _,_∶_)
|
||||
open import Stlc
|
||||
import Data.Nat using (ℕ)
|
||||
\end{code}
|
||||
|
||||
|
||||
## Canonical Forms
|
||||
|
||||
<!--
|
||||
As we saw for the simple calculus in Chapter [Types]({{ "Types" | relative_url }}),
|
||||
-->
|
||||
|
||||
The first step in establishing basic properties of reduction and typing
|
||||
is to identify the possible _canonical forms_ (i.e., well-typed closed values)
|
||||
belonging to each type. For function types the canonical forms are lambda-abstractions,
|
||||
while for boolean types they are values `true` and `false`.
|
||||
|
||||
\begin{code}
|
||||
data canonical_for_ : Term → Type → Set where
|
||||
canonical-λ : ∀ {x A N B} → canonical (λ[ x ∶ A ] N) for (A ⇒ B)
|
||||
canonical-true : canonical true for 𝔹
|
||||
canonical-false : canonical false for 𝔹
|
||||
|
||||
canonical-forms : ∀ {L A} → ∅ ⊢ L ∶ A → Value L → canonical L for A
|
||||
canonical-forms (Ax ()) ()
|
||||
canonical-forms (⇒-I ⊢N) value-λ = canonical-λ
|
||||
canonical-forms (⇒-E ⊢L ⊢M) ()
|
||||
canonical-forms 𝔹-I₁ value-true = canonical-true
|
||||
canonical-forms 𝔹-I₂ value-false = canonical-false
|
||||
canonical-forms (𝔹-E ⊢L ⊢M ⊢N) ()
|
||||
\end{code}
|
||||
|
||||
## Progress
|
||||
|
||||
As before, the _progress_ theorem tells us that closed, well-typed
|
||||
terms are not stuck: either a well-typed term can take a reduction
|
||||
step or it is a value.
|
||||
|
||||
\begin{code}
|
||||
data Progress : Term → Set where
|
||||
steps : ∀ {M N} → M ⟹ N → Progress M
|
||||
done : ∀ {M} → Value M → Progress M
|
||||
|
||||
progress : ∀ {M A} → ∅ ⊢ M ∶ A → Progress M
|
||||
\end{code}
|
||||
|
||||
<!--
|
||||
The proof is a relatively straightforward extension of the progress proof we saw in
|
||||
[Types]({{ "Types" | relative_url }}).
|
||||
-->
|
||||
|
||||
We give the proof in English first, then the formal version.
|
||||
|
||||
_Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
|
||||
|
||||
- The last rule of the derivation cannot be `Ax`,
|
||||
since a variable is never well typed in an empty context.
|
||||
|
||||
- If the last rule of the derivation is `⇒-I`, `𝔹-I₁`, or `𝔹-I₂`
|
||||
then, trivially, the term is a value.
|
||||
|
||||
- If the last rule of the derivation is `⇒-E`, then the term has the
|
||||
form `L · M` for some `L` and `M`, where we know that `L` and `M`
|
||||
are also well typed in the empty context, giving us two induction
|
||||
hypotheses. By the first induction hypothesis, either `L`
|
||||
can take a step or is a value.
|
||||
|
||||
- If `L` can take a step, then so can `L · M` by `ξ·₁`.
|
||||
|
||||
- If `L` is a value then consider `M`. By the second induction
|
||||
hypothesis, either `M` can take a step or is a value.
|
||||
|
||||
- If `M` can take a step, then so can `L · M` by `ξ·₂`.
|
||||
|
||||
- If `M` is a value, then since `L` is a value with a
|
||||
function type we know from the canonical forms lemma
|
||||
that it must be a lambda abstraction,
|
||||
and hence `L · M` can take a step by `βλ·`.
|
||||
|
||||
- If the last rule of the derivation is `𝔹-E`, then the term has
|
||||
the form `if L then M else N` where `L` has type `𝔹`.
|
||||
By the induction hypothesis, either `L` can take a step or is
|
||||
a value.
|
||||
|
||||
- If `L` can take a step, then so can `if L then M else N` by `ξif`.
|
||||
|
||||
- If `L` is a value, then since it has type boolean we know from
|
||||
the canonical forms lemma that it must be either `true` or
|
||||
`false`.
|
||||
|
||||
- If `L` is `true`, then `if L then M else N` steps by `βif-true`
|
||||
|
||||
- If `L` is `false`, then `if L then M else N` steps by `βif-false`
|
||||
|
||||
This completes the proof.
|
||||
|
||||
\begin{code}
|
||||
progress (Ax ())
|
||||
progress (⇒-I ⊢N) = done value-λ
|
||||
progress (⇒-E ⊢L ⊢M) with progress ⊢L
|
||||
... | steps L⟹L′ = steps (ξ·₁ L⟹L′)
|
||||
... | done valueL with progress ⊢M
|
||||
... | steps M⟹M′ = steps (ξ·₂ valueL M⟹M′)
|
||||
... | done valueM with canonical-forms ⊢L valueL
|
||||
... | canonical-λ = steps (βλ· valueM)
|
||||
progress 𝔹-I₁ = done value-true
|
||||
progress 𝔹-I₂ = done value-false
|
||||
progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L
|
||||
... | steps L⟹L′ = steps (ξif L⟹L′)
|
||||
... | done valueL with canonical-forms ⊢L valueL
|
||||
... | canonical-true = steps βif-true
|
||||
... | canonical-false = steps βif-false
|
||||
\end{code}
|
||||
|
||||
This code reads neatly in part because we consider the
|
||||
`steps` option before the `done` option. We could, of course,
|
||||
do it the other way around, but then the `...` abbreviation
|
||||
no longer works, and we will need to write out all the arguments
|
||||
in full. In general, the rule of thumb is to consider the easy case
|
||||
(here `steps`) before the hard case (here `done`).
|
||||
If you have two hard cases, you will have to expand out `...`
|
||||
or introduce subsidiary functions.
|
||||
|
||||
#### Exercise: 3 stars, optional (progress_from_term_ind)
|
||||
Show that progress can also be proved by induction on terms
|
||||
instead of induction on typing derivations.
|
||||
|
||||
\begin{code}
|
||||
postulate
|
||||
progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M
|
||||
\end{code}
|
||||
|
||||
## Preservation
|
||||
|
||||
The other half of the type soundness property is the preservation
|
||||
of types during reduction. For this, we need to develop
|
||||
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), the story goes like this:
|
||||
|
||||
- The _preservation theorem_ is proved by induction on a typing derivation.
|
||||
derivation, pretty much as we did in chapter [Types]({{ "Types" | relative_url }})
|
||||
|
||||
- The one case that is significantly different is the one for the
|
||||
`βλ·` rule, whose definition uses the substitution operation. To see that
|
||||
this step preserves typing, we need to know that the substitution itself
|
||||
does. So we prove a ...
|
||||
|
||||
- _substitution lemma_, stating that substituting a (closed) term
|
||||
`V` for a variable `x` in a term `N` preserves the type of `N`.
|
||||
The proof goes by induction on the form of `N` and requires
|
||||
looking at all the different cases in the definition of
|
||||
substitition. The lemma does not require that `V` be a value,
|
||||
though in practice we only substitute values. The tricky cases
|
||||
are the ones for variables and for function abstractions. In both
|
||||
cases, we discover that we need to take a term `V` that has been
|
||||
shown to be well-typed in some context `Γ` and consider the same
|
||||
term in a different context `Γ′`. For this we prove a ...
|
||||
|
||||
- _context invariance_ lemma, showing that typing is preserved
|
||||
under "inessential changes" to the context---a term `M`
|
||||
well typed in `Γ` is also well typed in `Γ′`, so long as
|
||||
all the free variables of `M` appear in both contexts.
|
||||
And finally, for this, we need a careful definition of ...
|
||||
|
||||
- _free variables_ of a term---i.e., those variables
|
||||
mentioned in a term and not bound in an enclosing
|
||||
lambda abstraction.
|
||||
|
||||
To make Agda happy, we need to formalize the story in the opposite
|
||||
order.
|
||||
|
||||
|
||||
### Free Occurrences
|
||||
|
||||
A variable `x` appears _free_ in a term `M` if `M` contains an
|
||||
occurrence of `x` that is not bound in an enclosing lambda abstraction.
|
||||
For example:
|
||||
|
||||
- Variable `x` appears free, but `f` does not, in ``λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x``.
|
||||
- Both `f` and `x` appear free in ``(λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f``.
|
||||
Indeed, `f` appears both bound and free in this term.
|
||||
- No variables appear free in ``λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x``.
|
||||
|
||||
Formally:
|
||||
|
||||
\begin{code}
|
||||
data _∈_ : Id → Term → Set where
|
||||
free-` : ∀ {x} → x ∈ ` x
|
||||
free-λ : ∀ {x y A N} → y ≢ x → x ∈ N → x ∈ (λ[ y ∶ A ] N)
|
||||
free-·₁ : ∀ {x L M} → x ∈ L → x ∈ (L · M)
|
||||
free-·₂ : ∀ {x L M} → x ∈ M → x ∈ (L · M)
|
||||
free-if₁ : ∀ {x L M N} → x ∈ L → x ∈ (if L then M else N)
|
||||
free-if₂ : ∀ {x L M N} → x ∈ M → x ∈ (if L then M else N)
|
||||
free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
|
||||
\end{code}
|
||||
|
||||
A term in which no variables appear free is said to be _closed_.
|
||||
|
||||
\begin{code}
|
||||
_∉_ : Id → Term → Set
|
||||
x ∉ M = ¬ (x ∈ M)
|
||||
|
||||
closed : Term → Set
|
||||
closed M = ∀ {x} → x ∉ M
|
||||
\end{code}
|
||||
|
||||
Here are proofs corresponding to the first two examples above.
|
||||
|
||||
\begin{code}
|
||||
f≢x : f ≢ x
|
||||
f≢x ()
|
||||
|
||||
example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
|
||||
example-free₁ = free-λ f≢x (free-·₂ free-`)
|
||||
|
||||
example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
|
||||
example-free₂ (free-λ f≢f _) = f≢f refl
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Exercise: 1 star (free-in)
|
||||
Prove formally the remaining examples given above.
|
||||
|
||||
\begin{code}
|
||||
postulate
|
||||
example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
|
||||
example-free₄ : f ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
|
||||
example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
|
||||
example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
|
||||
\end{code}
|
||||
|
||||
Although `_∈_` may appear to be a low-level technical definition,
|
||||
understanding it is crucial to understanding the properties of
|
||||
substitution, which are really the crux of the lambda calculus.
|
||||
|
||||
### Substitution
|
||||
|
||||
To prove that substitution preserves typing, we first need a technical
|
||||
lemma connecting free variables and typing contexts. If variable `x`
|
||||
appears free in term `M`, and if `M` is well typed in context `Γ`,
|
||||
then `Γ` must assign a type to `x`.
|
||||
|
||||
\begin{code}
|
||||
free-lemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
|
||||
\end{code}
|
||||
|
||||
_Proof_: We show, by induction on the proof that `x` appears
|
||||
free in `M`, that, for all contexts `Γ`, if `M` is well
|
||||
typed under `Γ`, then `Γ` assigns some type to `x`.
|
||||
|
||||
- If the last rule used was `` free-` ``, then `M = `` `x ``, and from
|
||||
the assumption that `M` is well typed under `Γ` we have
|
||||
immediately that `Γ` assigns a type to `x`.
|
||||
|
||||
- If the last rule used was `free-·₁`, then `M = L · M` and `x`
|
||||
appears free in `L`. Since `L` is well typed under `Γ`,
|
||||
we can see from the typing rules that `L` must also be, and
|
||||
the IH then tells us that `Γ` assigns `x` a type.
|
||||
|
||||
- Almost all the other cases are similar: `x` appears free in a
|
||||
subterm of `M`, and since `M` is well typed under `Γ`, we
|
||||
know the subterm of `M` in which `x` appears is well typed
|
||||
under `Γ` as well, and the IH yields the desired conclusion.
|
||||
|
||||
- The only remaining case is `free-λ`. In this case `M =
|
||||
λ[ y ∶ A ] N`, and `x` appears free in `N`; we also know that
|
||||
`x` is different from `y`. The difference from the previous
|
||||
cases is that whereas `M` is well typed under `Γ`, its
|
||||
body `N` is well typed under `(Γ , y ∶ A)`, so the IH
|
||||
allows us to conclude that `x` is assigned some type by the
|
||||
extended context `(Γ , y ∶ A)`. To conclude that `Γ`
|
||||
assigns a type to `x`, we appeal the decidable equality for names
|
||||
`_≟_`, and note that `x` and `y` are different variables.
|
||||
|
||||
\begin{code}
|
||||
free-lemma free-` (Ax Γx≡A) = (_ , Γx≡A)
|
||||
free-lemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = free-lemma x∈L ⊢L
|
||||
free-lemma (free-·₂ x∈M) (⇒-E ⊢L ⊢M) = free-lemma x∈M ⊢M
|
||||
free-lemma (free-if₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈L ⊢L
|
||||
free-lemma (free-if₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈M ⊢M
|
||||
free-lemma (free-if₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈N ⊢N
|
||||
free-lemma (free-λ {x} {y} y≢x x∈N) (⇒-I ⊢N) with free-lemma x∈N ⊢N
|
||||
... | Γx≡C with y ≟ x
|
||||
... | yes y≡x = ⊥-elim (y≢x y≡x)
|
||||
... | no _ = Γx≡C
|
||||
\end{code}
|
||||
|
||||
A subtle point: if the first argument of `free-λ` was of type
|
||||
`x ≢ y` rather than of type `y ≢ x`, then the type of the
|
||||
term `Γx≡C` would not simplify properly; instead, one would need
|
||||
to rewrite with the symmetric equivalence.
|
||||
|
||||
As a second technical lemma, we need that any term `M` which is well
|
||||
typed in the empty context is closed (has no free variables).
|
||||
|
||||
#### Exercise: 2 stars, optional (∅⊢-closed)
|
||||
|
||||
\begin{code}
|
||||
postulate
|
||||
∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
|
||||
\end{code}
|
||||
|
||||
<div class="hidden">
|
||||
\begin{code}
|
||||
∅⊢-closed′ : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
|
||||
∅⊢-closed′ {M} {A} ⊢M {x} x∈M with free-lemma x∈M ⊢M
|
||||
... | (B , ∅x≡B) = just≢nothing (trans (sym ∅x≡B) (apply-∅ x))
|
||||
\end{code}
|
||||
</div>
|
||||
|
||||
Sometimes, when we have a proof `Γ ⊢ M ∶ A`, we will need to
|
||||
replace `Γ` by a different context `Γ′`. When is it safe
|
||||
to do this? Intuitively, the only variables we care about
|
||||
in the context are those that appear free in `M`. So long
|
||||
as the two contexts agree on those variables, one can be
|
||||
exchanged for the other.
|
||||
|
||||
\begin{code}
|
||||
context-lemma : ∀ {Γ Γ′ M A}
|
||||
→ (∀ {x} → x ∈ M → Γ x ≡ Γ′ x)
|
||||
→ Γ ⊢ M ∶ A
|
||||
→ Γ′ ⊢ M ∶ A
|
||||
\end{code}
|
||||
|
||||
_Proof_: By induction on the derivation of `Γ ⊢ M ∶ A`.
|
||||
|
||||
- If the last rule in the derivation was `Ax`, then `M = x`
|
||||
and `Γ x ≡ just A`. By assumption, `Γ′ x = just A` as well, and
|
||||
hence `Γ′ ⊢ M : A` by `Ax`.
|
||||
|
||||
- If the last rule was `⇒-I`, then `M = λ[ y : A] N`, with
|
||||
`A = A ⇒ B` and `Γ , y ∶ A ⊢ N ∶ B`. The
|
||||
induction hypothesis is that, for any context `Γ″`, if
|
||||
`Γ , y : A` and `Γ″` assign the same types to all the
|
||||
free variables in `N`, then `N` has type `B` under
|
||||
`Γ″`. Let `Γ′` be a context which agrees with
|
||||
`Γ` on the free variables in `N`; we must show
|
||||
`Γ′ ⊢ λ[ y ∶ A] N ∶ A ⇒ B`.
|
||||
|
||||
By `⇒-I`, it suffices to show that `Γ′ , y:A ⊢ N ∶ B`.
|
||||
By the IH (setting `Γ″ = Γ′ , y : A`), it suffices to show
|
||||
that `Γ , y : A` and `Γ′ , y : A` agree on all the variables
|
||||
that appear free in `N`.
|
||||
|
||||
Any variable occurring free in `N` must be either `y` or
|
||||
some other variable. Clearly, `Γ , y : A` and `Γ′ , y : A`
|
||||
agree on `y`. Otherwise, any variable other
|
||||
than `y` that occurs free in `N` also occurs free in
|
||||
`λ[ y : A] N`, and by assumption `Γ` and
|
||||
`Γ′` agree on all such variables; hence so do
|
||||
`Γ , y : A` and `Γ′ , y : A`.
|
||||
|
||||
- If the last rule was `⇒-E`, then `M = L · M`, with `Γ ⊢ L ∶ A ⇒ B`
|
||||
and `Γ ⊢ M ∶ B`. One induction hypothesis states that for all
|
||||
contexts `Γ′`, if `Γ′` agrees with `Γ` on the free variables in
|
||||
`L` then `L` has type `A ⇒ B` under `Γ′`; there is a similar IH
|
||||
for `M`. We must show that `L · M` also has type `B` under `Γ′`,
|
||||
given the assumption that `Γ′` agrees with `Γ` on all the free
|
||||
variables in `L · M`. By `⇒-E`, it suffices to show that `L` and
|
||||
`M` each have the same type under `Γ′` as under `Γ`. But all free
|
||||
variables in `L` are also free in `L · M`; in the proof, this is
|
||||
expressed by composing `free-·₁ : ∀ {x} → x ∈ L → x ∈ L · M` with
|
||||
`Γ~Γ′ : (∀ {x} → x ∈ L · M → Γ x ≡ Γ′ x)` to yield `Γ~Γ′ ∘ free-·₁
|
||||
: ∀ {x} → x ∈ L → Γ x ≡ Γ′ x`. Similarly for `M`; hence the
|
||||
desired result follows from the induction hypotheses.
|
||||
|
||||
- The remaining cases are similar to `⇒-E`.
|
||||
|
||||
\begin{code}
|
||||
context-lemma Γ~Γ′ (Ax Γx≡A) rewrite (Γ~Γ′ free-`) = Ax Γx≡A
|
||||
context-lemma {Γ} {Γ′} {λ[ x ∶ A ] N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (context-lemma Γx~Γ′x ⊢N)
|
||||
where
|
||||
Γx~Γ′x : ∀ {y} → y ∈ N → (Γ , x ∶ A) y ≡ (Γ′ , x ∶ A) y
|
||||
Γx~Γ′x {y} y∈N with x ≟ y
|
||||
... | yes refl = refl
|
||||
... | no x≢y = Γ~Γ′ (free-λ x≢y y∈N)
|
||||
context-lemma Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (context-lemma (Γ~Γ′ ∘ free-·₁) ⊢L)
|
||||
(context-lemma (Γ~Γ′ ∘ free-·₂) ⊢M)
|
||||
context-lemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
|
||||
context-lemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
|
||||
context-lemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (context-lemma (Γ~Γ′ ∘ free-if₁) ⊢L)
|
||||
(context-lemma (Γ~Γ′ ∘ free-if₂) ⊢M)
|
||||
(context-lemma (Γ~Γ′ ∘ free-if₃) ⊢N)
|
||||
\end{code}
|
||||
|
||||
|
||||
Now we come to the conceptual heart of the proof that reduction
|
||||
preserves types---namely, the observation that _substitution_
|
||||
preserves types.
|
||||
|
||||
Formally, the _Substitution Lemma_ says this: Suppose we
|
||||
have a term `N` with a free variable `x`, where `N` has
|
||||
type `B` under the assumption that `x` has some type `A`.
|
||||
Also, suppose that we have some other term `V`,
|
||||
where `V` has type `A`. Then, since `V` satisfies
|
||||
the assumption we made about `x` when typing `N`, we should be
|
||||
able to substitute `V` for each of the occurrences of `x` in `N`
|
||||
and obtain a new term that still has type `B`.
|
||||
|
||||
_Lemma_: If `Γ , x ∶ A ⊢ N ∶ B` and `∅ ⊢ V ∶ A`, then
|
||||
`Γ ⊢ (N [ x := V ]) ∶ B`.
|
||||
|
||||
\begin{code}
|
||||
preservation-[:=] : ∀ {Γ x A N B V}
|
||||
→ (Γ , x ∶ A) ⊢ N ∶ B
|
||||
→ ∅ ⊢ V ∶ A
|
||||
→ Γ ⊢ (N [ x := V ]) ∶ B
|
||||
\end{code}
|
||||
|
||||
One technical subtlety in the statement of the lemma is that we assume
|
||||
`V` is closed; it has type `A` in the _empty_ context. This
|
||||
assumption simplifies the `λ` case of the proof because the context
|
||||
invariance lemma then tells us that `V` has type `A` 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 `λ`. It is possible
|
||||
to prove the theorem under the more general assumption `Γ ⊢ V ∶ A`,
|
||||
but the proof is more difficult.
|
||||
|
||||
<!--
|
||||
Intuitively, the substitution lemma says that substitution and typing can
|
||||
be done in either order: we can either assign types to the terms
|
||||
`N` and `V` separately (under suitable contexts) and then combine
|
||||
them using substitution, or we can substitute first and then
|
||||
assign a type to `N [ x := V ]`---the result is the same either
|
||||
way.
|
||||
-->
|
||||
|
||||
_Proof_: By induction on the derivation of `Γ , x ∶ A ⊢ N ∶ B`,
|
||||
we show that if `∅ ⊢ V ∶ A` then `Γ ⊢ N [ x := V ] ∶ B`.
|
||||
|
||||
- If `N` is a variable there are two cases to consider,
|
||||
depending on whether `N` is `x` or some other variable.
|
||||
|
||||
- If `N = `` `x ``, then from `Γ , x ∶ A ⊢ x ∶ B`
|
||||
we know that looking up `x` in `Γ , x : A` gives
|
||||
`just B`, but we already know it gives `just A`;
|
||||
applying injectivity for `just` we conclude that `A ≡ B`.
|
||||
We must show that `x [ x := V] = V`
|
||||
has type `A` under `Γ`, given the assumption that
|
||||
`V` has type `A` under the empty context. This
|
||||
follows from context invariance: if a closed term has type
|
||||
`A` in the empty context, it has that type in any context.
|
||||
|
||||
- If `N` is some variable `x′` different from `x`, then
|
||||
we need only note that `x′` has the same type under `Γ , x ∶ A`
|
||||
as under `Γ`.
|
||||
|
||||
- If `N` is an abstraction `λ[ x′ ∶ A′ ] N′`, then the IH tells us,
|
||||
for all `Γ′`́ and `B′`, that if `Γ′ , x ∶ A ⊢ N′ ∶ B′`
|
||||
and `∅ ⊢ V ∶ A`, then `Γ′ ⊢ N′ [ x := V ] ∶ B′`.
|
||||
|
||||
The substitution in the conclusion behaves differently
|
||||
depending on whether `x` and `x′` are the same variable.
|
||||
|
||||
First, suppose `x ≡ x′`. Then, by the definition of
|
||||
substitution, `N [ x := V] = N`, so we just need to show `Γ ⊢ N ∶ B`.
|
||||
But we know `Γ , x ∶ A ⊢ N ∶ B` and, since `x ≡ x′`
|
||||
does not appear free in `λ[ x′ ∶ A′ ] N′`, the context invariance
|
||||
lemma yields `Γ ⊢ N ∶ B`.
|
||||
|
||||
Second, suppose `x ≢ x′`. We know `Γ , x ∶ A , x′ ∶ A′ ⊢ N′ ∶ B′`
|
||||
by inversion of the typing relation, from which
|
||||
`Γ , x′ ∶ A′ , x ∶ A ⊢ N′ ∶ B′` follows by update permute,
|
||||
so the IH applies, giving us `Γ , x′ ∶ A′ ⊢ N′ [ x := V ] ∶ B′`
|
||||
By `⇒-I`, we have `Γ ⊢ λ[ x′ ∶ A′ ] (N′ [ x := V ]) ∶ A′ ⇒ B′`
|
||||
and the definition of substitution (noting `x ≢ x′`) gives
|
||||
`Γ ⊢ (λ[ x′ ∶ A′ ] N′) [ x := V ] ∶ A′ ⇒ B′` as required.
|
||||
|
||||
- If `N` is an application `L′ · M′`, the result follows
|
||||
straightforwardly from the definition of substitution and the
|
||||
induction hypotheses.
|
||||
|
||||
- The remaining cases are similar to application.
|
||||
|
||||
We need a lemmas stating that a closed term can be weakened to any context.
|
||||
\begin{code}
|
||||
weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∶ A → Γ ⊢ V ∶ A
|
||||
weaken-closed {V} {A} {Γ} ⊢V = context-lemma Γ~Γ′ ⊢V
|
||||
where
|
||||
Γ~Γ′ : ∀ {x} → x ∈ V → ∅ x ≡ Γ x
|
||||
Γ~Γ′ {x} x∈V = ⊥-elim (x∉V x∈V)
|
||||
where
|
||||
x∉V : ¬ (x ∈ V)
|
||||
x∉V = ∅⊢-closed ⊢V {x}
|
||||
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
preservation-[:=] {Γ} {x} {A} (Ax {Γ,x∶A} {x′} {B} [Γ,x∶A]x′≡B) ⊢V with x ≟ x′
|
||||
...| yes x≡x′ rewrite just-injective [Γ,x∶A]x′≡B = weaken-closed ⊢V
|
||||
...| no x≢x′ = Ax [Γ,x∶A]x′≡B
|
||||
preservation-[:=] {Γ} {x} {A} {λ[ x′ ∶ A′ ] N′} {.A′ ⇒ B′} {V} (⇒-I ⊢N′) ⊢V with x ≟ x′
|
||||
...| yes x≡x′ rewrite x≡x′ = context-lemma Γ′~Γ (⇒-I ⊢N′)
|
||||
where
|
||||
Γ′~Γ : ∀ {y} → y ∈ (λ[ x′ ∶ A′ ] N′) → (Γ , x′ ∶ A) y ≡ Γ y
|
||||
Γ′~Γ {y} (free-λ x′≢y y∈N′) with x′ ≟ y
|
||||
...| yes x′≡y = ⊥-elim (x′≢y x′≡y)
|
||||
...| no _ = refl
|
||||
...| no x≢x′ = ⇒-I ⊢N′V
|
||||
where
|
||||
x′x⊢N′ : Γ , x′ ∶ A′ , x ∶ A ⊢ N′ ∶ B′
|
||||
x′x⊢N′ rewrite update-permute Γ x A x′ A′ x≢x′ = ⊢N′
|
||||
⊢N′V : (Γ , x′ ∶ A′) ⊢ N′ [ x := V ] ∶ B′
|
||||
⊢N′V = preservation-[:=] x′x⊢N′ ⊢V
|
||||
preservation-[:=] (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V)
|
||||
preservation-[:=] 𝔹-I₁ ⊢V = 𝔹-I₁
|
||||
preservation-[:=] 𝔹-I₂ ⊢V = 𝔹-I₂
|
||||
preservation-[:=] (𝔹-E ⊢L ⊢M ⊢N) ⊢V =
|
||||
𝔹-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V) (preservation-[:=] ⊢N ⊢V)
|
||||
\end{code}
|
||||
|
||||
|
||||
### Main Theorem
|
||||
|
||||
We now have the tools we need to prove preservation: if a closed
|
||||
term `M` has type `A` and takes a step to `N`, then `N`
|
||||
is also a closed term with type `A`. In other words, small-step
|
||||
reduction preserves types.
|
||||
|
||||
\begin{code}
|
||||
preservation : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹ N → ∅ ⊢ N ∶ A
|
||||
\end{code}
|
||||
|
||||
_Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
|
||||
|
||||
- We can immediately rule out `Ax`, `⇒-I`, `𝔹-I₁`, and
|
||||
`𝔹-I₂` as the final rules in the derivation, since in each of
|
||||
these cases `M` cannot take a step.
|
||||
|
||||
- If the last rule in the derivation was `⇒-E`, then `M = L · M`.
|
||||
There are three cases to consider, one for each rule that
|
||||
could have been used to show that `L · M` takes a step to `N`.
|
||||
|
||||
- If `L · M` takes a step by `ξ·₁`, with `L` stepping to
|
||||
`L′`, then by the IH `L′` has the same type as `L`, and
|
||||
hence `L′ · M` has the same type as `L · M`.
|
||||
|
||||
- The `ξ·₂` case is similar.
|
||||
|
||||
- If `L · M` takes a step by `β⇒`, then `L = λ[ x ∶ A ] N` and `M
|
||||
= V` and `L · M` steps to `N [ x := V]`; the desired result now
|
||||
follows from the fact that substitution preserves types.
|
||||
|
||||
- If the last rule in the derivation was `if`, then `M = if L
|
||||
then M else N`, and there are again three cases depending on
|
||||
how `if L then M else N` steps.
|
||||
|
||||
- If it steps via `β𝔹₁` or `βB₂`, the result is immediate, since
|
||||
`M` and `N` have the same type as `if L then M else N`.
|
||||
|
||||
- Otherwise, `L` steps by `ξif`, and the desired conclusion
|
||||
follows directly from the induction hypothesis.
|
||||
|
||||
\begin{code}
|
||||
preservation (Ax Γx≡A) ()
|
||||
preservation (⇒-I ⊢N) ()
|
||||
preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = preservation-[:=] ⊢N ⊢V
|
||||
preservation (⇒-E ⊢L ⊢M) (ξ·₁ L⟹L′) with preservation ⊢L L⟹L′
|
||||
...| ⊢L′ = ⇒-E ⊢L′ ⊢M
|
||||
preservation (⇒-E ⊢L ⊢M) (ξ·₂ valueL M⟹M′) with preservation ⊢M M⟹M′
|
||||
...| ⊢M′ = ⇒-E ⊢L ⊢M′
|
||||
preservation 𝔹-I₁ ()
|
||||
preservation 𝔹-I₂ ()
|
||||
preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) βif-true = ⊢M
|
||||
preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) βif-false = ⊢N
|
||||
preservation (𝔹-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′
|
||||
...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Exercise: 2 stars, recommended (subject_expansion_stlc)
|
||||
|
||||
<!--
|
||||
An exercise in the [Types]({{ "Types" | relative_url }}) chapter asked about the
|
||||
subject expansion property for the simple language of arithmetic and boolean
|
||||
expressions. Does this property hold for STLC? That is, is it always the case
|
||||
that, if `M ==> N` and `∅ ⊢ N ∶ A`, then `∅ ⊢ M ∶ A`? It is easy to find a
|
||||
counter-example with conditionals, find one not involving conditionals.
|
||||
-->
|
||||
|
||||
We say that `M` _reduces_ to `N` if `M ⟹ N`,
|
||||
and that `M` _expands_ to `N` if `N ⟹ M`.
|
||||
The preservation property is sometimes called _subject reduction_.
|
||||
Its opposite is _subject expansion_, which holds if
|
||||
`M ==> N` and `∅ ⊢ N ∶ A`, then `∅ ⊢ M ∶ A`.
|
||||
Find two counter-examples to subject expansion, one
|
||||
with conditionals and one not involving conditionals.
|
||||
|
||||
## Type Soundness
|
||||
|
||||
#### Exercise: 2 stars, optional (type_soundness)
|
||||
|
||||
Put progress and preservation together and show that a well-typed
|
||||
term can _never_ reach a stuck state.
|
||||
|
||||
\begin{code}
|
||||
Normal : Term → Set
|
||||
Normal M = ∀ {N} → ¬ (M ⟹ N)
|
||||
|
||||
Stuck : Term → Set
|
||||
Stuck M = Normal M × ¬ Value M
|
||||
|
||||
postulate
|
||||
Soundness : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹* N → ¬ (Stuck N)
|
||||
\end{code}
|
||||
|
||||
<div class="hidden">
|
||||
\begin{code}
|
||||
Soundness′ : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹* N → ¬ (Stuck N)
|
||||
Soundness′ ⊢M (M ∎) (¬M⟹N , ¬ValueM) with progress ⊢M
|
||||
... | steps M⟹N = ¬M⟹N M⟹N
|
||||
... | done ValueM = ¬ValueM ValueM
|
||||
Soundness′ {L} {N} {A} ⊢L (_⟹⟨_⟩_ .L {M} {.N} L⟹M M⟹*N) = Soundness′ ⊢M M⟹*N
|
||||
where
|
||||
⊢M : ∅ ⊢ M ∶ A
|
||||
⊢M = preservation ⊢L L⟹M
|
||||
\end{code}
|
||||
</div>
|
||||
|
||||
|
||||
## Uniqueness of Types
|
||||
|
||||
#### Exercise: 3 stars (types_unique)
|
||||
|
||||
Another nice property of the STLC is that types are unique: a
|
||||
given term (in a given context) has at most one type.
|
||||
Formalize this statement and prove it.
|
||||
|
||||
|
||||
## Additional Exercises
|
||||
|
||||
#### Exercise: 1 star (progress_preservation_statement)
|
||||
|
||||
Without peeking at their statements above, write down the progress
|
||||
and preservation theorems for the simply typed lambda-calculus.
|
||||
|
||||
#### Exercise: 2 stars (stlc_variation1)
|
||||
|
||||
Suppose we add a new term `zap` with the following reduction rule
|
||||
|
||||
--------- (ST_Zap)
|
||||
M ⟹ zap
|
||||
|
||||
and the following typing rule:
|
||||
|
||||
----------- (T_Zap)
|
||||
Γ ⊢ zap : A
|
||||
|
||||
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.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
|
||||
#### Exercise: 2 stars (stlc_variation2)
|
||||
|
||||
Suppose instead that we add a new term `foo` with the following
|
||||
reduction rules:
|
||||
|
||||
---------------------- (ST_Foo1)
|
||||
(λ[ x ∶ A ] ` x) ⟹ foo
|
||||
|
||||
----------- (ST_Foo2)
|
||||
foo ⟹ true
|
||||
|
||||
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.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
#### Exercise: 2 stars (stlc_variation3)
|
||||
|
||||
Suppose instead that we remove the rule `ξ·₁` from the `⟹`
|
||||
relation. Which of the following properties of the STLC remain
|
||||
true in the absence of this rule? For each one, write either
|
||||
"remains true" or else "becomes false." If a property becomes
|
||||
false, give a counterexample.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
#### Exercise: 2 stars, optional (stlc_variation4)
|
||||
Suppose instead that we add the following new rule to the
|
||||
reduction relation:
|
||||
|
||||
---------------------------------- (ST_FunnyIfTrue)
|
||||
(if true then t_1 else t_2) ⟹ true
|
||||
|
||||
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.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
|
||||
#### Exercise: 2 stars, optional (stlc_variation5)
|
||||
|
||||
Suppose instead that we add the following new rule to the typing
|
||||
relation:
|
||||
|
||||
Γ ⊢ L ∶ 𝔹 ⇒ 𝔹 ⇒ 𝔹
|
||||
Γ ⊢ M ∶ 𝔹
|
||||
------------------------------ (T_FunnyApp)
|
||||
Γ ⊢ L · M ∶ 𝔹
|
||||
|
||||
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.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
|
||||
|
||||
#### Exercise: 2 stars, optional (stlc_variation6)
|
||||
Suppose instead that we add the following new rule to the typing
|
||||
relation:
|
||||
|
||||
Γ ⊢ L ∶ 𝔹
|
||||
Γ ⊢ M ∶ 𝔹
|
||||
--------------------- (T_FunnyApp')
|
||||
Γ ⊢ L · M ∶ 𝔹
|
||||
|
||||
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.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
|
||||
|
||||
#### Exercise: 2 stars, optional (stlc_variation7)
|
||||
|
||||
Suppose we add the following new rule to the typing relation
|
||||
of the STLC:
|
||||
|
||||
-------------------- (T_FunnyAbs)
|
||||
∅ ⊢ λ[ x ∶ 𝔹 ] N ∶ 𝔹
|
||||
|
||||
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.
|
||||
|
||||
- Determinism of `step`
|
||||
|
||||
- Progress
|
||||
|
||||
- Preservation
|
||||
|
||||
|
||||
### Exercise: STLC with Arithmetic
|
||||
|
||||
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 numbers (and remove
|
||||
booleans, for brevity).
|
||||
|
||||
\begin{code}
|
||||
data Type′ : Set where
|
||||
_⇒_ : Type′ → Type′ → Type′
|
||||
ℕ : Type′
|
||||
\end{code}
|
||||
|
||||
To terms, we add natural number constants, along with
|
||||
plus, minus, and testing for zero.
|
||||
|
||||
\begin{code}
|
||||
data Term′ : Set where
|
||||
`_ : Id → Term′
|
||||
λ[_∶_]_ : Id → Type′ → Term′ → Term′
|
||||
_·_ : Term′ → Term′ → Term′
|
||||
#_ : Data.Nat.ℕ → Term′
|
||||
_+_ : Term′ → Term′ → Term′
|
||||
_-_ : Term′ → Term′ → Term′
|
||||
if0_then_else_ : Term′ → Term′ → Term′ → Term′
|
||||
\end{code}
|
||||
|
||||
(Assume that `m - n` returns `0` if `m` is less than `n`.)
|
||||
|
||||
#### Exercise: 4 stars (stlc_arith)
|
||||
|
||||
Finish formalizing the definition and properties of the STLC extended
|
||||
with arithmetic. Specifically:
|
||||
|
||||
- Copy the whole development of STLC that we went through above (from
|
||||
the definition of values through the Type Soundness theorem), and
|
||||
paste it into the file at this point.
|
||||
|
||||
- Extend the definitions of the `subst` operation and the `step`
|
||||
relation to include appropriate clauses for the arithmetic operators.
|
||||
|
||||
- Extend the proofs of all the properties (up to `soundness`) of
|
||||
the original STLC to deal with the new syntactic forms. Make
|
||||
sure Agda accepts the whole file.
|
||||
|
||||
|
|
@ -724,7 +724,11 @@ free-lemma (⊢Y ⊢M) w∈ = free-lemma ⊢M w∈
|
|||
### Substitution preserves types
|
||||
|
||||
\begin{code}
|
||||
-- trivial : Set
|
||||
-- trivial = ∀ ρ x → ρ x ≡ ` x ⊎ closed (ρ x)
|
||||
|
||||
⊢subst : ∀ {Γ Δ ρ}
|
||||
-- → (∀ {x A} → Γ ∋ x `: A → trivial ρ x)
|
||||
→ (∀ {x A} → Γ ∋ x `: A → Δ ⊢ ρ x `: A)
|
||||
-------------------------------------------------
|
||||
→ (∀ {M A} → Γ ⊢ M `: A → Δ ⊢ subst ρ M `: A)
|
||||
|
|
@ -762,13 +766,18 @@ Let's look at examples. Assume `M` is closed. Example 1.
|
|||
|
||||
Example 2.
|
||||
|
||||
subst (∅ , "y" ↦ ` "y" , "x" ↦ M) (`λ "y" `→ ` "x" · ` "y")
|
||||
subst (∅ , "y" ↦ N , "x" ↦ M) (`λ "y" `→ ` "x" · ` "y")
|
||||
≡
|
||||
`λ "y" `→ subst (∅ , "y" ↦ ` "y" , "x" ↦ M , "y" ↦ ` "y") (` "x" · ` "y")
|
||||
`λ "y" `→ subst (∅ , "y" ↦ ` N , "x" ↦ M , "y" ↦ ` "y") (` "x" · ` "y")
|
||||
≡
|
||||
`λ "y" `→ (M · ` "y")
|
||||
|
||||
The hypotheses of the theorem appear to be violated. Drat!
|
||||
Before I wrote: "The hypotheses of the theorem appear to be violated. Drat!"
|
||||
But let's assume that ``M `: A``, ``N `: B``, and the lambda bound `y` has type `C`.
|
||||
Then ``Γ ∋ y `: B`` will not hold for the extended `ρ` because of interference
|
||||
by the earlier `y`. So I'm not sure the hypothesis is violated.
|
||||
|
||||
|
||||
|
||||
\begin{code}
|
||||
⊢substitution : ∀ {Γ x A N B M}
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ a fresh name whenever substituting for a lambda term.
|
|||
## Imports
|
||||
|
||||
\begin{code}
|
||||
module TypedFresh where
|
||||
module fresh.TypedFresh where
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
|
|
|
|||
Loading…
Reference in a new issue