Project 1: OCaml Warmup

Due: Thur, Feb 16, 2017 11:59:59pm

Updates

• The submit server is now accepting and testing submissions. You will need to download .submit and submit.jar to the directory containing your code. Run java -jar submit.jar to submit everything in the current directory. Check the submit server for test results.

• Revised instructions for using ocaml on the GRACE cluster in What to Turn In

• Added a clarifying note about add in Part 2: Lambda Calculus

Introduction

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.

Advice

• Start early. Submit something as early as possible. You can submit the code skeleton to get partial credit and work out any issues with the submit server.

• Make examples and think about what these functions should produce before you start writing code.

• Let the type of inputs to a function guide the structure of the function. Together with examples from above, the code will basically write itself.

Part 0: Binary trees

This is not part of the project; it is only here as a warm-up to the rest. Try to do these finger exercises first. If you have trouble, don’t try to proceed to the rest of the project, but rather try to master these simpler concepts first. You do not have submit this code and it will not be graded if you do.

Here’s a type for binary trees:

Implement the following functions:

A path is a list of directions, which are either left or right, and can describe a path to an element in a binary tree:

Write a function the gets the element found by following a given path. This function should fail if the path goes off the end of the tree:

A binary search tree is binary tree with an ordering on elements such that all elements in the left subtree of a node are less than or equal the value of the node and all elements in the right subtree.

Here’s one possible type for binary search trees:

Think of the comparison function like (<=).

Implement the following functions:

Using your implementation of binary search trees, implement a sorting algorithm that consumes a list of elements and produce the same list of elements but in sorted order.

Part 1: Boolean Expressions and Vectors

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:

Here 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 EAnd (EOr (EVar "a", EVar "b"), EVar "c"). (We’ll explain EForall and EExists in a moment.) We will use associative lists, which are just lists of pairs, to assign truth values to variables:

Here 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 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.

However complex a boolean expression, it represents a single bit. We can put those bits together to represent integers using the following type:

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"]. 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 -> expr -> 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 : expr -> 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 : expr -> 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]

  In contrast, calling 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.

• 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 -> expr 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 -> expr 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:

Part 2: Lambda Calculus

Your next task is to implement a few functions related to Lambda calculus, which you learned about in CMSC 330. Below is an interface file "lambda.mli". You must implement the last seven of the listed functions in "lambda.ml". (We’ve already implemented unparse for you.)

These functions should do the following:

• free_vars e returns a list of the free variables in e. (Duplicates are allowed.)

• is_alpha e1 e2 returns true only if the two expressions are alpha equivalent, meaning they are the same expressions up to a consistent renaming of bound variables.

• 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 capturing 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").

• 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 and Lam (x, e) do not reduce (they return None).

  • App (e1, e2)

    • Returns App(e1’, e2) if e1 reduces to e1’.

    • Returns App(e1, e2’) if e1 cannot be reduced and e2 reduces to e2’.

    • Returns subst x e2 e if e1==Lam(x,e) and e2 cannot be reduced.

• normal_form e keeps applying beta to e until the expression cannot be reduced any more, and then returns the result.

• expr_of_int n returns the Church numeral (see slide 19 at the link above) encoding of a non-negative OCaml integer.

• add e1 e2 adds two Church numerals (slide 22) and produces a Church numeral representing their sum. Note: there are several different—but equivalent—terms that can represent the sum of two Church numerals. Your implementation may produce any one of them.

Part 3: Unit Testing

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_trie and suite_lambda, as 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.

What to Turn In

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 run java -jar submit.jar in the project directory.

Important note: On GRACE you should use the version of OCaml installed in the public directory for this course. It is version 4.04.0 and has the ocamlfind and ounit libraries pre-installed. To access this version of ocaml, run the following command after logging in to grace.umd.edu:

You can confirm you have the new version of OCaml as follows:

If you want to make so that you always use the new version of OCaml, you can create (or edit, if it exists) the file .startup.tty in your home directory and add the source command from above. Running the following will add this line to that file. After doing this, the newer version of OCaml will be available when you log in without having to the source thing every time:

To test this, log out, log back in. If you run ocaml, you should see 4.04.0.

You should now be able to download, unpack, and compile the code skeleton for Project 1 on GRACE. Here’s a sample, showing how to do it:

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.

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 Integrity 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.