Homework 3

Due: Friday, January 30th at 11:59pm.

Submission Instructions

Start with the template code, provided here.

• Replace each failwith "TODO" with your solution. (failwith has type string -> t for any type t, and throws an exception when it evaluates. Your solution to each problem should not include failwith.)
• Be sure to test your solutions in utop or in tests alongside your submission. To load your file into utop, use #use "hw3.ml";;.
• Submit your version of hw3.ml to the HW3 assignment on Gradescope. Only submit hw3.ml; not any other files or folders.

• At the top of the template file, there is a comment for you to write in approximately how many hours you spent on the assignment. Filling this in is optional, but helpful feedback for the instructors.

Binary Search Trees

A binary search tree is an efficient data structure for implementing a map, which allows you to insert key/value pairs, look up the value for a key, and remove keys from the map.

type entry = 
  { key : int; value : string }

type bst = 
  | Leaf
  | Node of bst * entry * bst

This homework will task you with implementing various operations on binary search trees and debugging their correctness using PBT.

Q1: Writing some specs (15 points, autograded)

To use PBT, we first need to come up with specifications: functions that we take as definitions for correctness.

Grading criteria for Q1

We will be using property based testing to check whether your version of sorted computes the correct answer.

Q1.1 (5pts) First, implement a function has_key to test if a certain key is in a binary search tree:

let rec has_key (t : bst) (k : int) : bool = failwith "TODO"

Q1.2 (5pts) Additionally, implement a function has_entry to test if a certain entry is in the tree:

let rec has_entry (t : bst) (e : entry) : bool = failwith "TODO"

Q1.3 (5pts) Finally, we will need to test if a tree is sorted. The definition of "sorted" for our bst type is similar to int_tree from last homework, except that we perform comparisons over the keys. In other words, a bst is sorted if for every Node(x, e, y) in the tree, e.key is greater than or equal to all keys stored in x and less than or equal to all keys stored in y.

let rec sorted (t : bst) : bool = failwith "TODO"

Q2: A generator for BSTs (5 points, manually graded)

Next, use functions from Random to implement a generator gen_bst for bsts. You can find documentation for Random here. This generator will take an integer n to serve as a bound for the maximal depth of the tree.

let rec gen_bst (n : int) : unit -> bst = failwith "TODO"

You are free to write the generator in any style you wish, as long as it is useful for your PBT experiments. Later exercises will grade you on whether your PBT tests actually find bugs, so it cannot be trivial. Feel free to use randomness to generate unbalanced trees.

Note: here, a value of the bst type is, without any additional properties, a "raw" binary search tree, which might not be sorted. Do not assume values of type bst are sorted without explicit properties which state so.

Grading criteria: Q2

While later problems will depend on your gen_bst generator being useful, we will grade gen_bst itself on whether it successfully uses randomness to produce any tree.

Aside: forall functions for using generators

Next, we'll provide some forall functions that you will need to use to help with Q3 and Q4. We will use generators to conduct property-based tests; i.e., random sampling to test if universally-quantified formulas are true.

Below is a version of forall that uses gen_bst from Q2 as well as an entry to a bst:

let rec forall_bst_entry
    (gen_bst : unit -> bst)
    (gen_entry : unit -> entry) (* you would need to implement this *)
    (prop : bst * entry -> bool)
    (trials : int)
  : (bst * entry) option = 
  if trials <= 0
  then None
  else 
    let x = gen_bst () in 
    let y = gen_entry () in 
    let xy = (x, y) in
    if prop xy
    then forall gen prop (trials - 1)
    else Some xy

We will also give you versions of forall that lets you quantify over keys:

let rec forall_bst_key
    (gen_bst : unit -> bst)
    (gen_key : unit -> key) (* you would need to implement this *)
    (prop : bst * string -> bool)
    (trials : int)
  : (bst * string) option = 
  if trials <= 0
  then None
  else 
    let x = gen_bst () in 
    let y = gen_key () in 
    let xy = (x, y)
    if prop xy
    then forall gen prop (trials - 1)
    else Some xy

Q3: Looking up a key (25 points, manually graded)

Q3.1 Given an arbitrary binary search tree, if we want to look up the value with a given key, the best we can do is search through the whole tree --- since the key might be anywhere. Implement this:

let rec lookup (t : bst) (k : int) : string option = failwith "TODO"

Here, you should return Some v, if v is the value associated to the first entry you find that matches key k. If no entry matches, return None.

Grading criteria: Q3.1

Whether your function type checks and does not contain failwith. We will evaluate its correctness in the next question.

Q3.2

Next, we will check that it is correct by using PBT. Show using PBT that the following formula is (most likely) true:

\[(P1)\ \forall t \in \texttt{bst}, \forall k \in \texttt{int}, \mathsf{lookup}(t, k) = \mathsf{None} \iff \mathsf{has\_key}(t, k) = \mathsf{false}.\]

In natural language: \((P1)\) states that if \(\mathsf{lookup}(t, k)\) returns \(\mathsf{None}\), then \(k\) must not be in the tree. To show property \((P1)\), define a function called p1 that contains a use of forall2 to demonstrate this property.

let p1 () : (bst * int) option = failwith "TODO"

This theorem should return None if and only if forall2 cannot find a counterexample. You will need to write your own generator for ints.

Grading criteria: Q3.2

Whether p1 correctly uses forall2 to implement and evaluate the theorem \((P1)\) (using gen_bst to generate the bsts); and if PBT does not find any counter-examples.

Q3.3 Next, use PBT to evaluate the following property:

