Binary-Tree Interpretations: Issues, and Designs

Binary-Trees are a recursive data structure
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 a 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 and mediator are in binary-tree-as-node-id-array.re
The interpretationof BINARY-TREEs as NODE-ID-ARRAYs bypasses 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 adds a layer of complex complex specs and interpretations. See the discussion of the interpretation below.
SpecWeb Index Interpretations

Binary-Trees as Array and Root

Abstractly, binary trees are maps from Node-Ids to tuples of Val, (left) Node-Id, and (right) Node-Id together with a distinguished Node-Id representing the root of the tree. In order to facilate the interpretation NODE-ID is specified as a definitional extension of NAT. The actual interpretation is constructed using the SORT-AS-QUOTIENT-OF-SUBSORT template as follows.

Interpretation of the sorts

Concrete-Sort
The Concrete-Sort is Array-and-Root. I.e., tuples of a root Node-Id and an Array of tuples of Val, Node-Id, Node-Id
Admissible-Rep-Subsort
The admissible-rep? predicate is: valid-tree? Abstractly, an Array-and-Root pair <A r> is a valid-tree? iff either r is the empty-node-id? (represents the empty-bbt) or r is a join-node-id? and the left and right Node-Ids represent binary-trees in A. In fact, we use an even stronger predicate: the Array-and-Root represents a binary-tree and the representation contains no junk (each element in the defined-dom of the Array represents some node of the tree) and no holes (if n is in the defined-dom of the array, then so is each m < n). This is equivalent to: the root represents a tree in A and the number of join nodes is one less than the size of A.
Note on order
The order (pre-, infix-, post-, etc) of the nodes in the array is not fixed by the admissible-rep? predicate. Fixing this order permits further optimization of the basic operations. In particular, once an order is specified, there will be just one element in each equivalence class. Hence, tree-equiv? would reduce to Array equal. Although the admissable reps are not restricted to reps with a particular order, the interpretations of the basic operations generate only post-order reps. In fact, it generates reps that are in what we will call a strong post-order form: every Node-Id of the left subtree precedes every Node-Id of the right subtree which in turn precedes the root (with necesary provisos for the empty Node-Id).
Abstract-Sort
The Abstract-Sort is obtained by factoring the valid-tree?s via the equivalence relation tree-equiv?. <A1 r1> is tree-equiv? <A2 r2> iff either r1 and r2 are both empty Node-Id-ids (= zero) or both are join Node-Id and the value at r1 in A1 equals the value at r2 in A2 and the corresponding left and right subtrees are tree-equiv?.

Some design issues

Order of traversal: post-fix
The order of traversal is apparent in two places: in recoding, the order used determines which result we get; in constructing a result, we get the same result regardless of the order used. The particular traversal order we use for generating new codes (node-ids) is (strong) post-fix order: recode the left subtree, then recode the right subtree, and then recode the current node.
Totality
Simple totality of arrays (defined on each nat less than their size) is achieved by: using null-val for the value of the empty-bbt; allocating an array of the precise size needed for the binary-tree being constructed (in each case the size of the result of a basic operation is a simple function of the size of the args).

Recoding

(bt-recode next-code old root new-so-far code-so-far)
next-code: (Node-Id -> Node-Id)
A recoding function which takes a single arg, code-so-far. The actual recoding function used is least-unused-code which simply adds one to the last new code used.
old: Array; root: Node-Id
A concrete binary-tree rep in the form: old (Array) and root.
new-so-far: Array
A partial result (whose incremented value is returned).
code-so-far: Node-Id
Contains the history of the recoding (i.e., the map from old node-ids to new node-ids, here simplified to just the last new node-id used)
returns: tuple of new-array-so-far, new-root, new-code-so-far

Interpretation of the basic operations

empty-bbt
The empty-bbt is represented by (the equivalence class containing) the pair: (empty-tree-array one), zero.
(empty-tree-array n) is a constant array of size n whose elements are all of the form: <null-val zero zero>
(join l-btr r-btr)
The array and root pair for (join* <Al rl> <Ar rr>) is constructed as follows:
  1. allocate an empty-tree-array rslt of size = size of Al + size of Ar
  2. recode/copy Al into rslt yielding l-rslt
  3. recode/copy Ar into l-rslt yielding r-rslt
  4. construct join node
(left btr)
The array and root pair for (left* <A r> is constructed as follows:
  1. allocate an empty-tree-array rslt of size of left subtree
  2. recode/copy the left subtree of A into rslt
(right btr)
The array and root pair for (right* <A r> is constructed as follows:
  1. allocate an empty-tree-array rslt of size of right subtree
  2. recode/copy the right subtree of A into rslt