Homework 1

Due September 17, 2007 (Monday)
2:00pm (via the submit server);
Proofs (part 4) due September 19, 2pm

Corrections

Introduction

This homework will give you practice writing code in OCaml.

What to Submit

You should submit one file, hw1.ml for parts 1 to 3 via the submit server. For part 4, you should turn in a printout of your code and your written proofs in class on the day the project is due.

Part 1: Simple OCaml functions

Part 2: Peano Arithmetic

Unsigned integers can be represented using an inductively defined type as proposed by Peano: a number is either zero, or the successor of another number. We can represent this as an OCaml datatype num:
type num =
    Zero        (* 0 *)
  | Succ of num (* Succ(n) == 1+n *)
Try to define all of these functions using a single (possibly recursive) function. This is to help make the connection between the code for these functions and inductive proofs. For extra credit, if you like, you can define additional versions of these functions that are tail-recursive.

Part 3: Functions on Sets

For this part, we will define an evaluator for programs that represent single-argument functions which take a set as an argument and return a set as a result. These functions can refer to intersection and union, as well as constant sets and the function's argument, according to the following grammar:

type setfun =
    Var
  | Const of (int list)
  | Union of setfun * setfun
  | Intersect of setfun * setfun
For example, we can define the function f(x) = x intersect {1} as the value Intersect(Var,Const [1]) Or, we can define the function f(x) = x union x union {1,2} as the setfun value Union(Var,Union(Var,Const [1;2])).

To evaluate these functions, you should define an evaluator function evals : setfun -> int list -> int list. This function takes two arguments: the function body itself (of type setfun) and the value to fill in the for the variable (the function's actual argument). The result is the evaluation of the function on the given argument. For example evals (Intersect(Var,Const [1])) [1;2] would return [1] while evals (Intersect(Var,Const [1])) [2] would return []. You should be sure that the lists that you provide to evals and that you return are actually sets; i.e., they should contain no duplicates. For this purpose, define the function is_set : int list -> bool that returns true if the argument contains no duplicates. Throw the exception failure if the argument fails this test (use the OCaml builtin failwith : string -> unit which throws the Failure exception with the first argument as its error message).

Also, define the subset operator on sets, leqSet : int list -> int list -> bool which returns true if the first argument is a subset of the second. Likewise, throw Failuire if either argument is not a set.

Part 4: Proofs

Prove two properties about the functions you have defined. Use proof by induction, where your proof should follow the structure of the inductive types you have defined; i.e., have one case for each variant of your datatype.

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 syllabus---please review it at this time.

Valid HTML 4.01!