🚀 go-pugleaf

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 |
+-----------------------------+-------------------------------+