Example: Testing for Braun Trees

Braun trees are special binary trees that can be defined inductively as follows:

Given a natural number n, there is exactly one Braun tree of size n. It is straightforward to prove that Braun trees are balanced.

A polymorphic datatype is declared as follows for representing binary trees:

datatype tree (a:t@ype) = | tree_nil of ((*void*)) | tree_cons of (a, tree(a)(*left*), tree(a)(*right*)) // end of [tree] // end of [datatype]

The following defined function brauntest0 tests whether a given binary tree is a Braun tree:

fun{ a:t@ype } size (t: tree a): int = case+ t of | tree_nil () => 0 | tree_cons (_, tl, tr) => 1 + size(tl) + size(tr) // end of [size] fun{ a:t@ype } brauntest0 (t: tree a): bool = ( case+ t of | tree_nil () => true | tree_cons (_, tl, tr) => let val cond1 = brauntest0(tl) andalso brauntest0(tr) in if cond1 then let val df = size(tl) - size(tr) in (df = 0) orelse (df = 1) end else false end // end of [tree_cons] ) (* end of [brauntest0] *)

The implementation of brauntest0 follows the definition of Braun trees closely. If applied to binary trees of size n, the time-complexity of the function size is O(n) and the time-complexity of the function brauntest0 is O(n(log(n))).

In the following program, the defined function brauntest1 also tests whether a given binary tree is a Braun tree:

fun{ a:t@ype } brauntest1 (t: tree a): bool = let exception Negative of () fun aux (t: tree a): int = ( case+ t of | tree_nil () => 0 | tree_cons (_, tl, tr) => let val szl = aux (tl) and szr = aux (tr) val df = szl - szr in if df = 0 orelse df = 1 then 1+szl+szr else $raise Negative() end // end of [tree_cons] ) (* end of [aux] *) in try let val _ = aux (t) in true // [t] is a Braun tree end with ~Negative() => false // [t] is not a Braun tree // end of [try] end // end of [brauntest1]

Clearly, a binary tree cannot be a Braun tree if one of its subtrees, proper or improper, is not a Braun tree. The auxiliary function aux is defined to return the size of a binary tree if the tree is a Braun tree or raise an exception otherwise. When the evaluation of the try-expression in the body of brauntest1 starts, the call to aux on a binary tree t is first evaluated. If the evaluation of this call returns, then t is a Braun tree and the boolean value true is returned as the value of the try-expression. Otherwise, the exception Negative() is raised and then caught, and the boolean value false is returned as the value of the try-expression. The time complexity of brauntest1 is the same as that of aux, which is O(n).

The use of the exception mechanism in the implementation of brauntest1 is a convincing one because the range between the point where an exception is raised and the point where the raised exception is captured can span many function calls. If this range is short (e.g., spanning only one function call) in a case, then the programmer should probably investigate whether it is a sensible use of the exception mechanism. For instance, the use of exception in the following example may seem interesting but it actually leads to very inefficient code:

fun{ a:t@ype } list0_length (xs: list0 (a)): int = try 1 + list0_length (xs.tail()) with ~ListSubscriptExn() => 0 // end of [list0_length]

Therefore, making use of exceptions in this style should be avoided.

Please find the entirety of the code in this section plus some additional code for testing on-line.