Types and Programming Languages
Lecture 12
Simon Gay
Department of Computing Science
University of Glasgow
2006/07
Type Safety: Unique Use
In order to prove that every value is used exactly once, we need
to define an alternative operational semantics which allows us
to see values being “consumed”.
The idea is to explicitly represent every value as being stored in
memory and accessed by a pointer. Then we can define
reductions on Store , Term configurations so that every value
is removed from the store when it is first used.
Then we will prove that when executing a well-typed term, we
never get a dangling pointer, and that at the end of execution,
there is nothing left in the store except the final value.
The system will look like what we would get in lambda calculus
with references, if we put ref around every value.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
2
Linear Lambda Calculus: Syntax
The same as before, plus store locations (pointers) m,n,…
v ::= integer literal
| true | false
| x:T.e
|m
(not top-level syntax)
e ::= v
|x
| e + e | e == e | e & e | if e then e else e
| ee
T ::= int
| bool
|TT
2006/07
Store
S ::= m=v,…
Types and Programming Languages Lecture 12 - Simon Gay
3
Linear Lambda Calculus: Semantics
First define removal of a location from the store:
(S, m=v, S’) – m = S,S’
Now define reductions of the form
S , e  S’ , e’
Evaluating a value creates a store location and returns it:
S , true
S , false
S,v
S , x:T.e




S+[m=true] , m
S+[m=false] , m
S+[m=v] , m
S+[m=x:T.e] , m
v is a integer literal
In each case, m is a fresh location.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
4
Linear Lambda Calculus: Semantics
Next we define reductions which consume values.
S(m)  true
S, if m then t else e  S  m, t
S(m)  false
S, if m then t else e  S  m, e
S(m)  u
S(n)  v
w is the sum of u and v
S, m  n  (S  m  n)  [p  w ], p
m,n different
S(m)  x : T.e
S, mn  S  m, e[n / x ]
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
5
Linear Lambda Calculus: Semantics
Finally we define reductions within expressions, as usual.
S, e  S' , e'
S, e  S' , e'
S, e  f  S' , e' f
S, m  e  S' , m  e'
Similarly for the other operators.
S, c  S' , c '
S, if c then t else e  S' , if c' then t else e
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
6
Example
,
(x:int. x+1)2
m = x:int. x+1 ,
m2
(m = x:int. x+1 , n = 2) , m n
n=2 ,
n+1
(n = 2 , p = 1) ,
n+p
q=3 ,
q
FINAL RESULT
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
7
Example
,
(x:int. (x+1)+x)2
m = x:int. (x+1)+x ,
m2
(m = x:int. (x+1)+x , n = 2) , m n
n=2 ,
(n+1)+n
(n = 2 , p = 1) ,
(n+p)+n
q=3 ,
q+n
STUCK: n is a “dangling pointer”
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
8
Exercise
We now have two different semantics for (essentially) the same
language: lambda calculus. The original semantics is based on
reductions of expressions. The new semantics uses a store
(and destroys values after their first use).
Try to prove the following theorem, relating the semantics:
If  , e * S,m=v, m in the linear lambda calculus
semantics, then e * v in the standard lambda calculus
semantics.
Why don’t we expect the converse to be true?
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
9
Proving Type Safety: Unique Use
Just as in the case of lambda calculus with references, we need
the idea of a store typing  , so that we can give a type to the
expression m (store location).
The store typing must be treated in the same way as the
environment , so that in a typing judgement  |   e:T
the  and  describe exactly the variables and locations used
by e.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
10
Linear Lambda Calculus with Store Typings
 |   true : bool
 |   false : bool
 |   v : int
if v is an integer literal
x : T |   x : T (LS-Var)
 |   e : int
 | '  f : int
,  | , '  e  f : int
 |   c : bool
 | m:T  m : T (LS-Loc)
(LS-Plus)
 | '  e : T
 | '  f : T
,  | , '  if c then e else f : T
, x : T |   e : U
 |   x:T.e : T o U
2006/07
(LS-Abs)
similarly &, ==
(LS-If)
 |   e : T o U
 | '  e' : T
,  | , '  ee' : U (LS-App)
Types and Programming Languages Lecture 12 - Simon Gay
11
Well-Typed Stores
Just as we saw for references, we need the idea of a well-typed
store. We write  S ::  and define it by the following rules:
  :: 
