🚀 go-pugleaf

In article 5378@beaver.cs.washington.edu, jon@cs.washington.edu (Jon Jacky) writes:
>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.

No.  In the general case the ordering of the subtrees rooted at a given node
is significant.  At the very least children would have to have the type
Node -> seq Node.  

	Chris Flatters
	cflatter@nrao.edu

There's been some discussion about describing a generic model of trees
in Z.

Generic free type definitions are not in the language described in the
Z Reference Manual because I wasn't able to work out how to give them
a meaning in the kind of set theory I was using.  The crucial
difference between Z and functional programming languages like ML is
that constructions in Z are described with all the power of
first-order logic, so are not continuous, as the constructions
definable in ML are.  Non-generic type definitions are handled by
showing how to translate them into a given set declaration and an
axiomatic description, but this translation doesn't work for generics.

In the case of sequences, we get around the problem that there are no
generic free type definitions by constructing an explicit model: a
sequence over X is a function from an initial interval of the natural
numbers to the set X.  (Not quite: historical accident makes Z's
sequences start at 1 instead of 0 as they should -- there's flame
bait!)  This has the added advantage that we can define functions on
sequences "by construction" as well as by recursion.

We can do the same thing for various kinds of homogeneous trees: a
tree over X is a function from paths to X with a domin that is closed
under taking prefixes.  A path is a sequence of some kind of "step";
for example, you get binary trees by taking a step to be either 'L' or 'R'.

So the tree

			1	
			|
		+-------+-------+
		|		|
		2		5
		|
	+-------+-------+	
	|		|
	3		4

would be represented in the model by

	{ <> |-> 1, <L> |-> 2, <L,L> |-> 3, <L,R> |-> 4, <R> |-> 5 }


Different flavours of tree are obtained by taking different notions of
"step", and maybe adding extra closure conditions.  For example, trees
where every node has a sequence of children are obtained by taking
steps to be naturals, with the closure condition that

	s ^ <i> in dom T and j < i ==> s ^ <j> in dom T.

This model lets you define all the usual tree operations, and having
explicit paths lets you deal easily with specifications that have a
tree and a current place in the tree -- like a file system that has a
current directory.

-- Mike Spivey

+-----------------------------+-------------------------------+
| Mike Spivey,                | Phone:  (0865) 273838 (Work)  |
| Programming Research Group, |         (086 736) 641 (Home)  |
| 11, Keble Road,             | FAX:    (0865) 273839         |
| Oxford, OX1 3QD, England.   | E-mail: mike@uk.ac.oxford.prg |
+-----------------------------+-------------------------------+