Introduction to Programming in ATS:
Prev	Chapter 6. Effectful Programming Features	Next

Example: Testing for Braun Trees

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

If a binary tree is empty, then it is a Braun tree.
If both children of a binary tree are Braun trees and the size of the left child minus the size of the right child equals 0 or 1, then the binary tree is a Braun tree.

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
(
t0: tree(a)
) : int =
(
case+ t0 of
| tree_nil() => 0
| tree_cons(_, tl, tr) => 1 + size(tl) + size(tr)
) (* end of [size] *)

fun{
a:t@ype
} brauntest0
(
t0: tree(a)
) : bool =
(
case+ t0 of
| tree_nil() => true
| tree_cons(_, tl, tr) => let
    val test = brauntest0(tl) andalso brauntest0(tr)
  in
    if test
      then let
        val dif = size(tl)-size(tr) in (dif=0) orelse (dif=1)
      end else false
    // end of [if]
  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
(
t0: tree(a)
) : bool = let
//
exception Negative of ()
//
  fun
  aux
  (
  t0: tree(a)
  ) : int =
  (
    case+ t0 of
    | tree_nil() => 0
    | tree_cons
        (_, tl, tr) => let
        val szl = aux(tl)
        and szr = aux(tr)
        val dif = szl - szr
      in
        if (dif=0 orelse dif=1) then 1+szl+szr else $raise Negative()
      end // end of [tree_cons]
  ) (* end of [aux] *)
//
in
  try let
    val _ = aux(t0)
  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.