Introduction to Programming in ATS:
<<< Previous	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 whose size is 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 (a) of ()
  | tree_cons (a) of (a, tree(a)(*left*), tree(a)(*right*))
// end of [tree]

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

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

<<< Previous	Home	Next >>>
Effectful Programming Features	Up	References