Empty
 S :: 1,  2
 | 1  v : T
 S, m  v ::  2 , m : T
Next
This is rather subtle. The store typing  describes the store
locations that are available for use, i.e. not already used within
other parts of the store.
Examples:
 m=2, n=true :: m:int, n:bool
 m=2, n=x:int. x+m :: n:intint
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
12
Well-Typed Stores
We will need the following fact about well-typed stores.
Lemma: If  S,m=v :: ,m:T and  | ’  v : T
then  S :: ,’
This might seem trivial, but the effect is that we can use rule
Next (previous slide) in reverse even when m was not the last
location to be added.
It can be proved (exercise) by induction on the derivation of
 S,m=v :: ,m:T . The base case is trivial and the inductive
case breaks into two sub-cases, depending on whether or not
m is the last location added.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
13
Substitution Lemma
As usual we need a substitution lemma. Because of the way the
operational semantics is defined, we only need to consider
substituting a store location for a variable.
Lemma:
If , x:T |   e:U then  | ,n:T  e[n/x] : U
Proof (outline):
e cannot be a boolean or integer literal or a store location (why?)
If e is a variable then it must be x (why?) and  and  must
be  (why?) so the desired conclusion is  | n:T  n:T
which follows from rule LS-Loc.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
14
Substitution Lemma
Proof (continued):
The other cases use the induction hypothesis in a similar way to
the Substitution Lemma for simply typed lambda calculus. The
difference is that the substitution only goes into one part of the
expression.
If e is t+u then we have
where
1 |   e : int
2 | '  f : int
, x : T | , '  e  f : int
1, 2  , x : T
and we consider two cases, depending on whether x is used in
e or in f.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
15
Type Preservation
Theorem: If  |   e:T and  S ::  and S , e  S’ , e’
then there exists ’ such that  | ’  e’:T and  S’ :: ’ .
Proof: By induction on the derivation of S , e  S’ , e’ .
1.
S , true
 S+[m=true] , m
We have  |   true:bool so = (why?) and S= (why?).
Therefore S’ = (m=true) .
Taking ’ = m:bool gives  | ’  m:bool and  S’ :: ’
as required.
The cases of the other values are similar. For y:U.e we can’t
say that = and S= because e may use locations.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
16
Type Preservation
2.
S , if m then e else e’  S-m , e
We have
therefore
Taking
 | 1  m : bool
because S(m)=true .
 | 2  e : T
 |  2  e' : T
 | 1,  2  if m then e else e' : T
1  m : bool
'  (1, 2 )  m  2
we have  | ’  e:T
and we just need  S-m :: ’
which follows from the Lemma on slide 13.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
17
Type Preservation
3.
S , mn  S-m , e[n/x]
because S(m)= x:T.e .
 | m : T o U  m : T o U
We have
|n:T n:T
 | m : T o U, n : T  mn : U
and  S :: m:T —o U, n:T
By the lemma on slide 13,  S-m :: ,n:T
where
 |   x:T.e : TU
This typing is justified by x:T |   e : U
from which the Substitution Lemma gives  | ,n:T  e[n/x] : U
as required.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
18
Type Preservation
4. The remaining cases, such as
S, e  S' , e'
S, e  S' , e'
S, e  f  S' , e' f
S, m  e  S' , m  e'
follow from straightforward uses of the induction hypothesis.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
19
Progress
Finally we can also prove
Progress Theorem
If  S ::  and  |   e:T then either S , e  S’ , e’
(for some S’) or e is a store location.
very easily, by checking that for every potentially reducing term
(e.g. if m then t else e), the typing and the store typing mean
that one of the reduction rules applies.
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
20
The Final Value
Combining Progress and Preservation, we see that reduction of
a typed term in a typed store terminates with S , m and one of
the following cases applies:
1.
2.
3.
4.
S is m=true
S is m=false
S is m=v for some integer literal v
S(m) = x:T.e and  S-m ::  and x:T |   e : U
i.e. S contains just m and the locations referred to by e
Exercise: work out the complete reduction sequence for
(x:int.y:int.x+y)3
2006/07
Types and Programming Languages Lecture 12 - Simon Gay
21
Descargar

Types and Programming Languages