Binary-Trees

Binary-Trees: Concepts, Issues, and Designs

Binary-Trees are NOT Trees

Binary-Trees are not trees: they are a (ML like) recursive data type. In particular, a subtree can have more than one ancestor; there can be more than one "path" to the "root". Consider (join t t)

Constructors and Destructors

The constructors are empty-bbt and join. The destructors are: left and right. There is a single testor: empty-bbt?

Issue in designing interpretations of Binary-Trees

As mentioned, binary-trees are not trees: they are a (ML like) recursive data type. Interpretations then factor into two steps:

Interpretation of recursive data types

The problem is how to define an constructive sort to implement the recursive sort. A primary technique is to introduce a sort of atoms ("objects" or "identifiers") for the elements and interpret the constructors and destructors as maps over the atoms. A refinement of this technique is to introduce a product (record) structure and interpret each recursive structure (e.g., binary-tree) as a map from identifiers to tuples some of whose components are identifiers.

Interpretation of the data types introduced

For example, interpretation of the maps as ARRAYs or LISTs.

BINARY-TREEs as NODE-ID-ARRAYs

The interpretation of BINARY-TREEs as NODE-ID-ARRAYs goes directly to ARRAYs skipping maps because the map interpretation requires so much structure (FINITE-SORT domain etc) that the resulting spec is equivalent to ARRAY. Hence, the map step just a layer of complex complex specs and interpretations.

Binary-Trees: Specs, interpretations etc

Binary-Tree Spec

binary-tree.re

BINARY-TREEs as NODE-ID-ARRAYs

binary-tree-as-node-id-array.re

SpecWeb Index

Specs