
Project 1
Due September 16, 2011
11:59:59pm
Updates
 Deadline pushed to September 16 (from September 14)
Part 1: List functions
Write your solutions to the following problems in a file part1.ml
Implement the following functions in OCaml. Do not use any functions
in the List module, i.e., write every function from scratch using just
list notation [...], ::, and pattern matching.
 Write a function prod l : int list > int that returns
the product of the elements of l. The function prod should
return 1 if the list is empty.
 Write a function max l : int list > int that returns the
largest integer in l. You may assume that l is not
empty.
 Write a function addTail l e : 'a list > 'a > 'a list
that takes a list l and a single element e and
returns a new list where e is appended to the back
of l. For example, addTail [1;2] 3 =
[1;2;3].
 Write a function index l e : 'a list > 'a > int that
takes a list and a single element and returns the position of the first
occurrence of that element in the list (indexed by zero). You should
return 1 if the element is not in the list.
 Write a function rindex l e : 'a list > 'a > int that
takes a list and a single element and returns the position of the last
occurrence of that element in the list (indexed by zero). You should
return 1 if the element is not in the list.
 Write a function fill n x : int > 'a > 'a list that
returns a list containing n occurrences of x. For
example, fill 3 "foo" = ["foo"; "foo"; "foo"]. You
may assume that n is nonnegative.
 Write a function unzip l : ('a*'b) list > ('a list)*('b
list) that given a list of pairs, returns a pair of lists with the
elements in the same order. For example, unzip [(1, 2); (3, 4)]
= ([1; 3], [2;4]).
 Write a function app_int f m n : (int>'a)>int>int>'a
list that returns the list [f m; f (m+1); ...; f n]. It
should return the empty list if n < m.
Part 2: Boolean Formulae
In this part of the project, you can use the List library.
Write your solutions to this part of the project in a file part2.ml.
You will use the following data type, representing boolean formulae:
type formula =
False
 True
 Var of char
 And of formula * formula
 Or of formula * formula
 Not of formula
 Forall of char * formula
 Exists of char * formula
Here False and True represent the obvious values.
Var c represents the boolean variable with name c
(notice that variable names can only be characters). The constructors
And, Or, and Not represent boolean
conjunction, disjunction, and negation, respectively. For example,
the mathematical formula (a or b) and c would be represented by
the OCaml value 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 represent assignments of truth values to variables:
type assignment = (char * bool) list
Here if an assignment contains the pair (c,b), then
that assignment gives the variable represented by the character
c the value b. When working with the type
assignment, you will find the functions List.assoc,
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
with an assignment, all listed variables are distinct (i.e.,
you don't need to worry about names in one part of the list
"shadowing" names elsewhere in the list).
The last two kinds of formula, Forall and
Exists, represent the similarly named quantifiers. The boolean
formula Forall(x, f) is true if f is true under all
assignments to x, i.e., if f is true when
x=true and when x=false. The boolean formula
Exists(x, f) is true if f is true either for
x=true or x=false. For example, the formula
Forall('x', Or(Var 'x', Var 'y')) is true under the
assignment [('y', true)] and false under the assignment
[('y', false)].
Write the following functions that work with boolean formulae:
 nnf : formula > bool. This function returns true if
the formula is in negation normal form (NNF). A formula is in
NNF if negation appears only "in front" of variables. For example,
Or(Not (Var 'x'), True) is in NNF, but Not(And(Var 'x',
False)) is not.
 to_nnf : formula > formula. Given an arbitrary
formula, this function returns an equivalent formula in NNF. To write
this function, you can use the following equivalences:
Not True  =  False
 Not False  =  True
 Not(Not f)  =  f
 Not(And(f1, f2))  =  Or(Not f1, Not f2)
 Not(Or(f1, f2))  =  And(Not f1, Not f2)
 Not(Forall(x, f))  =  Exists(x, Not f)
 Not(Exists(x,f))  =  Forall(x, Not f)

 eval : formula > assignment > bool. This function
evaluates the boolean formula on the given variable assignment and
returns the result as an OCaml bool. For example, given the
OCaml value And(Or(Var 'x', Var 'y'), Var 'z') and the
assignment [('x', true); ('y', false); ('z', true)], the
eval function should return true. Your function can
assume that all of the formula's free variables are
specified in the assignment.
 vars_of : formula > char list. This function takes a
formula and returns a list of the names of the free variables
of the formula. The free variables are those that are not bound by a
quantifier. For example, for Exists('x', Or(Var 'x', Var
'y')), you should return a list containing only 'y'.
The list should contain no duplicates. There is no requirement as to
the order that the variable names must appear in the list.
 sat : formula > assignment option. This function
returns Some a, where a is a satisfying assignment,
if the formula is satisfiable, or None otherwise. For
example, sat (Or(Var 'x', Var 'y')) could return three
things: Some ([('x', true); ('y', false)]), Some ([('x',
false); ('y', true)]), or Some ([('x', true); ('y',
true)]), whereas sat (And(Var 'x', Not (Var 'x'))) would
return None. If more than one assignment is possible, you
may return any assignment. You might find the vars_of
function handy here. Do not worry about the efficiency of this
function; it's fine if it takes exponential time. (For a better
algorithm, read up on DPLL.)
What to Submit
Submit part1.ml and part2.ml.
Academic Integrity
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
syllabusplease review it at this time.
