THE UNIVERSITY OF MICHIGAN COMPUTING RESEARCH LABORATORY ON THE RELATIONSHIPS BETWEEN SCOTT DOMAINS, SYNCHRONIZATION TREES, AND METRIC SPACES. William C. Rounds CRL-TR-25-83 JULY 1983 Room 1079, East Engineering Building Ann Arbor, Michigan 48109 USA Tel: (313) 763-8000

On the relationships between Scott domains, synchronization trees, and metric spaces. William C. Rounds Department of Computer and Communication Sciences'University of Michigan I. Introduction Scott's theory of Information Systems [S] is intended to provide an easy way to define partial order structures (domains) for denotational semantics. This paper illustrates the new method by considering a simple modal logic, due to Hennessy and Milner [HM], as an example of an information system. The models of formulas in this logic are the rigid synchronization trees of Milner [M]. We characterize the domain defined by the Hennessy-Milner information system as the complete partial order of synchronization forests: nonempty closed sets of synchronization trees. "Closed" means closed with respect to a natural metric distance on synchronization trees, first defined by de Bakker and Zucker [BaZ] and characterized by Golson and Rounds [GR]. After notational preliminaries and background results, Section III treats the Hennessy-Milner information system. The background results [BR], [GR] are used as lemmas in the characterization of the partial order. The next part (Section IV) shows how to use metric space methods to extend certain natural tree operations to forests. These operations become sup-continuous when so extended, and therefore can be used to provide a denotational semantics for concurrency which allows the full power of least-fixed point methods for recursion (Section V). From the results in this paper, we conclude that the Information System approach to denotational semantics shows real promise. We began by investigating the Hennessy-Milner information system as a way to construct complete

-2partial orders for synchronization trees. The result was a surprisingly natural construction of a complete partial order which we might not have found without the tools provided by information systems. II. Notation and previous work Definition 2.1. Let Z be a finite alphabet. A S-tree is a tree graph on a nonempty finite or countable set of nodes, with arc labels from Z. No ordering on the arcs leaving a node is presumed, and more than one such arc may have the same label. Nodes are unlabeled, although leaf nodes are considered to be the one-node tree NIL. E-trees are the rigid synchronization trees of Milner [M]. They correspond to'unfoldings' of state graphs for nondeterministic transition systems. Milner develops an algebraic system based on these trees and their generalizations, suitable for a semantics for communicating systems. Our purpose here is to show a way of associating a Scott order structure (domain) to Z-trees. First we need to recall some definitions. Notation. Suppose t is the Z-tree represented by a. a (a E Z) I n We then write t = Za.t. The same notation will suffice for a tree with countably 1 1 many arcs from the root. For each a e Z we define the binary transition relation a — > on the set TZ of all E-trees by a t a> u iff t = Za.t., a = a. for some i, and u = t.. 2. 1~~~

