# Homework 1

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

## Corrections

• (9/10, 1:45pm) The original definition of setfun was incorrect: it included a parameter (i.e., it was written type `a setfun = ... ). This was from an earlier version of things that aimed to be more general, but it's not really necessary so I removed it.
• (9/12, 4pm) Proofs (part 4) now due on September 19 in class, rather than the 17th.

## 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

• 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 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]).

## 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 *)
```
• Write a function int_of_num : num -> int to convert a num to a positive OCaml integer. For example, int_of_num (Succ (Succ (Zero))) would return 2.
• Write a function num_of_int : int -> num to convert from a positive OCaml integer to a num. (You may assume the argument ot int_of_num is positive.) For example, num_of_int 1 would return Succ Zero
• Write a function add : num -> num -> num that adds two num values. Do not implement this by converting the numbers to integers, performing the addition, and converting them back!
• Write a function mul : num -> num -> num that multiplies two num values.
• Write a function seq : num -> num the returns the sum of all integers from Zero to the first argument, inclusive. For example, seq (Succ (Succ Zero)) would return Succ (Succ (Succ Zero)).
• Write a function eqnum : num -> num -> bool that returns true if the two provided numbers are equal, and false otherwise. For example, eqnum (Succ Zero) Zero would be false, and eqnum (Succ Zero) (Succ Zero) would be true.
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.
• Prove that int_of_num (seq (num_of_int n)) is equal to n * (n+1) / 2
• Prove that all setfuns are monotonic; i.e., that if leqSet l1 l2 then for all e we have leqSet (evals e l1) (evals e l2)