home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / specific / z / 537 < prev    next >
Encoding:
Text File  |  1993-01-25  |  3.0 KB  |  75 lines
  1. Newsgroups: comp.specification.z
  2. Path: sparky!uunet!paladin.american.edu!howland.reston.ans.net!usc!rpi!batcomputer!cornell!uw-beaver!jon
  3. From: jon@cs.washington.edu (Jon Jacky)
  4. Subject: Trees in Z (was: common data structures in Z)
  5. Message-ID: <1993Jan25.195022.5378@beaver.cs.washington.edu>
  6. Summary: Model a tree as a relation, not as records with embedded pointers
  7. Keywords: Z, tree, formal specification
  8. Sender: news@beaver.cs.washington.edu (USENET News System)
  9. Organization: Computer Science & Engineering, U. of Washington, Seattle
  10. Date: Mon, 25 Jan 93 19:50:22 GMT
  11. Lines: 62
  12.  
  13. C. M. Sperberg-McQueen <U35395@uicvm.uic.edu> writes:
  14.  
  15. > I'm having trouble formulating a good definition of trees,
  16. > despite the example of a definition of a binary tree in Spivey's manual. ...
  17. >
  18. > (complicated attempt using free types omitted...)
  19. >
  20. > I seem to be headed toward a bewildering tangle ...
  21. >
  22. > It's hard to believe that Z has been in use for over ten years without
  23. > anyone needing to specify arbitrary trees!  How did you do it?
  24.  
  25. This generic schema summarizes some techniques I've seen.  You don't need to
  26. bother with free types, and you don't need recursive data structures.  Remember
  27. that any graph composed of nodes and arcs can be modelled by a relation.  A
  28. tree is just a special case:
  29.  
  30.     +--Tree[Node]---------------------------
  31.     |  nodes: P Node
  32.     |  root: Node
  33.     |  parent: Node -+> Node
  34.     |  children: Node <-> Node
  35.     +---------------------------
  36.     |  root e nodes
  37.     |  dom parent U ran parent = nodes    
  38.     |  dom parent = nodes \ {root}
  39.     |  children = parent~
  40.     |  parent+ \cap id = empty
  41.     +--------------------------------------
  42.  
  43. Parent is declared to be a function, not a relation, to say that a node can
  44. have only one parent.
  45.  
  46. In order, the predicates say:
  47.  
  48. - The root is a node.
  49. - All the nodes are connected, and everything that is connected is in nodes.
  50. - Every node except the root has a parent.
  51. - The children relation is just the inverse of the parent function.
  52. - There aren't any cycles - no node is its own ancestor.   This is expressed
  53.   by saying the transitive closure of parent doesn't intersect the identity
  54.   function.  
  55.  
  56. I think that does it.
  57.  
  58. The key idea here is that structure of the tree is given by the parent function
  59. (or, equivalently, the children relation).   You do not need to include any
  60. embedded "pointers" (or references or names or whatever you want to call them)
  61. in the Node data type itself; there is no need for recursive data definitions.
  62. It's important that Node can be almost any data type, it doesn't need to have
  63. been designed in advance to fit into a tree. 
  64.  
  65. I think the problem with the attempt in the original posting was that it was
  66. too close to an implementation.  Instead of just modelling the tree itself as a
  67. relation, it tried to model the *implementation* of a tree as a data structure
  68. made out of records with embedded pointers.  
  69.  
  70. Jonathan Jacky                jon@radonc.washington.edu
  71. Radiation Oncology RC-08        voice:    (206)-548-4117
  72. University of Washington        FAX:    (206)-548-6218    
  73. Seattle, Washington  98195
  74. USA
  75.