CMSC 430, Fall 2016
Due Wed, Sep 14, 2016 @ 11:59:59pm
evalto be in same order as in code skeleton.
This project will help refresh your memory on programming in OCaml by asking you to write two small modules and then develop test cases for them. You may find it helpful to review the OCaml slides from CMSC 330.
Here is the code skeleton for the project.
In this part of the project, you will develop some functions for working with boolean expressions and vectors of boolean expressions. We will use the following data type to represent boolean expressions:
type expr = EFalse | ETrue | EVar of string | EAnd of expr * expr | EOr of expr * expr | ENot of expr | EForall of string * expr | EExists of string * exprHere
ETruerepresent the obvious values.
EVar srepresents the boolean variable with name
s. The constructors
ENotrepresent boolean conjunction, disjunction, and negation, respectively. For example, the expression (a or b) and c could be represented as
And(Or(Var "a", Var "b"), Var "c"). (We'll explain
Existsin a moment.)
We will use associative lists, which are just lists of pairs, to assign truth values to variables:
type asst = (string * bool) listHere if an
asstcontains the pair
(s, b), then that assignment gives the variable represented by the string
b. When working with the type
asst, you will find the functions
List.mem_assoc, and related functions helpful. See the OCaml library documentation for more details.
You may assume for purposes of this project that whenever you work
asst, variables on the left override variables on
the right. E.g., the assignment
["a", true; "a",
The last two expressions,
EExists, represent the similarly named
quantifiers. The expression
EForall(x,e) is true
e is true when
x is true and
x is false. Similarly,
e is true either when
x is true or
x is false.
However complex a boolean expression, it represents a single bit. We can put those bits together to represent integers using the following type:
type bvec = expr list (* low order bit at head of list *)A
bvecis a list of boolean expressions representing bits, with the low order bit at the head of the list. For example, we could represent the number 13 as
[ETrue; EFalse; ETrue; ETrue]. Zero could be represented as
[EFalse; EFalse], etc. An unknown 4-bit integer could be represented as
[EVar "a"; EVar "b"; EVar "c"; EVar "d"].
You can find the definitions of the above types
boolean.mli, along with type signatures for several
functions you must implement in
eval : asst -> expr -> boolevaluates the expression on the given assignment and returns the result as an OCaml
bool. For example, given assignment
["x", true; "y", false; "z", true]and expression
EAnd(EOr(EVar "x", EVar "y"), EVar "z"), the
evalfunction should return
true. Your function can assume all of the expression's free variables are specified in the assignment.
free_vars : expr -> string listreturns a list of the free varialbes of the expression. The free variables are those that are not bound by a quantifier. For example, for
EExists("x", EOr(EVar "x", EVar "y")), you should return a list containing only
"y". The list should contain no duplicates. The free variables may appear in any order in the list.
sat : expr -> asst optionshould return either
ais any satisfying assignment for the expression or
Noneif the expression is not satisfiable. For example, given
EOr(EVar "x", EVar "y"), the
satfunction could return any of the following:
Some ["x", true; "y", false]
Some ["x", false; "y", true]
Some ["x", true; "y", true]
EAnd(EVar "x", ENot(EVar "x"))should return
None. If more than one assignment is possible, you may return any assignment. You might find the
free_varsfunction handy here. Do not worry about the efficiency of
int_of_bvec : bvec -> intreturns the OCaml integer corresponding to a vector consisting solely of
EFalse. For example,
int_of_bvec [EFalse; ETrue]returns
2. You don't have to handle the case when some element of
bvec_of_int : int -> bvecis the inverse of
int_of_bvec. (You may want to use
/in writing this function.)
subst : asst -> bvec -> bvecapplies the (possibly partial) assignment to the vector. For example,
subst ["x", true] [EVar "x"; ETrue; EAnd(EVar "x", EVar "y")]should return
[ETrue; ETrue; EAnd(ETrue, EVar "y")].
zero : bvec -> exprreturns a boolean expression that is true iff the vector is zero. For example
zero [EVar "x"; EVar "y"]could evaluate to
EAnd(ENot(EVar "x"), ENot(EVar "y")).
bitand : bvec -> bvec -> bvecreturns a new vector representing the bitwise and of the two vectors. You can assume for this problem that the two bit vectors have the same length.
eq : bvec -> bvec -> exprreturns an expression representing whether the two vectors are equal. Again you can assume the bit vectors have the same length.
add : bvec -> bvec -> bvecreturns a new vector representing the sum of the two vectors. You may assume the two vectors have the same length. Since there may be a carry out of the last bit, the resulting vector will have one more element than the input vectors. You'll have to figure out the expression for addition yourself. Hint: You'll probably want to write a recursive helper function that has an extra parameter for the carry bit.
If you've gotten this far, you've now built a (likely very slow) solver for part of bitvector arithmetic! Suppose we have:
let x = [EVar "a"; EVar "b"] let y = [EVar "c"; EVar "d"] let z = [EFalse; EFalse; ETrue] (* 4 *)Then we can use our solver to answer questions like:
sat (eq (add x y) z) (* are there two, two-bit numbers that sum to 4? *) sat (eq (add x x) z) (* is there a two-bit number that, doubled, is 4? *)etc. Cool!
Your next task is to implement a few functions related to
calculus, which you learned about in CMSC 330. Below is an
lambda.mli. You must implement the last six
of the listed functions in
lambda.ml. (We've already
unparse for you.)
type expr = | Var of string | Lam of string * expr | App of expr * expr val unparse : expr -> string val free_vars : expr -> string list val subst : string -> expr -> expr -> expr val beta : expr -> expr option val normal_form : expr -> expr val expr_of_int : int -> expr val add : expr -> expr -> exprThese functions should do the following:
free_vars ereturns a list of the free variables in
e, with no duplicates.
subst x e1 e2returns a copy of
e2in which free occurrences of
xhave been replaced by
e1. Be sure to implement capture-avoiding substitution, i.e., bound variables should be renamed as needed to avoid capture free variables under a lambda. For example,
subst "x" (Var "y") (Lam("y", Var "x"))should return something equivalent to
Lam("z", Var "y")and not
Lam("y", Var "y"). (Did you have to worry about this for boolean expressions? Why not?)
beta eapplies one step of call-by-value beta reduction to
e, or returns
Noneif no reduction is possible, according to the following rules:
Lam (x, e)do not reduce (they return
App (e1, e2)
e1cannot be reduced and
subst x e2 eif
e2cannot be reduced.
Nonein any other cases.
normal_form ekeeps applying
euntil the expression cannot be reduced any more, and then returns the result.
expr_of_int nreturns the Church numeral (see slide 19 at the link above) encoding of a non-negative OCaml integer.
add e1 e2returns the sum of two Church numerals (slide 22).
Your last task is to write unit tests for parts 1 and 2 above, using
OUnit. Put your test
cases in the file
test.ml, and be sure to add your test cases
to the suites
appropriate. We will grade this part of the project by running your
test cases against various correct and incorrect implementations. A
test case will only be counted as correct if it passes a correct
implementation and fails at least one incorrect implementation.
Put all your code in the code skeleton we have
supplied, and upload your solution to the submit server. You can
either upload your solution via the web interface, or you can
java -jar submit.jar in the project directory. Your
code can use any OCaml standard library functions that you like.
Important note: On GRACE you should use the version of OCaml installed at
Please post any questions you have about this on Piazza. You are welcome to install OCaml on your own machine, though we can't provide much support for that. We do recommend using opam to manage the installation process if you choose to do that. You can use opam to install both OCaml and OUnit
The Campus Senate has adopted a policy asking students to include the following statement on each assignment in every course: "I pledge on my honor that I have not given or received any unauthorized assistance on this assignment." Consequently your program is requested to contain this pledge in a comment near the top.
Please carefully read the academic honesty section of the course syllabus. Any evidence of impermissible cooperation on projects, use of disallowed materials or resources, or unauthorized use of computer accounts, will be submitted to the Student Honor Council, which could result in an XF for the course, or suspension or expulsion from the University. Be sure you understand what you are and what you are not permitted to do in regards to academic integrity when it comes to project assignments. These policies apply to all students, and the Student Honor Council does not consider lack of knowledge of the policies to be a defense for violating them. Full information is found in the course syllabus---please review it at this time.