-3Definition 2.2 (weak observational equivalence). Let a series Wk (k>O) of equivalence relations on Tz be given as follows: t W0 u always; t Wk u <=> (Vt',a)[t -> t' => (3u')(u u and u' W t')] and vice versa. The. weak observational equivalence W on T is given by t W u <=> (Vk>O) (t W u), Examples. Let Z={a,b,c} a a b b b a/ a 2/' W2 W/X2 Hennessy-Milner logic (HML) first appeared in [HM] as a language for describing s-trees (or transition systems). Definition 2.3. HML is the least class of formulas containing the Boolean constants tt and ff, and closed under Boolean connectives A, V, - and under application of the (unary) modal operators 6 for each acZ. Examples. ( ( tt A O tt) n+a (< ttV V tt) Definition 2.4. (Semantics of HML). Let ~s HML. t s T satisfies f (t I 9) iff one of the following inductive cases holds: (i) = tt <=> teTE (ii) 9 = ~^A <=> t = 9 and t = 8:(iii) 9= 4 <=> not (t D= p) (iv) 9 = ~iv <=> t = 9 or t b 9 (v) 9= 9 B <=> (u)(t q u A u = 9).

-4Examples. b 8 9 = ^ ( ttA tt A l tt) bas aA b |. Definition 2.5. The modal rank r(9) of a formula s HML is defined inductively r(tt)=r(ff)=0; r (V I) =r (fA p) =max{r (C),r (p) }; r('-I) =r () r4<, 9 =r',). Let HM= L { e HML I r () < k}. Definition 2.6. (Elementary equivalence) Define the equivalences E and E on Tv by t Ek u <=> V esHML(k) [t, <=> u J -], and t E u <=> (Vk) t E U. Finally we have the notion of logical equivalence. Definition 2.7. = i iff Vt(t 9 <=> t JI). The proofs of the following facts can be found in [BR] and [GR]. Note: Lemma 2.1. For all t, u s Ty, and k > 0, t Wk u <=> t E u. Corollary: W = E. Lemma 2.3. (Master formula theorem for HML.) For each s-tree t and each k>O there is a formula C(k,t) s HMLk such that (i) t g(k,t) (ii) for all u, if u F 9(k,t) thenu Wk t. kc

-5Lemma 2.4.. (Compactness theorem for HML.) Let PCHML. If every finite subset of r has a tree model then so does r. Let Mod(r) be the set of tree models of r; that is, {t | (VEr) (t 9)}. The compactness theorem states ((v F finite p r) Mod(F) 0) implies Mod(P) 0. We note that 2.4 holds even for infinite Z. Finally, we recall some facts about the "Golson metric" d on TE. Definition 2.8. Let e (t,u)-=max{k I t W u} with e (t,u)= — if t W u. w k w The pseudo-metric distance d (t,u) is then given by 2w u, where w 2 =0. d is actually an ultrametric on T. We have w' " d (t,v) < max(dw(t,u), d (u,v)). w w w Jurther, dw(t,u)=0<=> t W u, so that d is a metric on TE/W. (k) Definition 2.9. The k-section t of a tree t is defined to be the set of nodes at distance k or less from the root, together with the relevant arcs. The O-section is then just the one-node root. (k) (k) Lemma 2.5. t W u <=> t ) W u Lemma 2.6. d (t(k),t) + 0 as k +. Lemma 2.7. <T /W, d > is a compact metric space. Recall that a compact space is one where every covering by open sets has a finite subcovering. For a metric space it is equivalent to saying that every infinite sequence has a convergent subsequence.

-6III. Information systems and Hennessy-Milner logic First we recall the general definition of information system from Scott IS]. Definition 3.1. An information system is a structure <D,', Con, F-> where D is a set of'propositions','OeD is the least informative proposition, Con is a collection of finite subsets of D (the finite consistent sets), and I- is the entailment relation, a subset of Con x D. The following axioms hold: (i) P e Con A sP => A ~ Con; (ii) {5} c Con for all f C D; (iii) r e- H A P s Con =>P U{T} c Con; (iv) Pr Con => F c- (v) p e Con ^ 9 e r => r (vi) r H- 9 for all 9 ~ A and A F- => r - 8. An information system is a way of giving'facts', expressed in D, about abstract structures. The more'facts' we know, the more'well-defined' the structure becomes. We can express these notions purely in terms of D itself using sets of propositions. Definition 3.2. The ideal elements defined by the information system D are those subsets r of D satisfying (i) r is consistent: Every finite A c r is a member of Con; (ii) P is deductively closed: A c A, A e Con, and A - 8 => 0 ~ P. An element P is total if it is maximal with respect to the inclusion ordering on PD, and otherwise partial. Lemma 3.1. The ideal elements ID of an information system D form a complete partial order under ordinary inclusion.

-7For our purposes, all we need to know about complete partial orders is that every chain P. has a supremum UP.. In this case the union of the r. sets is the obvious supremum. It can be shown that the cpo's defined by information systems are exactly the consistently complete, algebraic cpo's. See [S] for details. HML as an information system. HML provides a natural example of an information system describing sets of E-trees. Definition 3.3. The HML system is given by: D={eHML | (3t) (t I) )}; Con={A c HML I A finite A Mod(A) A 0}; 9 =tt; A A- 0 <=> (Vt) [(VtEA) (t p *) => t 1 8]. (Alternatively, if A={91,'....,' }, A.'.A^ + is valid.) n n We want to characterize the abstract cpo <I, > in terms of E-trees. To do this we need two simple definitions. Definition 3.3. Let E be an equivalence relation in TZ. A set KcT is E-closed iff u e K and t E u imples t e K. Definition 3.4. KST is metric-closed iff t. K and d (ti,t)-0 imply.....1 w 1 t W t for some t e K. Let P (TZ) be the set of all nonempty W-closed, metric-closed subsets of c TV. (The elements of P (T.) are called Z-forests.) L c Theorem 3.2. <IHML- > is isomorphic to <P (T ), >. Proof. Consider the map P + Mod(P) from IHML to P(T ). We verify that Mod is the required isomorphism.

-8(i) r C', <=> Mod(r)' Mod(P'). The => direction is trivial. Consider the reverse implication. Suppose Mod(P) Mod(P') and let 8 e r. By 3.2, we need only find a finite A'S P' such that A - 9. Suppose this is not the case: for every finite subset A of rf, we have - (A - 8). Let A={1,..., }1: we have that AU{ 98} has a tree model, n because -(0,A..A0 +-9) is satisfiable. So every finite subset of r'U{f-9} has n a tree model, and therefore by compactness r'U{n0} has a tree model. But if t e Mod(P'), t s Mod(r) by hypothesis. However, e8 P, so t = 8,and t t= e, a contradiction. (ii) Mod(P) is metrically closed and W-closed. Certainly Tod(f) is W-closedJ ecause of 2.3. Let d (t,t) >O wher.e t c riod i. w n n Suppose that t is not W-equivalent to any u in Mod(P). Then there is some 0 e r such that t t =0. Let p be the modal rank of 80. Choose n such that d (tt)<l/2P. w n Then t W t so by 2.1, t E t. But t = 8 and t - ne, a contradiction. n p n p n (iii) If K is W-closed and metrically closed, then (31) K = mod(P). Let P = {9[ (Vt E K) (t t )}. It is easy to check that P is consistent and deductively closed. Certainly K CMod(P) by definition. We assert Mod(P) K; To show this we let t E Mod(P) and construct a sequence <s > such that d (s,t)-+ and s s K. n w n n Fix n>O. For each s ~ K let 9(n,s) be the master formula s HML satisfied -~~~~~~~~~~~- n by s(Lemma 2.3). By lemma 2.2 there are only a finite number of logically distinct?(n,s) as s ranges over K. Let = V. (n,s). This is a finite disjunction, and Vs~K, s = 9, so n SEK n <n ~ r. Since t e Mod(P) t = P. By definition of T, 3s ~ K such that t' 9(sn n and 2.7 d(t,.s )-Q. n

-9Now (i) shows that the map r + Mod(P) is one-one and order-preserving, and (ii) and (iii) show that it is onto. This completes the proof of Theorem 3.2. As corollary, we have the following proposition. Corollary 3.3. The maximal elements of <P (T ),2> are the (equivalence classes of) singleton Z-trees; the bottom element is the set T itself. It is an instructive exercise to show this corollary directly from the definition of <IHML, S> IV. Forests and operations on forests Definition 4.1. A Z-forest is a metrically closed, W-closed subset of TZ. We. recall the notion vf IIauidorff dcistance between closed subsets of a metric space. Definition 4.2. Let <X,d> be a metric space, and Y,Z closed subsets of X. d (Y,Z)=max{sup{d(yz)}, sup{d(z,Y)}} H ysY zeZ where d(y,Z)=inf{d(y,z)}. zCZ Intuitively, d(Y,Z) is the maximum distance any point in Y must travel to enter Z, or vice versa. We would like to characterize dH when d is the Golson metric d. To do this we extend the Wk and W relations to forests in the expected way. Definition 4.3. Let H and H' be forests. H W H' <=> (VteH) (3t'eH')t W t' and conversely. k k H W H' <=> (VtsH) Gt'SH')t W t' and conversely. Lemma 4.1. H W H' <=> (Vk)(H Wk H').

-10Proof. (=>) is trivial. Let H W H' for each k. If t c H, then for each k there is a tk E H' such that t Wk tk. Thus d (tk,t)+0, which implies t c H' k k K wk because H' is a forest. Similarly H' C H, completing the proof. (k) (k) Lemma 4.2. H WH'<=>H W whe H k) where H = {t t e H} and t is the k-section of t (Definition 2.9). Proof. routine. Definition 4.4. (Golson metric on forests) 1 d (H,H') = e(H,H') where e (H,H') = maxtk H W H'} w k with the usual proviso l/X= 0. Lemma 4.3. d is a metric on forests. w Proof. routine. Theorem 4.1. d =d. w H Proof. (d <d ). Let j=e (H,H'), so d (HH')=l/2j H- w w w => VtsH 3t' H'ed (t,t')< w -2) => inf d (t,H')< 1/2j for all t~H teH w => sup d (t,H')< 1/23 tlH w Similarly sup d (t',H)< 1/2 t'SH' w and the inequality holds. Now we want d >d. Again let d (H,H')=l/23 with j as above. If j=x there is nothing to show. Therefore we have j<c and H -Wj+.H'.

-11=> (3tsH)(Vt'H')dw(tt')> 2j+l or the same assertion with the roles of H,H' reversed. In the first case, which occurs without loss of generality, we have (3tsH) (Wt'H') d (t,t')>l/2 w - because d takes only discrete values. Therefore w inf d (t,t')=d (t,H')>1/23 W W - t' H' and so sup d (t,H')>1/2 teH and the inequality follows. An extension theorem for compact metric spaces. The space AT of trees admits A numbrer of operations saitable for def:ni-ng semantics for concurrency. DeBakker and Zucker, in particular, consider the operations of "sum" - joining trees at the root;, "shuffle" - interleaving trees nondeterministically; and "composition" - grafting one tree to terminating nodes of another. They prove these operations to be continuous in the metric topology of T. We would like to extend these operators to forests in a manner analogous to extending string-valued functions to languages. We present a general theorem which allows this in any compact metric space. In what follows, X is such a compact space, and G, H, and K are closed (hence compact) nonempty subsets. Lemma 4.4. If H,K!CX, then there is a k~K such that d(K,H)=d(k,H). Also, for any keK, there is an h~H such that d(k,H)=d(k,h). Proof. We show only the second result; the first is proved similarly. Recall that Xy. d(x,y) is a continuous function of y for fixed x. (So also is Xx. d(x,H).) Since d(k,H)=inf d(k,h), we can find a sequence h. E H such hsH that d(k,h.) approaches d(k,H). Since H is compact the h. have a convergent 1I 1

-12subsequence hij such that hij h c H as j-x.w By continuity of d, we know lim d(k,hi) = d(k,h). But lim d(k,hi) = lim d(k,hi) = d(k,H). J it j-*o:j-3 iLemma 4.5. Let <K.> be a decreasing chain of nonempty closed subsets of 1 X and let k. C K. for each i. Then there is a convergent subsequence kij-k with k E Qk Ki. Proof. By compactness there is a k and subsequence ki.+k as j-+. We need k e K. for each i. It is enough to show k E Kij for each j. Pick such a j; then since kip Kij for all p>j, we have k e Kij because Kij is closed. Finally, we need a lemma on Hausdorff distances. Lemma 4.6. Let H. be a decreasing sequence of nonempty closed subsets of X. Let H=. H.. Then d(Hi,H)+O. - Proof. We show sup {d(h,H)} - 0 as i-oo, from which the result follows. By h~H. Lemma 4.4, choose h. E H. such that sup d(h,H) = d(h.H). By 4.5 the sequence <h.> hEHi has a convergent subsequence hi jh E H. Now let C > 0. Choose i such that k d(hikh)<s. Then for any j>ik, sup d(h,H) < sup d(h,H) heHj hcHi = d(hik,H) < d(hik,h) < e. Definition 4.5. Let f:X+Y. The direct image function is the map f[ I:PX-+PY given by f[K] = {f(k) keK}. Theorem 4.2. Let f be a function from a compact metric space X into a metric space Y. The following are equivalent: (i) f is continuous; (ii) f[C Hi]=f f[Hi] for all decreasing sequences <H.> of closed nonempty subsets of X; and f[H] is closed for all closed H;

-13(iii) f[-] is continuous in the Hausdorff metric. Proof. We show (i)=->(iii)=>(ii)=> (i). (i)=>(iii). Let ~ > 0. We will find a 6 such that VH,H': d(H,H')<6 => d(f[H],f[H']) < ~. (i.e. f[ ] is uniformly continuous.) Since X is compact and (i) holds, we know f enjoys this property already. Choose 6 such that h,h' (d(hh')<6 => d(f(h),f(h')) < E) Suppose d(H,H')<. Then sup d(h,H')<d h~H -> V3sH d(h,-H')<5 -> WheH[ inf d(h,h') < 6] h' H' -> VheH 3h'eH'(d(h,h') < 6) (by 4.4) -> VheH3h'H' (d(f(h),f(h')) < C (by unif. cont.) -> VheH inf d(f(h),f(h')) < e h' e<H' sup d(f(h),f[H']) < e. heH Similarly sup. d(f(h'),f[H]) < e h' H' and (iii) follows. (iii) => (ii). Let <H.> be a decreasing sequence of closed subsets of X and let H= H. Then by 4.6 d(Hi,H)-+ as i-*. By (iii), d(f[Hi],f[H])0O. But f[Hil is again a decreasing sequence of closed sets, so d(f[Hi], f[Hi])*O by 4.6. This proves (ii) because limits are unique. (ii) => (i). Let d(t,t)+O; prove using (ii) that d(f(t ),f(t))-+. n n Define for k>O Sk={u | d(t,u)<-+}

-14Then S are a decreasing sequence and q Sk={t}. By (ii) we have k k k ft S] = f[{t}] = Q f[S]. Again by 4.6, since f[Sk] decrease, d(f[Sk], I f[Sk])-+. Let E > 0. Choose K such that d(f[Sk], Q f[Sk])< <. Now since t -*t, there is an N such that Vn > NK, t cSK and f(t )sF[SK]. n K -K n Thus for n>NK, d(f(t ),f(t)) = d(f(t ),f[{t}]) n n = d(f(t), Q f[Sk]) by (ii) i d(f[SK], i f[Sk]) < E. K k k This completes the proof of Theorem 4.2. (Note: (i) => (ii) is well-known; see [KI, p. 414.) In order to apply the results of Theorem 4.2 we present several tree operators. These can be used to define the semantics for appropriate combinations of processes, as in [BaZ]. We call on the lemmas of [BaZ], in fact, to establish that certain operators are metrically continuous. Theorem 4.2 then applies to show that the extended versions are sup-continuous. We give the versions for finite trees first. Definition 4.7.1 (alternative choice.) Let s and t be trees. Denote by s+t the result of joining s and t at the root. 4.7.2 A-Synchronized shuffle. Suppose A ~ Z. We want a tree operation which matches two trees (glues them together) at points A and otherwise interleaves events outside A. The appropriate definition is inductive.

-15Define NIL || s = sll NIL = s;'A A ('aisi I bjtj) = A a (s i tj) A a.=b.eA A 3 1 3 + I ai(Sillbjt.) + I h (aisi lt ). 4.7.3. Sequential Composition We would like to model two kinds of stopped processes: one which can continue (successful termination) and one which cannot (failed termination). In order to do this we introduce a new sort of nullary tree besides NIL, which wa call TND. Technically speaking, we should like W-equivalence to distinguish these two trees, and the HML formulas to distinguish them as well. We declare NIL and END to be W^-inequivalent, and we introduce elementary propositional variables FAILED and DONE into HML, with the definitions t 0 FAILED <=> t=NIL. t = DONE <=> t=END. Then one can check that the lemmas of Section II still hold. The base clause of Definition 4.7.2 should be amended to read END||s = sl JEND = s. Also in 4'7.1 we put NIL+END = END. We proceed with the definition of tou for finite t,u. NILot = NIL; ENDot = t; (saisi)ot = Eai(siot). 4.7.4. Renaming We wish to rename events so, for example, they are removed from a communication alphabet. This is done by considering a function h:S+-.

-16Define h(End) =End; h(Nil) =Nil; h (aiti )=Zh(ai)h(ti). Now we extend the above definitions to infinite trees. There is no problem with (1). For the others, we take Cauchy limits as in [BaZ]. 4.8.2 slt = lim s(k)I t(k) k-g A where s(k) is the k-section of s (Definition 2.9). 4.8.3 sot = lim sk) ot k-+~ (k) 4.8.4 h(t) = lim h(t(k)). We need to check that the above limits exist in the metric sense. Lemma 4.7. Let s,s',t,t' be finite trees and M = max(d(s,s'),d(t,t')). Then (1) d(s+t, s'+t') < M; (2) d(s lt, s' lt') <M, A A (3) d(sot, s'ot') < M; and (4) d(h(s), h(s')) < d(s,s'). Proof. deBakker and Zucker show (1) and (3). The also prove (2) when A=O. We include a proof for arbitrary A C Z. We assume all trees are non nullary, as these cases are all easy. Let e(s,s') = max{k | s Wk s'}. We will show (dropping the A subscript) eW(sI t,s'j It') >min(e (s,s'),ew(t,t')). w """- w w

-17Now let s = Ea.s. 1 1 s'= Ecisi. 1 1 t = Eb.t. 3 3 t'= Ed.t.'. Then s || t = u+u2+u3 where A 1 U= b a.i(si I tj) a.=b.eA 1 3 u2 = ai(s | t) aiAh u3 = I b.(s 1 t.) bjeh 3 Similar equations obtain for s,' [ t' = u'+u'+u'. Let e (s,s')=p and suppose (w.l.o.g.)p = min(e (s,s'),e (t,t')). We prove e (ui,u!) > p for i=1,2,3. Then by the result for +, w 1 - e (u 2+u3' U1+U2+3) > min{e (ui,u)} > PWe proceed inductively on the maximum height of the trees s,s',t,t' The height zero cases are straightfoward. aa. a. Estimating e (uu'): Let u1 ->s. t.. Then s ->si and t >t for some a.eA. Now p=e (s,s'). If p=O there is nothing to show. So we may a. assume (3i) s' >s' with e (s!,si) = p-l. 1 1 pw 1 a. Since a.eA, and e (t,t') > p, we know (3j) t' >t' with e (t.,t!) > p-l. I W- W _ j 3a. Now u' >s'i |I tj and by induction hypothesis, e (Si It t., s t.) > min(e (si 1 s!) e (t t)) > p-. w 1 w wj Similarly if a. Us -- S, | t' we deduce that there are s. and t. such that 1 3,a. and ew(sj |I t', s. II tj) > p-l. Therefore by definition of W, e (u1,u{) > p.

-18We need only consider e (u 2,u) as the proof for u3 u' is the same. a. ai a Let u2 - >si t, where ai.A. Then as before, s -— >s, and s'- >s for some i, where e (si's!) = p-1. W1 1 a. Now in this case u2 = Za.(sI | t'), and u' - s |s t'. Similarly if ~~~a. ~~ I2 1 ai u --- >si I t' we have u2 ->Si. t for some i. By I.H. e (si I t, s' I t') > p-. Therefore e (u,u') > p, as desired. The proof of (2) is now complete. We leave (4) as an easy exercise, and now the lemma is finished. Corollary. The sequences used in Definition 4.8 are convergent (to an equivalence class in the pseudo-metric). -Lemma 4.8. The inequalities of 4.7 hold for infinite trees. Proof. We show only (2) as the proof works the same way for the other cases. Consider first a special case: d (s,s')=O. Then we must show w d (s | t, s' | t') < d (t,t'). (Incidentally, this shows that W is a congruence with respect to II.) We know for each k: d(s(k) I t(k),s(k) I t' (k)) < d(t(k),t' (k)) (k) (k) (k)'t (k) because s ) W s' for each k. As k+- d t' ) d(t,t'), and the LHS + d(s I| t, s' |I t'). Therefore the inequality holds. We can now assume s -W s', and t -"W t'. Let e > 0. Choose k so large that k (k) (k^t * k) t d(sk s (k) d(ss dt) = d(s,s, ), t') = < c/2, and a(s |kl t', s'I| t') < E/2. Then by the triangle inequality d(s|l t, s' I t')< d(sl| t, s I tk) + d(s'k|I t'k, s' I t') + d(sk | tk, skll tk) < E/2 + e/2 + max d(s,s' ),d(t,t' )) = E + max(d(s,s'), d(t,t')) But ~ was arbitrary so the result holds.

-19Corollary. The operations of +, I|, o, and h are continuous (jointly). A Corollary. The same operations are sup-continuous on forests and Hausdorffcontinuous, when we pass to direct images. Unfortunately, the sequential composition operator is not quite the right one to lift to forests. That is, GOH = {tou I teG, ucH} requires that the same tree u be'grafted' wherever END occurs in t. We want a freer choice than this, which will allow substitution of any tree from H for END nodes in t. We give a special definition for the operator GoH. We start with Definition 4.9. Let G be a forest and t be a finite tree. The forest toG is given recursively: NILoG = {NIL}; ENDoG = G; (Za.t.)oG = {Ea.u. i u.st.oG}. 13. 1 1 1'3, Tt is easy to check that toG is closed for each t. Now let toG = lim t k)oG k~en for infinite t. Again we need to check that this limit exists. Lemma 4.9. For finite t,u: t Wk u => toG Wk uoG where Wk on the right is from Definition 4.3. Proof. We use induction on k. By Definition 4.3 we need to check that if t W u, a. a. w i>w.. By definition w. e t. oG where t = Ea.t.. Therefore t a>t. and since 1 1 1 11 1 a. t W+ u, we have u >u. for some u. W t.. If w = ia.w. let z = Ca.z. for each k+l 1 1. ik 11

-20such ai, where z. ~ u.oG. By IH, and the fact that u. Wk ti, we have Zi Wk w. 1 1 1 Then clearly z W w as desired. The reverse inclusion is similar. k+l Corollary. d(toG, uoG)<d(t,u) where the Hausdorff metric is used on the left, and t,u are finite. Proof. Apply Theorem 4.1 and the definitions at the beginning of this section. (k) Corollary. The limit t oG exists as k-+o. Definition 4.10. Let G,H ~ P (T ). HoG = lI toG teH Our objective is to prove that XGH(HoG) is sup-continuous in G and in H. This will be established via a series of independently interesting lemmas. We begin with Lemma 4.10. The map Xt.toG is metrically continuous in t. Proof. By the triangle inequality, for any k>0, (k) d(toG,uoG) < d(toG,t k)G) + d(t )oG,u kG) (k) + d(u oG,uoG) Let E > 0. Choose k large enough so that (1) d(toG,t() G) < ~/3 (2) d(t(k) oG,u(k)oG) < d(t(k),u (k) < d(t,u) + ~/3 (k) (3) d (u oG, uoG) < ~/3 Then d(toG,uoG) < d(t,u) + E => d(toG,uoG) < d(t,u). The result follows directly. Now we would like to establish Lemma 4.11. The map XG.toG is sup-continuous in G.

-21We begin with 4.11 for finite t. We must prove (*) to Gt = ( (toG.). 1 13. 1 This is clear if t = end or t = nil. Also, the left hand side is clearly included in the right. So let t = Za.t., and let w be any tree in the right hand set. Then w = Xa.w. where for each i, w. e t.oG., or w. s nt.oG.. By induction, w. e tjo CG.. Thus w e to(QG..: j i 3 3 3.3. We would like to extend (*) to every t. This can be done by direct calculation using the definitions, but the proof can also be given using the theorems and lemmas of previous sections. Lemma 4.12. For finite t, arbitrary closed G and n>O (toG)n) = (t (n)G)(n) Proof. This will be established by induction on n. First we give an inductive definition of the n-section of a finite tree t. Case (1) n=0, (end) =end; (nil) =nil; (Eaiti) =nil. Case (2) n>0. (end)n=end; (nil) =nil; (Eaiti)n=aiti nWhen n=0, the lemma is clear. Assume it for all values < n, and consider the case n. (endoG) n=Gn=(endn G)n (niloG) ={nil}=(nilnoG)n ((aiti.)oG) n={(Zaiu) | u et.oG} IX 1 1 n- n ={(a.tu. ) GG n- as desired.n ={7.a..t.n oGn by I.H.

-22Now to establish 4.12 for infinite t, we state a well-known property of metrically continuous functions. Lemma 4.13. Let f and g be continuous functions from a metric space X to a metric space Y. If f and g agree on a dense subset of X then f and g coincide. As a corollary, we get Lemma 4.14. The conclusion of 4.12 holds for infinite t. Proof. - The map t+toG is metrically continuous. (Lemma 4.10) The map (n) (n) (n) F+F, where F is a closed set and F( ={t teF} is also metrically (n) (n) continuous (proof: Xt.t is obviously m.c., so XF.F is both m.c. and (n) sup.c. by Theorem 4.2.). Composing these, we get a m.c. map t-(toG) (n) (n) Similarly t-(t oG) is m.c., and by 4.12 these maps agree on the dense subset of finite trees. Now we can prove the conclusion (*) of 4.11 for arbitrary t. Let G. be a decreasing sequence of nonempty closed sets. We claim for each i d(toG,to IGi) < d(toG.itoG.). We know that the sequence <toG.> is also closed and decreasing. By Lemma 4.6, d(toG.)+0 as i-*. But we also have, by the inequality above, d(toGi,to nGi)+0. Therefore, by uniqueness of limits, tonGi = q toGi. Proof of claim. For any k>0 d(toGi.tolGi.) < d((toGi) k (toGi) ) by properties of W-equivalence on forests. Let F.=toG.. F1 1 Then d(Fi.^ (to nGi) ) -d(Fk,(t tnGi) ) by 4.14 k kk =d(F., ( t oG.i) ) by 4.11 for finite trees =d(F.,C\ (tkoG)k) by sup-ctn. of XF.F(k) k) by 4.14. -d(F.,fl~(tOG.) ) by 4.14.

-23Now as k->+, F kF, and d is continuous, so for any E, we can choose a k such that k k d(CF,( toG) ) < d(Fi' toGi)+e. 1 1 111 1 Thus d(Fi,to f G.) < d(Fi, )toGi)+~ The inequality follows since ~ was arbitrary. Lemma 4.11 is thus proved for all cases. We are almost ready for Theorem 4.3. The map XGH.H~G is sup-continuous. Recall HoG = U toG. tsH Theorem 4.3 will be a consequence of Lemma 4.15. Let f be a metrically continuous function from the compact space X to P (Y) (with the Hausdorff metric). Define for closed H: f[H] = I f(x). xsH Then f: P (X)-+P (Y) is sup-continuous. Proof. We leave to the reader the proof that f[H] is closed. We then must show [fH]nH = f[H.] The inclusion of the left side in the right is obvious. Let y C [i f[Hi]. Then for each i, 3x.H. such that f(x.)=y. The x. have a convergent subsequence Xikfx, and x cs H. by Lemma 4.5. We want yEf(x). But d(f(xik), f(x))+0 as k-*g, and d(y,f(x)) < d(f(xik), f(x)) for each k. So d(y,f(x))=0. Thus y e f(x) since f(x) is closed. As a corollary: Theorem 4.3. XGH. HoG is sup-continuous in both arguments. The final and most trivial operation on closed sets is that of union: XFG. (FUG). Clearly this is a sup-continuous operation by the distributive law.

-24V. Applications and conclusions. The operators of Section IV can be used to give a denotational semantics to a CSP-like language, with two versions of nondeterminism. The operator 0 of Dijkstra will be interpreted as + on forests. When applied to singleton forests of the form a b and it produces a b This is exactly the guarded command construct from Dijkstra. On the other hand, the operator r will be interpreted as union of forests. When applied to the above two singletons, it produces which can be thought of as a'tree' t% In a sense, the n operator is introducing a hidden choice as in [HBR]. It should not beidentified with Milner's use of silent transitions, however. For /\ example in our semantics - Ja= a I a = Ia a ) A T \T ia a a t u t where t is the silent transition.

-25Consider the CSP-like language L: <S>:= <stmtvariable> |skipl failja-+SSl;S2 S1 S2 Sln s l |S h(S)IpxS <stmtvar>:= xxlyz... where in the construct a+S we let aeC range over atomic events, and in h(S) we specify a renaming h:Z+-. S stands for a statement expression with possible free occurrences of statement variables x,y,z... We interpret L in the space of maps [Env - P (T )], where Env = [Stmvar - P (T )] is the set of environments = assignments of'processes' to free statement variables. Let the variable p range over environments. We nave the semantic map Il::L- [Env+P (T)] C c M [x] p = p(x) for x a stmtvar M [skip]p = {end} — M fail]p = {nil} M a+S-]pP = (a-end)o[M [Sip]:~1 IS;s 21p M is 1P O M S 21 p M [S,;S2p = M [SlJp o M [S2]p j 1 2 M [sxl1S2P = M [S1Jp + M [S2]p M IS ls2]p = M [S1lp U M IS2]p M [1 1 S2]p = M [S1 | | M [S21p M [h(S)]p = h[M IS]p] M [BxS] = least fixpoint of ( where % is the map XK.M is.p (K/x) and p (K/x) is the same as p except x is assigned the forest K. Example: Consider ix (a+x 01 b-x)

-26This can be given by the familiar fixpoint formula n>O where L = TX, and I1) = 1 n+l() = ao.n(l) + bo<n(J) Pictorially 0 (1) = 1 2l(l) = a/ 2(I) = ia a b e 11 it etc. Thus the least fixpoint is the singleton set consisting of the full infinite binary tree over {a,b}. Example. Two more syntactic constructs can be introduced into L by definition. Let S be a statement expression not containing a free occurrence of the statement variable x. Then S def yx(s;x) S*def ix((s;x) n skip). In conclusion, we have shown how the information system approach leads to a natural cpo for the semantics of concurrency. This cpo is closely related to the metric spaces introduced in [BaZ], and even more closely to the structures explored in [BaBKM], where the cpo of closed languages (sets of strings) is used as a linear time semantic structure. The work of [BK] on projective limits gives another approach, although in this work no use is made of cpo methods.

-27It should be remarked that this theory is also connected closely to the work of Courcelle [C]. The contrast here is that we work with unordered trees and trees with infinite branching. However the metric space (Tz,d) can probably be obtained as a quotient of the free F-magma studied in [C]. Also in this paper compactness plays a key role for the definition of operators on our space. The space P (TZ) seems a natural candidate for further study; one interesting C problem is to relax the hypothesis of finite Z and still obtain sup-continuity properties. Acknowledgments Most of this work grew from discussions with W. Golson and S. Brookes. Thanks also to the members of the Theory Seminar at Ann Arbor: A. Blass, P. Hinman, and Y. Gurevich.

REFERENCES (BaBKM] DE BAKKER, J.W., J.A. BERGSTRA, J.W. KLOP, & J.-J.CH. MEYER, Linear time and branching time semantics for recursion with merge, Department of Computer Science Technical Report IW 211/82, Mathematisch Centrum, Amsterdam, 1982. [BaZ] DE BAKKER, J. W., & J.I. ZUCKER, Denotational semantics of concurrency, Proc. 14th ACM Symp. on Theory of Computing, pp. 153-158 [BK] BERGSTRA, J. A., & J.W. KLOP, Fixed point semantics in process algebras, Department of Computer Science Technical Report IW 206/82, Mathematisch Centrum, Amsterdam, 1982. [BR] BROOKES, S.D. & W.C. ROUNDS, Behavioral equivalence relations induced by programming logics, Proceedings 10th ICALP, 1983. (Also CMU Technical Report CS 83-112) [C] COURCELLE, B. Fundamental properties of infinite trees, TCS 25 (1983) 95-169. [GR] GOLSON, W., & W.C. ROUNDS, Connections between two theories of concurrency - metric spaces and synchronization trees, University of Michigan Computing Research Laboratory Technical Report, CRL TR 3-83 (To appear in Information and Control) [HBR] HOARE, C.A.R., S.D. BROOKES, & A.W. ROSCOE, A mathematical model for communicating processes, Oxford University, Programming Research Group Technical Report PRG-16 (1981). [HM] HENNESSY, M.C.B., & R. MILNER, On observing nondeterminism and concurrency, Proc. 7th ICALP, LNCS 85 (1980). [M] MILNER, R. A calculus of communicating systems, Springer LNCS Volume 92. [S] SCOTT, D. Domains for denotational semantics, Proc. 9th ICALP, 1982. [K] KURATOWSKI, K. Topology, Vol. 1 Academic Press, New York, 1966.