\[ (P2) \forall t \in \texttt{bst}, \forall \texttt{e} \in \texttt{entry}, \mathsf{lookup}(t, \texttt{e.k}) = \mathsf{Some}\ \texttt{e.v} \iff \mathsf{has\_entry}(t, e).\]

This property is false. Using forall2, implement p2 to test whether (P2) is true or false. This will require you to write a generator for entry. Additionally, using your local PBT experiments, find a counter-example and write the counter-example (a pair of a bst and entry which makes the property false) in lookup_has_entry_counter_example. Additionally, write in a comment above why the property is false. If your gen_bst generator cannot find a counter-example, you should go back and tweak it so that it does.

(* This property is false, so it should return a counter-example. *)
let p2 () : (bst * entry) option = failwith "TODO"

(* Briefly explain below why this counter-example breaks the property:

    TODO

*)
let p2_counter_example () : (bst * entry) = 
  failwith "TODO"

Grading criteria: Q3.3

Whether:

• p2 correctly uses forall2 to implement and evaluate property \((P2)\) (using gen_bst to generate the bst);
• You have written a correct counter-example for \((P2)\) in p2_counter_example.
• You have a brief explanation in a comment above p2_counter_example that explains why the property is broken on the counter-example.

Q3.4 While \((P2)\) is false, a slightly fixed version of \((P2)\) is true:

\[ (P2')\ \forall t, \forall \texttt{e}, \mathsf{lookup}(t, \texttt{e.k}) = \mathsf{Some}\ \texttt{e.v} \implies \mathsf{has\_entry}(t, e).\]

Note that we use "\(\implies\)" rather than "\(\iff\)". Using forall2, implement the below test which should use PBT to evaluate the correctness of \((P2')\). Additionally, in a comment above p2', write a brief explanation for why \((P2')\) is true but \((P2)\) is false.

(* Why is (P2') true? 

  TODO 

*)
let p2' () : (bst * entry) option = failwith "TODO"

Grading criteria: Q3.4

Whether:

• p2' correctly uses forall2 to implement and evaluate the theorem \((P2')\) (using gen_bst to generate the bst); and if PBT does not find any counter-examples;
• Your comment adequately explains why \((P2)\) is false, but \((P2')\) is true.

Q4: Using sortedness to lookup a key faster (30 points, manually graded)

Above, lookup needs to potentially traverse the whole tree, which can be prohibitively slow. However, given a sorted tree, we can do better. Since the tree is sorted, we can test if the key we are searching for is larger or smaller than the current entry's key; based on this information, we can go left or right. This means we do not traverse the whole tree, but only a certain path of it.

Q4.1 Implement this faster lookup:

let rec lookup_sorted (t : bst) (k : int) : string option = failwith "TODO"

Grading criteria: Q4.1

Whether your function type checks and does not contain failwith. We will evaluate its correctness in the next question.

Correctness of lookup_sorted

(Part of) the correctness of lookup_sorted is that it should not return None if the key actually is in the tree. But this is only true for sorted bsts:

\[ (P3) \forall t \in \texttt{bst}, \forall k \in \texttt{int}, \mathsf{sorted}(t) \implies \big(\mathsf{lookup\_sorted}(t, k) = \mathsf{None} \iff \mathsf{has\_key}(t, k) = \mathsf{false}\big). \]

We can show this property in two ways.

Q4.2 First, use forall2 with your gen_bst generator to show that the above property is true for all t and k:

let p3 () : (bst * int) option = failwith "TODO"

While the above likely won't find a counter-example, the above is not a very good test. Depending on how you wrote your gen_bst function, it might be the case that you almost never generate a sorted function; and thus, the left hand side of the implication will always be false.

Grading criteria: Q4.2

Whether p3 correctly uses forall2 to evaluate the truth value of \((P3)\) (using gen_bst to generate the bsts); and if it does not find any counter-examples.

Q4.3 To fix this, we need to write a generator for bsts that makes the left-hand side of the implication true. Thus, write a generator for bst that should always return a sorted bst:

let rec gen_sorted (n : int) : unit -> bst = failwith "TODO"

Grading criteria: Q4.3

Whether your function type checks and does not contain failwith. We will evaluate its correctness in the next question.

And evaluate two properties:

Q4.4 First, gen_sorted actually returns sorted bsts. To do this, pick a bound n, and use forall to test whether sorted is true for outputs of gen_sorted n:

let gen_sorted_property () : bst option = failwith "TODO"

(This should always return None, if gen_sorted and sorted are written correctly.)

Grading criteria: Q4.4

Whether you correctly use forall to evaluate if gen_sorted always returns sorted trees.

Q4.5 Second, that our property about lookup_sorted is still true when we use gen_sorted instead of gen_bst:

let p3_gen_sorted () : (bst * int) option = failwith "TODO"

Grading criteria: Q4.5

Whether you correctly use forall2 to evaluate if property \((P3)\) is true when using gen_sorted as the generator for bsts.

Violating lookup_sorted's hypothesis

Q4.6 If we consider all bsts, instead of the sorted ones, then the conclusion of \((P3)\) is false. That is, the below statement is false:

\[ (P4) \forall t \in \texttt{bst}, \forall k \in \texttt{int}, \mathsf{lookup\_sorted}(t, k) = \mathsf{None} \iff \mathsf{has\_key}(t, k) = \mathsf{false}. \]

Give a counter-example for the above statement's truth below:

let p4 () : (bst * int) = failwith "TODO"

Grading criteria: Q4.6

Whether the value you construct for p4 causes the conclusion of \((P4)\) (i.e., \(\mathsf{lookup\_sorted}(t, k) = \mathsf{None} \iff \mathsf{has\_key}(t, k) = \mathsf{false}\)) to be false.