ReferencesTyping Mutable References
(* $Date: 2013-07-17 16:19:11 -0400 (Wed, 17 Jul 2013) $ *)
Require Export Smallstep.
Most real languages include impure
features ("computational effects")...
Goal for this chapter formalize pointers.
- mutable pointer structures
- non-local control constructs (exceptions, continuations, etc.)
- process synchronization and communication
- etc.
Definitions
- keep the mechanisms for name binding (abstraction, let) the same;
- introduce new, explicit operations for allocating, changing, and looking up the contents of references (pointers).
Module STLCRef.
The basic operations on references are allocation,
dereferencing, and assignment.
- To allocate a reference, we use the ref operator, providing
an initial value for the new cell. For example, ref 5
creates a new cell containing the value 5, and evaluates to
a reference to that cell.
- To read the current value of this cell, we use the
dereferencing operator !; for example, !(ref 5) evaluates
to 5.
- To change the value stored in a cell, we use the assignment operator. If r is a reference, r := 7 will store the value 7 in the cell referenced by r. However, r := 7 evaluates to the trivial value unit; it exists only to have the side effect of modifying the contents of a cell.
Types
T ::= Nat
| Unit
| T → T
| Ref T
| Unit
| T → T
| Ref T
Inductive ty : Type :=
| TNat : ty
| TUnit : ty
| TArrow : ty → ty → ty
| TRef : ty → ty.
Terms
t ::= ... Terms | ref t allocation | !t dereference | t := t assignment | l location
Inductive tm : Type :=
(* STLC with numbers: *)
| tvar : id → tm
| tapp : tm → tm → tm
| tabs : id → ty → tm → tm
| tnat : nat → tm
| tsucc : tm → tm
| tpred : tm → tm
| tmult : tm → tm → tm
| tif0 : tm → tm → tm → tm
(* New terms: *)
| tunit : tm
| tref : tm → tm
| tderef : tm → tm
| tassign : tm → tm → tm
| tloc : nat → tm.
Tactic Notation "t_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "tvar" | Case_aux c "tapp"
| Case_aux c "tabs" | Case_aux c "tzero"
| Case_aux c "tsucc" | Case_aux c "tpred"
| Case_aux c "tmult" | Case_aux c "tif0"
| Case_aux c "tunit" | Case_aux c "tref"
| Case_aux c "tderef" | Case_aux c "tassign"
| Case_aux c "tloc" ].
Module ExampleVariables.
Definition x := Id 0.
Definition y := Id 1.
Definition r := Id 2.
Definition s := Id 3.
End ExampleVariables.
Typing (Preview)
Γ ⊢ t1 : T1 | (T_Ref) |
Γ ⊢ ref t1 : Ref T1 |
Γ ⊢ t1 : Ref T11 | (T_Deref) |
Γ ⊢ !t1 : T11 |
Γ ⊢ t1 : Ref T11 | |
Γ ⊢ t2 : T11 | (T_Assign) |
Γ ⊢ t1 := t2 : Unit |
Values and Substitution
Inductive value : tm → Prop :=
| v_abs : ∀x T t,
value (tabs x T t)
| v_nat : ∀n,
value (tnat n)
| v_unit :
value tunit
| v_loc : ∀l,
value (tloc l).
Hint Constructors value.
Extending substitution to handle the new syntax of terms is
straightforward.
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tvar x' ⇒
if eq_id_dec x x' then s else t
| tapp t1 t2 ⇒
tapp (subst x s t1) (subst x s t2)
| tabs x' T t1 ⇒
if eq_id_dec x x' then t else tabs x' T (subst x s t1)
| tnat n ⇒
t
| tsucc t1 ⇒
tsucc (subst x s t1)
| tpred t1 ⇒
tpred (subst x s t1)
| tmult t1 t2 ⇒
tmult (subst x s t1) (subst x s t2)
| tif0 t1 t2 t3 ⇒
tif0 (subst x s t1) (subst x s t2) (subst x s t3)
| tunit ⇒
t
| tref t1 ⇒
tref (subst x s t1)
| tderef t1 ⇒
tderef (subst x s t1)
| tassign t1 t2 ⇒
tassign (subst x s t1) (subst x s t2)
| tloc _ ⇒
t
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
Side Effects and Sequencing
r:=succ(!r); !ras an abbreviation for
(λx:Unit. !r) (r := succ(!r)).
Definition tseq t1 t2 :=
tapp (tabs (Id 0) TUnit t2) t1.
References and Aliasing
let r = ref 5 in let s = r in s := 82; (!r)+1the cell referenced by r will contain the value 82, while the result of the whole expression will be 83. The references r and s are said to be aliases for the same cell.
r := 5; r := !sassigns 5 to r and then immediately overwrites it with s's current value; this has exactly the same effect as the single assignment
r := !sunless we happen to do it in a context where r and s are aliases for the same cell!
Shared State
let c = ref 0 in let incc = λ_:Unit. (c := succ (!c); !c) in let decc = λ_:Unit. (c := pred (!c); !c) in ...
Objects
newcounter = λ_:Unit. let c = ref 0 in let incc = λ_:Unit. (c := succ (!c); !c) in let decc = λ_:Unit. (c := pred (!c); !c) in {i=incc, d=decc}Now, each time we call newcounter, we get a new record of functions that share access to the same storage cell c. The caller of newcounter can't get at this storage cell directly, but can affect it indirectly by calling the two functions. In other words, we've created a simple form of object.
let c1 = newcounter unit in let c2 = newcounter unit in // Note that we've allocated two separate storage cells now! let r1 = c1.i unit in let r2 = c2.i unit in r2 // yields 1, not 2!
References to Compound Types
equal = fix (λeq:Nat->Nat->Bool. λm:Nat. λn:Nat. if m=0 then iszero n else if n=0 then false else eq (pred m) (pred n))Now, to build a new array, we allocate a reference cell and fill it with a function that, when given an index, always returns 0.
newarray = λ_:Unit. ref (λn:Nat.0)To look up an element of an array, we simply apply the function to the desired index.
lookup = λa:NatArray. λn:Nat. (!a) nThe interesting part of the encoding is the update function. It takes an array, an index, and a new value to be stored at that index, and does its job by creating (and storing in the reference) a new function that, when it is asked for the value at this very index, returns the new value that was given to update, and on all other indices passes the lookup to the function that was previously stored in the reference.
update = λa:NatArray. λm:Nat. λv:Nat. let oldf = !a in a := (λn:Nat. if equal m n then v else oldf n);References to values containing other references can also be very useful, allowing us to define data structures such as mutable lists and trees.
Null References
- in C, a pointer variable can contain either a valid pointer
into the heap or the special value NULL
- source of many errors and much tricky reasoning
- (any pointer may potentially be "not there")
- but occasionally useful
- easy to implement here using references plus options (which
can be built out of disjoint sum types)
Option T = Unit + T NullableRef T = Option (Ref T)
Garbage Collection
Exercise: 1 star (type_safety_violation)
Show how this can lead to a violation of type safety.(* FILL IN HERE *)
☐
Locations
- Concretely: An array of 8-bit bytes, indexed by 32-bit integers.
- More abstractly: a list (or array) of values
- Even more abstractly: a partial function from locations to values.
Stores
Definition store := list tm.
We use store_lookup n st to retrieve the value of the reference
cell at location n in the store st. Note that we must give a
default value to nth in case we try looking up an index which is
too large. (In fact, we will never actually do this, but proving
it will of course require some work!)
Definition store_lookup (n:nat) (st:store) :=
nth n st tunit.
To add a new reference cell to the store, we use snoc.
Fixpoint snoc {A:Type} (l:list A) (x:A) : list A :=
match l with
| nil ⇒ x :: nil
| h :: t ⇒ h :: snoc t x
end.
Lemma length_snoc : ∀A (l:list A) x,
length (snoc l x) = S (length l).
Proof.
(* ELIDED *) Admitted.
Lemma nth_lt_snoc : ∀A (l:list A) x d n,
n < length l →
nth n l d = nth n (snoc l x) d.
Proof.
(* ELIDED *) Admitted.
Lemma nth_eq_snoc : ∀A (l:list A) x d,
nth (length l) (snoc l x) d = x.
Proof.
(* ELIDED *) Admitted.
To update the store, we use the replace function, which replaces
the contents of a cell at a particular index.
Fixpoint replace {A:Type} (n:nat) (x:A) (l:list A) : list A :=
match l with
| nil ⇒ nil
| h :: t ⇒
match n with
| O ⇒ x :: t
| S n' ⇒ h :: replace n' x t
end
end.
Lemma replace_nil : ∀A n (x:A),
replace n x nil = nil.
Proof.
(* ELIDED *) Admitted.
Lemma length_replace : ∀A n x (l:list A),
length (replace n x l) = length l.
Proof with auto.
(* ELIDED *) Admitted.
Lemma lookup_replace_eq : ∀l t st,
l < length st →
store_lookup l (replace l t st) = t.
Proof with auto.
(* ELIDED *) Admitted.
Lemma lookup_replace_neq : ∀l1 l2 t st,
l1 ≠ l2 →
store_lookup l1 (replace l2 t st) = store_lookup l1 st.
Proof with auto.
(* ELIDED *) Admitted.
Reduction
value v2 | (ST_AppAbs) |
(λa:T.t12) v2 / st ⇒ [a:=v2]t12 / st |
t1 / st ⇒ t1' / st' | (ST_App1) |
t1 t2 / st ⇒ t1' t2 / st' |
value v1 t2 / st ⇒ t2' / st' | (ST_App2) |
v1 t2 / st ⇒ v1 t2' / st' |
(ST_RefValue) | |
ref v1 / st ⇒ loc |st| / st,v1 |
t1 / st ⇒ t1' / st' | (ST_Ref) |
ref t1 / st ⇒ ref t1' / st' |
l < |st| | (ST_DerefLoc) |
!(loc l) / st ⇒ lookup l st / st |
t1 / st ⇒ t1' / st' | (ST_Deref) |
!t1 / st ⇒ !t1' / st' |
l < |st| | (ST_Assign) |
loc l := v2 / st ⇒ unit / replace l v2 st |
t1 / st ⇒ t1' / st' | (ST_Assign1) |
t1 := t2 / st ⇒ t1' := t2 / st' |
t2 / st ⇒ t2' / st' | (ST_Assign2) |
v1 := t2 / st ⇒ v1 := t2' / st' |
Reserved Notation "t1 '/' st1 '⇒' t2 '/' st2"
(at level 40, st1 at level 39, t2 at level 39).
Inductive step : tm × store → tm × store → Prop :=
| ST_AppAbs : ∀x T t12 v2 st,
value v2 →
tapp (tabs x T t12) v2 / st ⇒ [x:=v2]t12 / st
| ST_App1 : ∀t1 t1' t2 st st',
t1 / st ⇒ t1' / st' →
tapp t1 t2 / st ⇒ tapp t1' t2 / st'
| ST_App2 : ∀v1 t2 t2' st st',
value v1 →
t2 / st ⇒ t2' / st' →
tapp v1 t2 / st ⇒ tapp v1 t2'/ st'
| ST_SuccNat : ∀n st,
tsucc (tnat n) / st ⇒ tnat (S n) / st
| ST_Succ : ∀t1 t1' st st',
t1 / st ⇒ t1' / st' →
tsucc t1 / st ⇒ tsucc t1' / st'
| ST_PredNat : ∀n st,
tpred (tnat n) / st ⇒ tnat (pred n) / st
| ST_Pred : ∀t1 t1' st st',
t1 / st ⇒ t1' / st' →
tpred t1 / st ⇒ tpred t1' / st'
| ST_MultNats : ∀n1 n2 st,
tmult (tnat n1) (tnat n2) / st ⇒ tnat (mult n1 n2) / st
| ST_Mult1 : ∀t1 t2 t1' st st',
t1 / st ⇒ t1' / st' →
tmult t1 t2 / st ⇒ tmult t1' t2 / st'
| ST_Mult2 : ∀v1 t2 t2' st st',
value v1 →
t2 / st ⇒ t2' / st' →
tmult v1 t2 / st ⇒ tmult v1 t2' / st'
| ST_If0 : ∀t1 t1' t2 t3 st st',
t1 / st ⇒ t1' / st' →
tif0 t1 t2 t3 / st ⇒ tif0 t1' t2 t3 / st'
| ST_If0_Zero : ∀t2 t3 st,
tif0 (tnat 0) t2 t3 / st ⇒ t2 / st
| ST_If0_Nonzero : ∀n t2 t3 st,
tif0 (tnat (S n)) t2 t3 / st ⇒ t3 / st
| ST_RefValue : ∀v1 st,
value v1 →
tref v1 / st ⇒ tloc (length st) / snoc st v1
| ST_Ref : ∀t1 t1' st st',
t1 / st ⇒ t1' / st' →
tref t1 / st ⇒ tref t1' / st'
| ST_DerefLoc : ∀st l,
l < length st →
tderef (tloc l) / st ⇒ store_lookup l st / st
| ST_Deref : ∀t1 t1' st st',
t1 / st ⇒ t1' / st' →
tderef t1 / st ⇒ tderef t1' / st'
| ST_Assign : ∀v2 l st,
value v2 →
l < length st →
tassign (tloc l) v2 / st ⇒ tunit / replace l v2 st
| ST_Assign1 : ∀t1 t1' t2 st st',
t1 / st ⇒ t1' / st' →
tassign t1 t2 / st ⇒ tassign t1' t2 / st'
| ST_Assign2 : ∀v1 t2 t2' st st',
value v1 →
t2 / st ⇒ t2' / st' →
tassign v1 t2 / st ⇒ tassign v1 t2' / st'
where "t1 '/' st1 '⇒' t2 '/' st2" := (step (t1,st1) (t2,st2)).
Tactic Notation "step_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "ST_AppAbs" | Case_aux c "ST_App1"
| Case_aux c "ST_App2" | Case_aux c "ST_SuccNat"
| Case_aux c "ST_Succ" | Case_aux c "ST_PredNat"
| Case_aux c "ST_Pred" | Case_aux c "ST_MultNats"
| Case_aux c "ST_Mult1" | Case_aux c "ST_Mult2"
| Case_aux c "ST_If0" | Case_aux c "ST_If0_Zero"
| Case_aux c "ST_If0_Nonzero" | Case_aux c "ST_RefValue"
| Case_aux c "ST_Ref" | Case_aux c "ST_DerefLoc"
| Case_aux c "ST_Deref" | Case_aux c "ST_Assign"
| Case_aux c "ST_Assign1" | Case_aux c "ST_Assign2" ].
Hint Constructors step.
Definition multistep := (multi step).
Notation "t1 '/' st '⇒*' t2 '/' st'" := (multistep (t1,st) (t2,st'))
(at level 40, st at level 39, t2 at level 39).
Typing
Definition context := partial_map ty.
Store typings
Γ ⊢ lookup l st : T1 | |
Γ ⊢ loc l : Ref T1 |
Gamma; st ⊢ lookup l st : T1 | |
Gamma; st ⊢ loc l : Ref T1 |
[λx:Nat. (!(loc 1)) x, λx:Nat. (!(loc 0)) x]
Exercise: 2 stars (cyclic_store)
Can you find a term whose evaluation will create this particular cyclic store?Definition store_ty := list ty.
The store_Tlookup function retrieves the type at a particular
index.
Definition store_Tlookup (n:nat) (ST:store_ty) :=
nth n ST TUnit.
Suppose we are given a store typing ST describing the store
st in which some term t will be evaluated. Then we can use
ST to calculate the type of the result of t without ever
looking directly at st. For example, if ST is [Unit,
Unit→Unit], then we may immediately infer that !(loc 1) has
type Unit→Unit. More generally, the typing rule for locations
can be reformulated in terms of store typings like this:
That is, as long as l is a valid location (it is less than the
length of ST), we can compute the type of l just by looking it
up in ST. Typing is again a four-place relation, but it is
parameterized on a store typing rather than a concrete store.
The rest of the typing rules are analogously augmented with store
typings.
l < |ST| | |
Gamma; ST ⊢ loc l : Ref (lookup l ST) |
The Typing Relation
l < |ST| | (T_Loc) |
Gamma; ST ⊢ loc l : Ref (lookup l ST) |
Gamma; ST ⊢ t1 : T1 | (T_Ref) |
Gamma; ST ⊢ ref t1 : Ref T1 |
Gamma; ST ⊢ t1 : Ref T11 | (T_Deref) |
Gamma; ST ⊢ !t1 : T11 |
Gamma; ST ⊢ t1 : Ref T11 | |
Gamma; ST ⊢ t2 : T11 | (T_Assign) |
Gamma; ST ⊢ t1 := t2 : Unit |
Reserved Notation "Gamma ';' ST '⊢' t '∈' T" (at level 40).
Inductive has_type : context → store_ty → tm → ty → Prop :=
| T_Var : ∀Γ ST x T,
Γ x = Some T →
Γ; ST ⊢ (tvar x) ∈ T
| T_Abs : ∀Γ ST x T11 T12 t12,
(extend Γ x T11); ST ⊢ t12 ∈ T12 →
Γ; ST ⊢ (tabs x T11 t12) ∈ (TArrow T11 T12)
| T_App : ∀T1 T2 Γ ST t1 t2,
Γ; ST ⊢ t1 ∈ (TArrow T1 T2) →
Γ; ST ⊢ t2 ∈ T1 →
Γ; ST ⊢ (tapp t1 t2) ∈ T2
| T_Nat : ∀Γ ST n,
Γ; ST ⊢ (tnat n) ∈ TNat
| T_Succ : ∀Γ ST t1,
Γ; ST ⊢ t1 ∈ TNat →
Γ; ST ⊢ (tsucc t1) ∈ TNat
| T_Pred : ∀Γ ST t1,
Γ; ST ⊢ t1 ∈ TNat →
Γ; ST ⊢ (tpred t1) ∈ TNat
| T_Mult : ∀Γ ST t1 t2,
Γ; ST ⊢ t1 ∈ TNat →
Γ; ST ⊢ t2 ∈ TNat →
Γ; ST ⊢ (tmult t1 t2) ∈ TNat
| T_If0 : ∀Γ ST t1 t2 t3 T,
Γ; ST ⊢ t1 ∈ TNat →
Γ; ST ⊢ t2 ∈ T →
Γ; ST ⊢ t3 ∈ T →
Γ; ST ⊢ (tif0 t1 t2 t3) ∈ T
| T_Unit : ∀Γ ST,
Γ; ST ⊢ tunit ∈ TUnit
| T_Loc : ∀Γ ST l,
l < length ST →
Γ; ST ⊢ (tloc l) ∈ (TRef (store_Tlookup l ST))
| T_Ref : ∀Γ ST t1 T1,
Γ; ST ⊢ t1 ∈ T1 →
Γ; ST ⊢ (tref t1) ∈ (TRef T1)
| T_Deref : ∀Γ ST t1 T11,
Γ; ST ⊢ t1 ∈ (TRef T11) →
Γ; ST ⊢ (tderef t1) ∈ T11
| T_Assign : ∀Γ ST t1 t2 T11,
Γ; ST ⊢ t1 ∈ (TRef T11) →
Γ; ST ⊢ t2 ∈ T11 →
Γ; ST ⊢ (tassign t1 t2) ∈ TUnit
where "Gamma ';' ST '⊢' t '∈' T" := (has_type Γ ST t T).
Hint Constructors has_type.
Tactic Notation "has_type_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "T_Var" | Case_aux c "T_Abs" | Case_aux c "T_App"
| Case_aux c "T_Nat" | Case_aux c "T_Succ" | Case_aux c "T_Pred"
| Case_aux c "T_Mult" | Case_aux c "T_If0"
| Case_aux c "T_Unit" | Case_aux c "T_Loc"
| Case_aux c "T_Ref" | Case_aux c "T_Deref"
| Case_aux c "T_Assign" ].
Of course, these typing rules will accurately predict the results
of evaluation only if the concrete store used during evaluation
actually conforms to the store typing that we assume for purposes
of typechecking. This proviso exactly parallels the situation
with free variables in the STLC: the substitution lemma promises
us that, if Γ ⊢ t : T, then we can replace the free
variables in t with values of the types listed in Γ to
obtain a closed term of type T, which, by the type preservation
theorem will evaluate to a final result of type T if it yields
any result at all. (We will see later how to formalize an
analogous intuition for stores and store typings.)
However, for purposes of typechecking the terms that programmers
actually write, we do not need to do anything tricky to guess what
store typing we should use. Recall that concrete location
constants arise only in terms that are the intermediate results of
evaluation; they are not in the language that programmers write.
Thus, we can simply typecheck the programmer's terms with respect
to the empty store typing. As evaluation proceeds and new
locations are created, we will always be able to see how to extend
the store typing by looking at the type of the initial values
being placed in newly allocated cells; this intuition is
formalized in the statement of the type preservation theorem
below.
Properties
- Progress — pretty much same as always
- Preservation — needs to be stated more carefully!
Well-Typed Stores
Theorem preservation_wrong1 : ∀ST T t st t' st',
empty; ST ⊢ t ∈ T →
t / st ⇒ t' / st' →
empty; ST ⊢ t' ∈ T.
Abort.
Obviously wrong: no relation between assumed store typing
and provided store!
We need a way of saying "this store satisfies the assumptions of
that store typing"...
Definition store_well_typed (ST:store_ty) (st:store) :=
length ST = length st ∧
(∀l, l < length st →
empty; ST ⊢ (store_lookup l st) ∈ (store_Tlookup l ST)).
Informally, we will write ST ⊢ st for store_well_typed ST st.
We can now state something closer to the desired preservation
property:
Theorem preservation_wrong2 : ∀ST T t st t' st',
empty; ST ⊢ t ∈ T →
t / st ⇒ t' / st' →
store_well_typed ST st →
empty; ST ⊢ t' ∈ T.
Abort.
This works... for all but one of the evaluation rules!
Extending Store Typings
Inductive extends : store_ty → store_ty → Prop :=
| extends_nil : ∀ST',
extends ST' nil
| extends_cons : ∀x ST' ST,
extends ST' ST →
extends (x::ST') (x::ST).
Hint Constructors extends.
We'll need a few technical lemmas about extended contexts.
First, looking up a type in an extended store typing yields the
same result as in the original:
Lemma extends_lookup : ∀l ST ST',
l < length ST →
extends ST' ST →
store_Tlookup l ST' = store_Tlookup l ST.
Proof with auto.
(* ELIDED *) Admitted.
Next, if ST' extends ST, the length of ST' is at least that
of ST.
Lemma length_extends : ∀l ST ST',
l < length ST →
extends ST' ST →
l < length ST'.
Proof with eauto.
(* ELIDED *) Admitted.
Finally, snoc ST T extends ST, and extends is reflexive.
Lemma extends_snoc : ∀ST T,
extends (snoc ST T) ST.
Proof with auto.
(* ELIDED *) Admitted.
Lemma extends_refl : ∀ST,
extends ST ST.
Proof.
(* ELIDED *) Admitted.
Preservation, Finally
Definition preservation_theorem := ∀ST t t' T st st',
empty; ST ⊢ t ∈ T →
store_well_typed ST st →
t / st ⇒ t' / st' →
∃ST',
(extends ST' ST ∧
empty; ST' ⊢ t' ∈ T ∧
store_well_typed ST' st').
Note that this gives us just what we need to "turn the
crank" when applying the theorem to multi-step reduction
sequences.
Substitution lemma
Inductive appears_free_in : id → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (tvar x)
| afi_app1 : ∀x t1 t2,
appears_free_in x t1 → appears_free_in x (tapp t1 t2)
| afi_app2 : ∀x t1 t2,
appears_free_in x t2 → appears_free_in x (tapp t1 t2)
| afi_abs : ∀x y T11 t12,
y ≠ x →
appears_free_in x t12 →
appears_free_in x (tabs y T11 t12)
| afi_succ : ∀x t1,
appears_free_in x t1 →
appears_free_in x (tsucc t1)
| afi_pred : ∀x t1,
appears_free_in x t1 →
appears_free_in x (tpred t1)
| afi_mult1 : ∀x t1 t2,
appears_free_in x t1 →
appears_free_in x (tmult t1 t2)
| afi_mult2 : ∀x t1 t2,
appears_free_in x t2 →
appears_free_in x (tmult t1 t2)
| afi_if0_1 : ∀x t1 t2 t3,
appears_free_in x t1 →
appears_free_in x (tif0 t1 t2 t3)
| afi_if0_2 : ∀x t1 t2 t3,
appears_free_in x t2 →
appears_free_in x (tif0 t1 t2 t3)
| afi_if0_3 : ∀x t1 t2 t3,
appears_free_in x t3 →
appears_free_in x (tif0 t1 t2 t3)
| afi_ref : ∀x t1,
appears_free_in x t1 → appears_free_in x (tref t1)
| afi_deref : ∀x t1,
appears_free_in x t1 → appears_free_in x (tderef t1)
| afi_assign1 : ∀x t1 t2,
appears_free_in x t1 → appears_free_in x (tassign t1 t2)
| afi_assign2 : ∀x t1 t2,
appears_free_in x t2 → appears_free_in x (tassign t1 t2).
Tactic Notation "afi_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "afi_var"
| Case_aux c "afi_app1" | Case_aux c "afi_app2" | Case_aux c "afi_abs"
| Case_aux c "afi_succ" | Case_aux c "afi_pred"
| Case_aux c "afi_mult1" | Case_aux c "afi_mult2"
| Case_aux c "afi_if0_1" | Case_aux c "afi_if0_2" | Case_aux c "afi_if0_3"
| Case_aux c "afi_ref" | Case_aux c "afi_deref"
| Case_aux c "afi_assign1" | Case_aux c "afi_assign2" ].
Hint Constructors appears_free_in.
Lemma free_in_context : ∀x t T Γ ST,
appears_free_in x t →
Γ; ST ⊢ t ∈ T →
∃T', Γ x = Some T'.
Proof with eauto.
intros. generalize dependent Γ. generalize dependent T.
afi_cases (induction H) Case;
intros; (try solve [ inversion H0; subst; eauto ]).
Case "afi_abs".
inversion H1; subst.
apply IHappears_free_in in H8.
rewrite extend_neq in H8; assumption.
Qed.
Lemma context_invariance : ∀Γ Γ' ST t T,
Γ; ST ⊢ t ∈ T →
(∀x, appears_free_in x t → Γ x = Γ' x) →
Γ'; ST ⊢ t ∈ T.
Proof with eauto.
intros.
generalize dependent Γ'.
has_type_cases (induction H) Case; intros...
Case "T_Var".
apply T_Var. symmetry. rewrite ← H...
Case "T_Abs".
apply T_Abs. apply IHhas_type; intros.
unfold extend.
destruct (eq_id_dec x x0)...
Case "T_App".
eapply T_App.
apply IHhas_type1...
apply IHhas_type2...
Case "T_Mult".
eapply T_Mult.
apply IHhas_type1...
apply IHhas_type2...
Case "T_If0".
eapply T_If0.
apply IHhas_type1...
apply IHhas_type2...
apply IHhas_type3...
Case "T_Assign".
eapply T_Assign.
apply IHhas_type1...
apply IHhas_type2...
Qed.
Lemma substitution_preserves_typing : ∀Γ ST x s S t T,
empty; ST ⊢ s ∈ S →
(extend Γ x S); ST ⊢ t ∈ T →
Γ; ST ⊢ ([x:=s]t) ∈ T.
Proof with eauto.
intros Γ ST x s S t T Hs Ht.
generalize dependent Γ. generalize dependent T.
t_cases (induction t) Case; intros T Γ H;
inversion H; subst; simpl...
Case "tvar".
rename i into y.
destruct (eq_id_dec x y).
SCase "x = y".
subst.
rewrite extend_eq in H3.
inversion H3; subst.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ _ _ _ Hcontra Hs) as [T' HT'].
inversion HT'.
SCase "x ≠ y".
apply T_Var.
rewrite extend_neq in H3...
Case "tabs". subst.
rename i into y.
destruct (eq_id_dec x y).
SCase "x = y".
subst.
apply T_Abs. eapply context_invariance...
intros. apply extend_shadow.
SCase "x ≠ x0".
apply T_Abs. apply IHt.
eapply context_invariance...
intros. unfold extend.
destruct (eq_id_dec y x0)...
subst.
rewrite neq_id...
Qed.
Assignment Preserves Store Typing
Lemma assign_pres_store_typing : ∀ST st l t,
l < length st →
store_well_typed ST st →
empty; ST ⊢ t ∈ (store_Tlookup l ST) →
store_well_typed ST (replace l t st).
Proof with auto.
intros ST st l t Hlen HST Ht.
inversion HST; subst.
split. rewrite length_replace...
intros l' Hl'.
destruct (beq_nat l' l) eqn: Heqll'.
Case "l' = l".
apply beq_nat_true in Heqll'; subst.
rewrite lookup_replace_eq...
Case "l' ≠ l".
apply beq_nat_false in Heqll'.
rewrite lookup_replace_neq...
rewrite length_replace in Hl'.
apply H0...
Qed.
Weakening for Stores
Lemma store_weakening : ∀Γ ST ST' t T,
extends ST' ST →
Γ; ST ⊢ t ∈ T →
Γ; ST' ⊢ t ∈ T.
Proof with eauto.
intros. has_type_cases (induction H0) Case; eauto.
Case "T_Loc".
erewrite ← extends_lookup...
apply T_Loc.
eapply length_extends...
Qed.
We can use the store_weakening lemma to prove that if a store is
well typed with respect to a store typing, then the store extended
with a new term t will still be well typed with respect to the
store typing extended with t's type.
Lemma store_well_typed_snoc : ∀ST st t1 T1,
store_well_typed ST st →
empty; ST ⊢ t1 ∈ T1 →
store_well_typed (snoc ST T1) (snoc st t1).
Proof with auto.
intros.
unfold store_well_typed in ×.
inversion H as [Hlen Hmatch]; clear H.
rewrite !length_snoc.
split...
Case "types match.".
intros l Hl.
unfold store_lookup, store_Tlookup.
apply le_lt_eq_dec in Hl; inversion Hl as [Hlt | Heq].
SCase "l < length st".
apply lt_S_n in Hlt.
rewrite ← !nth_lt_snoc...
apply store_weakening with ST. apply extends_snoc.
apply Hmatch...
rewrite Hlen...
SCase "l = length st".
inversion Heq.
rewrite nth_eq_snoc.
rewrite ← Hlen. rewrite nth_eq_snoc...
apply store_weakening with ST... apply extends_snoc.
Qed.
Preservation!
Theorem preservation : ∀ST t t' T st st',
empty; ST ⊢ t ∈ T →
store_well_typed ST st →
t / st ⇒ t' / st' →
∃ST',
(extends ST' ST ∧
empty; ST' ⊢ t' ∈ T ∧
store_well_typed ST' st').
Proof with eauto using store_weakening, extends_refl.
(* ELIDED *) Admitted.
Exercise: 3 stars (preservation_informal)
Write a careful informal proof of the preservation theorem, concentrating on the T_App, T_Deref, T_Assign, and T_Ref cases.☐
Progress
Theorem progress : ∀ST t T st,
empty; ST ⊢ t ∈ T →
store_well_typed ST st →
(value t ∨ ∃t', ∃st', t / st ⇒ t' / st').
Proof with eauto.
(* ELIDED *) Admitted.
Section RefsAndNontermination.
Import ExampleVariables.
We know that the simply typed lambda calculus is normalizing,
that is, every well-typed term can be reduced to a value in a
finite number of steps. What about STLC + references?
Surprisingly, adding references causes us to lose the
normalization property: there exist well-typed terms in the STLC +
references which can continue to reduce forever, without ever
reaching a normal form!
How can we construct such a term? The main idea is to make a
function which calls itself. We first make a function which calls
another function stored in a reference cell; the trick is that we
then smuggle in a reference to itself!
First, ref (λx:Unit.unit) creates a reference to a cell of type
Unit → Unit. We then pass this reference as the argument to a
function which binds it to the name r, and assigns to it the
function (λx:Unit.(!r) unit) — that is, the function which
ignores its argument and calls the function stored in r on the
argument unit; but of course, that function is itself! To get
the ball rolling we finally execute this function with (!r)
unit.
(λr:Ref (Unit -> Unit). r := (λx:Unit.(!r) unit); (!r) unit) (ref (λx:Unit.unit))
Definition loop_fun :=
tabs x TUnit (tapp (tderef (tvar r)) tunit).
Definition loop :=
tapp
(tabs r (TRef (TArrow TUnit TUnit))
(tseq (tassign (tvar r) loop_fun)
(tapp (tderef (tvar r)) tunit)))
(tref (tabs x TUnit tunit)).
This term is well typed:
Lemma loop_typeable : ∃T, empty; nil ⊢ loop ∈ T.
Proof with eauto.
eexists. unfold loop. unfold loop_fun.
eapply T_App...
eapply T_Abs...
eapply T_App...
eapply T_Abs. eapply T_App. eapply T_Deref. eapply T_Var.
unfold extend. simpl. reflexivity. auto.
eapply T_Assign.
eapply T_Var. unfold extend. simpl. reflexivity.
eapply T_Abs.
eapply T_App...
eapply T_Deref. eapply T_Var. reflexivity.
Qed.
To show formally that the term diverges, we first define the
step_closure of the single-step reduction relation, written
⇒+. This is just like the reflexive step closure of
single-step reduction (which we're been writing ⇒*), except
that it is not reflexive: t ⇒+ t' means that t can reach
t' by one or more steps of reduction.
Inductive step_closure {X:Type} (R: relation X) : X → X → Prop :=
| sc_one : ∀(x y : X),
R x y → step_closure R x y
| sc_step : ∀(x y z : X),
R x y →
step_closure R y z →
step_closure R x z.
Definition multistep1 := (step_closure step).
Notation "t1 '/' st '⇒+' t2 '/' st'" := (multistep1 (t1,st) (t2,st'))
(at level 40, st at level 39, t2 at level 39).
Now, we can show that the expression loop reduces to the
expression !(loc 0) unit and the size-one store [r:=(loc 0)]
loop_fun.
As a convenience, we introduce a slight variant of the normalize
tactic, called reduce, which tries solving the goal with
multi_refl at each step, instead of waiting until the goal can't
be reduced any more. Of course, the whole point is that loop
doesn't normalize, so the old normalize tactic would just go
into an infinite loop reducing it forever!
Ltac print_goal := match goal with ⊢ ?x ⇒ idtac x end.
Ltac reduce :=
repeat (print_goal; eapply multi_step ;
[ (eauto 10; fail) | (instantiate; compute)];
try solve [apply multi_refl]).
Lemma loop_steps_to_loop_fun :
loop / nil ⇒*
tapp (tderef (tloc 0)) tunit / cons ([r:=tloc 0]loop_fun) nil.
Proof with eauto.
unfold loop.
reduce.
Qed.
Finally, the latter expression reduces in two steps to itself!
Lemma loop_fun_step_self :
tapp (tderef (tloc 0)) tunit / cons ([r:=tloc 0]loop_fun) nil ⇒+
tapp (tderef (tloc 0)) tunit / cons ([r:=tloc 0]loop_fun) nil.
Proof with eauto.
unfold loop_fun; simpl.
eapply sc_step. apply ST_App1...
eapply sc_one. compute. apply ST_AppAbs...
Qed.
Exercise: 4 stars (factorial_ref)
Use the above ideas to implement a factorial function in STLC with references. (There is no need to prove formally that it really behaves like the factorial. Just use the example below to make sure it gives the correct result when applied to the argument 4.)Definition factorial : tm :=
(* FILL IN HERE *) admit.
Lemma factorial_type : empty; nil ⊢ factorial ∈ (TArrow TNat TNat).
Proof with eauto.
(* FILL IN HERE *) Admitted.
If your definition is correct, you should be able to just
uncomment the example below; the proof should be fully
automatic using the reduce tactic.
(*
Lemma factorial_4 : exists st,
tapp factorial (tnat 4) / nil ==>* tnat 24 / st.
Proof.
eexists. unfold factorial. reduce.
Qed.
*)
☐
Additional Exercises
Exercise: 5 stars, optional (garabage_collector)
Challenge problem: modify our formalization to include an account of garbage collection, and prove that it satisfies whatever nice properties you can think to prove about it.End RefsAndNontermination.
End STLCRef.