home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / specific / z / 541 < prev    next >
Encoding:
Internet Message Format  |  1993-01-28  |  3.2 KB
  1. Path: sparky!uunet!ukma!usenet.ins.cwru.edu!agate!doc.ic.ac.uk!uknet!comlab.ox.ac.uk!hpl.hewlett-packard.co.uk
  2. From: mjw@hpl.hewlett-packard.co.uk (Mike Wray)
  3. Newsgroups: comp.specification.z
  4. Subject: Re: Trees in Z (was: common data structures in Z
  5. Message-ID: <9301280844.AA16817@mwray.hpl.hp.com>
  6. Date: 28 Jan 93 08:44:14 GMT
  7. Lines: 105
  8. X-Mailer: mail-news 2.0.3
  9.  
  10.  
  11. Continuing the discussion about generic free types,
  12. it seems to me that they would be prefectly OK in Z because
  13. they have a direct translation into existing Z.
  14.  
  15. At present we can define a tree of integers (using Z for the integers):
  16.  
  17.  
  18.     ITREE = leaf<<Z>> | join<< Z X ITREE X ITREE>>
  19.  
  20. This stands for (more or less)
  21.  
  22.     [ITREE]
  23.  
  24.     [ leaf: Z -> ITREE; join: Z X ITREE X ITREE -> ITREE |
  25.       
  26.       your favourite axiomatisation of freely generated ]
  27.  
  28. and is a convenient shorthand for the axioms defining
  29. freely generated.
  30.  
  31.  
  32. A similar interpretation can be given to generic free types.
  33. Consider a putative generic tree type:
  34.  
  35.     TREE[A] = leaf<<A>> | join<< A X TREE[A] X TREE[A]>>
  36.  
  37. with ITREE defined using it:
  38.  
  39.     ITREE = TREE[Z]
  40.  
  41. What does this mean? Consider the schema
  42.  
  43.  
  44.  *- TREE[A, B] -----------------------------------------
  45.  |
  46.  | leaf: A -> B
  47.  |
  48.  | join: A X B X B -> B
  49.  |
  50.  +------------------------------------------------------
  51.  |
  52.  | leaf and join are bijections onto their ranges,
  53.  | their ranges partition B,
  54.  | B is the least set closed under join
  55.  | (or any of the many equivalent closure properties)
  56.  +------------------------------------------------------
  57.  
  58. We can now declare ITREE and assert the TREE property of it:
  59.  
  60.     [ITREE]
  61.  
  62.     TREE[Z, ITREE]
  63.  
  64. More generally, a generic free type
  65.  
  66.  
  67.     Free[A] = f1<< Type1>> | .... | fn<< Typen>>
  68.  
  69. Corresponds to the schema
  70.  
  71.  *- Free[A, B] -----------------------------------------
  72.  |
  73.  | f1: Type1(B/Free[A]) -> B
  74.  |
  75.  | ...
  76.  |
  77.  | fn: Typen(B/Free[A]) -> B
  78.  |
  79.  +------------------------------------------------------
  80.  | The fi are bijections onto their ranges,
  81.  | the ranges partition B,
  82.  | closure property (B is closed under any fj with B as 
  83.  | an argument type)
  84.  +------------------------------------------------------
  85.  
  86.  where Type1(B/Free[A]) means Type1 with B substituted for Free[A].
  87.  
  88.  
  89.  An instance C = Free[D] corresponds to
  90.  
  91.     [C]
  92.     Free[C,D]
  93.  
  94. Thus, we interpret a generic free type as a schema which can be
  95. used to define instances.  Indeed, one can use this technique to
  96. simulate generic free types in Z today.
  97. The same technique extends to free types of more than one 
  98. parameter, and is equivalent to the present semantics for
  99. zero parameters.
  100.  
  101.  
  102. Mike Wray
  103.  
  104.  
  105.  +----------------------------------+-------------------------------------+
  106.  |                                  |   Mike Wray                         |
  107.  |     mjw@hplb.hpl.hp.co.uk        |   Hewlett-Packard Laboratories      |
  108.  |     mjw@hplb.hpl.hp.com          |   Filton Road                       |
  109.  |                                  |   Stoke Gifford                     |
  110.  +----------------------------------+   Bristol        BS12 6QZ           |
  111.  | Phone +44 272 228262 Direct      |   UK                                |
  112.  |       +44 272 799910 Switchboard |                                     |
  113.  +----------------------------------+-------------------------------------+
  114.  
  115.