Tree Specification

We saw 3 styles of specifications for Lists:

Classical: list = collection of nodes.
Recursive: list is either empty or consists of a head an a tail (which is a list).
Ours: features operations of whole lists rather than on individual elements (SPLIT, JOIN).

Trees generalize lists. A list is a degenerate tree.

Classical: tree = collection of nodes, where each node has exactly 1 predecessor (except the root which has none).
Recursive: binary tree is either empty of consists of a value, left subtree, and right subtree.

Our specification: notion of subtree.

We discussed the issue of JOINing lists. The same problems arise with trees and the same solutions apply.

Here, we choose to changes the type of a tree to subtree when necessary and restrict some operations to only work on trees.