🚀 go-pugleaf

C. M. Sperberg-McQueen <U35395@uicvm.uic.edu> writes:

> I'm having trouble formulating a good definition of trees,
> despite the example of a definition of a binary tree in Spivey's manual. ...
>
> (complicated attempt using free types omitted...)
>
> I seem to be headed toward a bewildering tangle ...
>
> It's hard to believe that Z has been in use for over ten years without
> anyone needing to specify arbitrary trees!  How did you do it?

This generic schema summarizes some techniques I've seen.  You don't need to
bother with free types, and you don't need recursive data structures.  Remember
that any graph composed of nodes and arcs can be modelled by a relation.  A
tree is just a special case:

	+--Tree[Node]---------------------------
	|  nodes: P Node
	|  root: Node
	|  parent: Node -+> Node
	|  children: Node <-> Node
	+---------------------------
	|  root e nodes
	|  dom parent U ran parent = nodes	
	|  dom parent = nodes \ {root}
	|  children = parent~
	|  parent+ \cap id = empty
	+--------------------------------------

Parent is declared to be a function, not a relation, to say that a node can
have only one parent.

In order, the predicates say:

- The root is a node.
- All the nodes are connected, and everything that is connected is in nodes.
- Every node except the root has a parent.
- The children relation is just the inverse of the parent function.
- There aren't any cycles - no node is its own ancestor.   This is expressed
  by saying the transitive closure of parent doesn't intersect the identity
  function.  

I think that does it.

The key idea here is that structure of the tree is given by the parent function
(or, equivalently, the children relation).   You do not need to include any
embedded "pointers" (or references or names or whatever you want to call them)
in the Node data type itself; there is no need for recursive data definitions.
It's important that Node can be almost any data type, it doesn't need to have
been designed in advance to fit into a tree. 

I think the problem with the attempt in the original posting was that it was
too close to an implementation.  Instead of just modelling the tree itself as a
relation, it tried to model the *implementation* of a tree as a data structure
made out of records with embedded pointers.  

Jonathan Jacky				jon@radonc.washington.edu
Radiation Oncology RC-08		voice:	(206)-548-4117
University of Washington		FAX:	(206)-548-6218	
Seattle, Washington  98195
USA