This assignment has 15 points.
1. [2 points] Write a well-typed, non-terminating program in a typed lambda calculus that only has unit, non-recursive functions (ie: \x:t.e) and references (ie: operations ref e, e1 := e2 and !e).
2. [6 points] Prove the type preservation lemma for a language with unit, non-recursive functions and references. In other words, prove that:
If |- (M,e) : t and (M,e) --> (M', e') then (M', e') : t
The syntax of types and expressions are:
t ::= unit | t1 -> t2 | t ref
e ::= x | () | e1; e2 | \x:t.e | e1 e2 | ref e | e1 := e2 | !e | l
v ::= () | \x:t.e | l
M ::= . | M,l -> v (treat as a function from locations l to values v)
Psi ::= . | Psi, l:t (treat as a function from locations l to types t)
You may assume the following lemmas have already been proven:
Lemma 1: If |- M : Psi and l not in Dom(M) and Psi; . |- v : t then |- (M,l->v) : (Psi,l:t)
Lemma 2: If |- M : Psi and Psi(l) = t and Psi; . |- v : t then |- M[l->v] : Psi
Lemma 3: If |- M : Psi and l in Dom(M) then Psi; . |- M(l) : Psi(l)
Lemma 4: If Psi;G |- e : t and l not in Dom(Psi) then Psi,l:t';G |- e : t
Only do the proof for the three cases involving these operational rules:
(l not in Dom(M))
--------------------------- (E-ref)
(M;ref v) --> (M,l-> v; l)
(l in Dom(M))
------------------------------- (E-assign)
(M; l := v) --> (M[l -> v]; ())
(l in Dom(M))
------------------------------- (E-deref)
(M; !l ) --> (M; M(l))
3. [7 points] Implement the operational semantics of (ie: an interpreter for) a language that only has references and unit in SML. The expressions of your language should be:
e ::= v | e1; e2 | ref e | e1 := e2 | !e
v ::= () | l
M ::= . | M,l -> v
You should define the syntax of expressions using a datatype. You may implement locations using integers. eg:
datatype val =
Unit
| Loc of int
datatype exp =
Val of val
| Seq of exp * exp (* this is semicolon *)
| ...
You should also define a type for memories:
type memory = ...
Your main job will be to define:
a function eval that implements a single step of the operational semantics
a function printval that prints out a value legibly (print out a location by printing the integer that represents it; print the unit value as ())
a function printmemory that prints out a memory in a legible way (eg, as a list of location, value pairs)
a function evalstar that executes as many steps of the operational semantics as possible (ie: until a value is reached) and prints out the final value and the final memory at the end
The evaluation functions may assume that all expressions and memories are well-typed. You may raise the exception Bad if you run in to a situation you
cannot implement (because, for instance, a memory reference is out of bounds):
exception Bad
fun eval : (memory * exp) -> (memory * exp) (* may raise exception Bad *)
fun printval : val -> unit
fun printmemory : memory -> unit
fun evalstar : (memory * exp) -> unit (* may raise exception Bad *)