Problem Set 4: Interpreters and Proofs
In this assignment, you will develop an environment-based interpreter to replace the substitution-based interpreter defined in class. You will also practice proving your functional programs are correct. You will do this assignment individually.
Note: You can do Parts 1 and 2 in either order (or switch back and forth). You do not need to complete Part 1 before beginning Part 2. (But we haven't introduced proofs in class yet, so you should wait until next week to work on Part 2 ... that means that it is in your best interest to get as much done on Part 1 now as you can!)
Download the code here. Unzip and untar it:
$ tar xfz a4.tgzGo in to the directory and list its all contents. Type:
$ cd a4 $ ls -aYou should see:
- A collection of .ml and .mli files
.merlinfile to configure merlin for you
.ocamlinitfile to load the appropriate files in to the OCaml toplevel if you use it. Before starting the toplevel, you will have to compile your binaries: use ocamlbuild and/or the Makefile.
A few important things to remember before you start:
- This assignment must be done individually.
- Make sure that the functions you are asked to write have the correct names and the number and type of arguments specified in the assignment. Programs that do not compile will be subject to penalties on top of regular deductions.
- In this problem set, it is important to use good style (style will factor in to your grade). Style is naturally subjective, but the COS 326 style guide provides some good rules of thumb. As always, think first; write second; test and revise third. Aim for elegance.
Part 1: Environment-based Evaluator
In class, we developed a substitution-based interpreter in OCaml. While substitution makes for a good theoretical model of how OCaml programs evaluate, practical implementations use an environment-based model of execution. Fortunately, the two models coincide, so you can safely use substitution to reason about your programs while your interpreter uses environments to implement them.
In this part of the assignment, you will implement an environment-based interpreter for a simplified OCaml-like language (let's call it MiniML). In a4.tgz, you should find the following files:
Syntax.ml: The datatype that defines the abstract syntax of the language. The language contains integers, pairs, lists, and possibly-recursive functions. This file also contains a definition of environments and a few small functions you must complete.
EvalSubst.ml: A call-by-value, substitution-based interpreter. We have partially implemented a substitution-based interpreter for you. This is to give you a (partial) reference implementation that you can look at and to ensure that you understand the semantics of recursive functions, variables, let expressions, etc. You do not have to implement any more of this interpreter! (You may for fun, of course.)
EvalEnv.ml: A call-by-value, environment-based interpreter. In this interpreter, variable bindings are stored in an environment. When we encounter a variable in our code, we look up the value of the variable in the environment. In addition, to evaluate a function definition, we create a closure, which is a pair of the recursive function definition and its environment.
EvalUtil.ml: A couple of utilities shared between both the substitution-based interpreter and the environment-based interpreter.
Testing.ml: A small collection of test cases. You will have to edit this file to add a few additional test cases (and then as many more as you want to test your code).
Printing.ml: Some pretty-printing routines. You do not have to touch this file.
Main.ml: A driver that runs the test cases. It is set up to test EvalEnv. Change one line to test EvalSubst, the substitution-based interpreter.
It is a good idea to begin by familiarizing yourself with the code before you start writing any new code yourself.
- Start by looking at
Syntax.ml. That is the place where we define the datatype for the language. Bring questions about how the various elements of the language work to precept.
- Next, look at some of the test cases in Testing.ml. Those show you how to use the data types to construct example programs. Even though the substitution-based interpreter is incomplete, you should be able to execute a few of the examples, such as fact4. Try it. The examples also help show you how to use pairs and lists. If you aren't sure how some of the elements of the language (like pairs or lists) should be structured or can't figure out how some of the examples we have given you work, ask in precept, on Piazza, or in office hours.
- Next, look at some of the code in
EvalSubst.ml. That code will illustrate the basic structure of a (substitution-based) interpreter. Your environment-based interpreter will be a little different, of course.
Your main task is to implement the environment-based interpreter. To do this, you will initially have to modify 2 files:
Syntax.ml, fill in the small definitions of
Syntax.mlfor a description of what they should do.)
EvalEnv.ml, examine the
is_value. This defines the elements of the language that are values. Next, look at
eval_body, which is the bulk of the interpreter. We have given you 1 case of the interpreter: The case for variables. That case simply looks up a variable in the current environment. You should not change this case. The other key cases are:
- The case for Rec. Rec is the definition of a function, which might be recursive. In this case, you will have to return not a Rec (like in the subsitution-based interpreter), but instead a Closure, which packages the components of the function definition up with an environment.
- The case for function application. We will let you figure out what to do there.
In Testing.ml, we ask you to create several specific new test cases. Please see that file and create the new functions that are requested. (Of course, you might want to do this while writing and testing your interpreter above.) You may create as many more test cases as you like.
In functional programming language implementations, it is important to optimize the size of the closures that are created. The most naïve thing one can do when creating a closure is to put ALL variables in the current execution environment into the closure's environment. However, any given function only requires access to its free variables. For a refresher on free and bound variables read this note.
Some key examples:
x + 2
free variables: x
let x = 3 in x + 2
free variables: none (x is bound by let)
rec f x = x + y
free variables: only y (x is bound as function parameter)
closure [y=3] f x = x + y
free variables: none (x is bound as function parameter, y is found in environment)
The environment that a
Rec is evaluated with to form
the closure could have many superfluous bindings that can be
pruned, including duplicate bindings of the same variable or
variables that do not appear in the function. Revise your
implementation of the
Rec case of the interpreter to
create minimal closures — closures that only contain the free
variables of the function in the environment. To do so,
you'll need to write a function that analyzes an arbitrary function to
extract the free variables of the function, and include only these
bindings in the environment.
Note: be careful comparing strings. You should use
String.compare. We placed a couple of helper functions
in Syntax.ml for comparing variables for equality and inequality
Part 2: Program Correctness
In this section, you must answer several theoretical questions. You must present your proofs in the 2-column style illustrated in class with facts that you conclude (like a new expression being equal to a prior one) on the left and a justification (like by "evaluation" or "simple math") on the right. Hand in the text file proofs.txt filled in with your answers.
To prepare for this part of the assignment, read the online notes on equational reasoning. Hand in proofs in the style presented in those notes.
Part 2.1: Complex Numbers
Complex numbers can be represented by their real and immaginary components. Let us use a pair of integers for this. Consider the following addition function that adds the corresponding components of the pairs.
type complex = int * int let cadd (c1:complex) (c2:complex) = let (x1,y1) = c1 in let (x2,y2) = c2 in (x1+x2, y1+y2)
Let a == (a1,a2), b == (b1, b2), and c == (c1,c2) be complex numbers. Prove that addition is associative. In other words, prove:
cadd a (cadd b c) == cadd (cadd a b) c
Part 2.2: A Minimal Proof
Consider the following code (and please note that min_int is a constant with type int that OCaml provides you with):
let max (x:int) (y:int) = if x >= y then x else y let rec maxs (xs:int list) = match xs with  -> min_int | hd::tail -> max hd (maxs tail) let rec append (l1:'a list) (l2:'a list) : 'a list = match l1 with  -> l2 | hd::tail -> hd :: append tail l2
You may use the fact that max, maxs and append are all total
functions. You may also use the following simple properties
max by name without proving them:
For all integer values a, b, c: (commutativity) max a b == max b a (associativity) max (max a b) c == max a (max b c) (idempotence) max a (max a b) == max a b (min_int) max min_int a == a
Now, prove that for all integer lists xs and ys,
max (maxs xs) (maxs ys) == (maxs (append xs ys))
At the beginning of your proof, be sure to state the methodology that you intend to use (ie: by induction on ...) Mention where you use properties such as associativity, commutativity, idempotence or min_int, if and when you need to use them.
Part 2.3: Map and Back
In previous assignments, we sometimes asked you to write recursive functions over lists using map and fold and some times without. Now you can prove that it doesn't matter which way you choose to write your function — the two styles are equivalent.
let rec map (f:'a -> 'b) (xs:'a list) : 'b list = match xs with  ->  | hd::tail -> f hd :: map f tail let bump1 (xs:int list) : int list = map (fun x -> x+1) xs let bump2 (xs:int list) : int list = match xs with  ->  | hd::tail -> (hd+1) :: map (fun x -> x+1) tail let rec bump3 (xs:int list) : int list = match xs with  ->  | hd::tail -> (hd+1) :: bump3 tail
(a) Prove that
for all integer lists l, bump1 l == bump2 l.
(b) Prove that
for all integer lists l, bump1 l == bump3 l.
(c) In one sentence, what's the big difference between the part (a) and part (b)?
Part 2.4: Zippity do da
In this question, you may need a few additional laws of the lambda
calculus to prove your programs correct. First, pattern-matching
on pairs can be viewed as more primitive operations to extract the
first component (
fst e) and the second component
snd e) of a pair. More precisely, you are free to
use the following equation provided that x does not appear as a free
(pair-pattern) let (x,y) = e1 in e2 == let x = fst e1 in let y = snd e1 in e2Second, it may be useful for you to use what is known as an eta-equivalence rule. This rule is only valid if the expression
eunder consideration has a pair type
t1 * t2. The eta rule is as follows:
(eta-pair) e == (fst e, snd e)This last rule says that an expression that taking the first and second projections of a pair (
e) and then re-creating the pair is the same as the pair itself untouched. As a point of interest, there are other eta-rules for other types. For example, if
t1 -> t2and
xdoes not appear free in
ethen the eta-rule for function types says the following:
(eta-function) e == fun x -> e x
With these new laws in mind, consider the following functions:
let rec zip (ls:'a list * 'b list) : ('a * 'b) list = match ls with (,_) ->  | (_,) ->  | (x::xrest, y::yrest) -> (x,y)::zip (xrest,yrest) let rec unzip (xs:('a * 'b) list) : 'a list * 'b list = match xs with  -> (,) | (x,y)::tail -> let (xs,ys) = unzip tail in (x::xs, y::ys)
Prove or disprove each of the following.
For all l : ('a * 'b) list, zip(unzip l) == l.
For all l1 : 'a list, l2 : 'b list, unzip(zip (l1,l2)) == (l1,l2).
NOTE: The way that you disprove a theorem is you give a counter example. For instance, if a theorem says "for all x of type t, ... property about x ..." then to disprove the theorem, all you need to do is find one value v with type t and show that the property does not hold for v. If you can, then clearly the property does not hold "for all" x of type t.
Handin Instructions and Grading Information
This problem set is to be done individually.
You must hand in these files to dropbox (see link on assignment page):