COMP 150-AVS, Fall 2018
Due Thu, Sep 20 @ 11:59pm
This project will give you practice programming in OCaml by asking you to implement code for constructing, manipulating, and solving boolean formulae. You will then use your code to model binary numbers and solve a 3x3 magic square.
Here is the code skeleton for the project.
In this part of the project, you will develop some functions for working with boolean expressions, represented using the following type:
type bexpr = EFalse | ETrue | EVar of string | EAnd of bexpr * bexpr | EOr of bexpr * bexpr | ENot of bexpr | EForall of string * bexpr | EExists of string * bexprHere
EFalse
and ETrue
represent the obvious
values. EVar s
represents the boolean variable with
name s
. The
constructors EAnd
, EOr
,
and ENot
represent 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 Forall
and Exists
in 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
asst
contains the pair (s, b)
,
then that assignment gives the variable represented by the
string s
the value b
. When working with the
type asst
, you will find the
functions List.assoc
, List.mem_assoc
, and
related functions helpful. See
the OCaml
standard library documentation for
more details.
You may assume for purposes of this project that whenever you work
with an asst
, variables on the left override variables on
the right. E.g., the assignment ["a", true; "a",
false]
assigns true
to Var "a"
.
The last two expressions, EForall
and EExists
, represent the similarly named
quantifiers. The expression EForall(x,e)
is true
if e
is true when x
is true and
when x
is false. Similarly, EExists(x,e)
is
true if e
is true either when x
is true or
when x
is false.
You can find the definitions of the above types
in boolean.mli
, along with type signatures for several
functions you must implement in boolean.ml
:
eval : asst -> bexpr -> bool
evaluates 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 eval
function should return true
. Your
function can assume all of the expression's free variables are
specified in the assignment.free_vars : bexpr -> string list
returns a list of
the free variables 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 : bexpr -> asst option
should return
either Some a
where a
is any satisfying
assignment for the expression or None
if the expression
is not satisfiable. For example, given EOr(EVar "x", EVar
"y")
, the sat
function could return any of the
following:
Some ["x", true; "y", false]
Some ["x", false; "y", true]
Some ["x", true; "y", true]
sat
on 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_vars
function handy
here. Do not worry about the efficiency of sat
.However complex a boolean expression, it represents a single bit. In the next part of the project, you will put those bits together to represent integers using the following type:
type bvec = bexpr list (* low order bit at head of list *)A
bvec
is 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 []
or [EFalse]
or [EFalse; EFalse]
, etc. An
unknown 4-bit integer could be represented as [EVar "a"; EVar
"b"; EVar "c"; EVar "d"]
.
Implement the following functions in bvec.ml
:
int_of_bvec : bvec -> int
returns the OCaml integer
corresponding to a vector consisting solely of ETrue
and/or EFalse
. For example, int_of_bvec [EFalse;
ETrue]
returns 2
. You don't have to handle the
case when some element of bvec
is
neither ETrue
nor EFalse
.bvec_of_int : int -> bvec
is the inverse
of int_of_bvec
. (You may want to use mod
and /
in writing this function.)subst : asst -> bvec -> bvec
applies 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 -> bexpr
returns 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 -> bvec
returns 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 -> bexpr
returns an expression
representing whether the two vectors are equal. Again you can assume
the bit vectors have the same length.add : bvec -> bvec -> bvec
returns 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!
A magic square is an n-by-n grid of the numbers 1 through n^2 such that every number appears exactly once and the sum of each row, column, and diagonal is the same. For example, here is a 3x3 magic square:
8 | 1 | 6 |
3 | 5 | 7 |
4 | 9 | 2 |
In this part, you will write a function that solves the magic squares
problem, using the machinery you developed in part 1. In particular,
what we will do is "reduce" the problem of finding a solution to the
magic squares problem to a boolean formula. We can then use
the sat
function to actually find a solution. Here are the
functions you should write; place them in magic.ml
:
pad : bvec -> int -> bvec
. The function pad v i
returns a new bvec
that is equal to v
but whose
length is the greater of i
and the length of v
.
I.e., it pads v
, if necessary, with extra False
s so
that it has i
bits.
add_three : bvec -> bvec -> bvec -> bvec
. This function
returns a new vector that represents the sum of the three input
vectors. You can assume the three bvec
s have the same length.
is_digit : bvec -> bexpr
. The input is a bvec
of length 4 (i.e., exactly 4 boolean formulae). This function returns
a formula that is true if and only if the bvec
is greater than
or equal to 1 and less than or equal to 9.
disjoint : bvec list -> bexpr
. This function takes a
list of bvec
s and returns a formula representing whether all
the bvec
s are different from each other.
is_magic : bvec list -> bexpr
. This function takes a
list of exactly nine bvec
s and returns a formula representing
whether the list is a magic square. A list [v1; v2; v3; v4; v5;
v6; v7; v8; v9]
represents the following square:
v1 | v2 | v3 |
v4 | v5 | v6 |
v7 | v8 | v9 |
bvec
s in the list consist of exactly
four boolean formulae each, i.e., they are four-bit numbers.
You can try out your is_magic
function by seeing if it can
decide that the square above is magic. You can also try replacing one
or two entries by variables, and then seeing if your code correctly
finds the right numbers to fill in. However, you'll have to wait a
long, long time if you try making a lot of the entries in the magic
square variables, since your sat
function probably takes
exponential time.
Your next task is to implement a few functions related to
Lambda
calculus. Below is an
interface file lambda.mli
. You must implement the last
six of the listed functions in lambda.ml
. (We've
already implemented unparse
for you.)
type lexpr = | Var of string | Lam of string * lexpr | App of lexpr * lexpr val unparse : lexpr -> string val free_vars : lexpr -> string list val subst : string -> lexpr -> lexpr -> lexpr val beta : lexpr -> lexpr option val normal_form : lexpr -> lexpr val lexpr_of_int : int -> lexpr val add : lexpr -> lexpr -> lexprThese functions should do the following:
free_vars e
returns a list of the free variables
in e
, with no duplicates.
subst x e1 e2
returns a copy of e2
in
which free
occurrences of x
have 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 e
applies one step of call-by-value beta
reduction
to e
, or returns None
if no reduction is
possible,
according to the following rules:
Var x
amd Lam (x, e)
do not reduce (they
return None
).
App (e1, e2)
App(e1', e2)
if e1
reduces
to e1'
.
App(e1, e2')
if e1
cannot be
reduced
and e2
reduces to e2'
.
subst x e2 e
if e1=Lam(x,e)
and e2
cannot be reduced.
None
in any other cases.
normal_form e
keeps applying beta
to e
until the expression cannot be reduced any more, and then returns
the result.
lexpr_of_int n
returns the Church numeral (see slide
19 at
the link above) encoding of a non-negative OCaml integer.
add e1 e2
returns 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 suite_boolean
, suite_bvec
, suit_magic
,
and suite_lambda
, as appropriate.
We will grade this part of the project by running your test cases against correct and incorrect implementations. More specifically, we will create a correct implementation cor and a set of incorrect implementations Incor. Your test cases should detect that the incorrect implementations are buggy, but not just by trivially saying all implementations are buggy. Thus, you will receive credit for detection an incorrect implementation i∈Incor if at least one of your test cases both (1) flags i as incorrect and (2) passes cor as correct.
Put all your code in the code skeleton we have supplied, and upload your solution using Gradescope. Details will be posted here once we figure out what those details are.