CONCUR 2004 – Concurrency Theory- P6: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | 136 M. Bojanczyk and I. Walukiewicz Given two types a and ft we denote by dtype a fi the delayed type which assigns to a letter a the type a a ft. A type a is reachable from a type 3 denoted 3 a if G ft a holds for some context CQ. This relation is a quasiorder and weuse for the accompanying equivalence relation. The following simple lemma is given without a proof Lemma 2. Ift is a subtree oft then sig t s C sig t s . If a 3 then dtype a fi dtype fi fi . The following lemma shows that for TL EF -definable languages the relation is a congruence with respect to the function dtype a fi -. Lemma 3. If ft and ax fix then dtype ao ax dtype fi0 fix . Proof. Since a TL EF -definable language satisfies dtype a fi dtype fi a it is sufficient to prove the case where ft ai. Let C be a context such that C a0 fio and let D be a context such that jO 3o a0- All these contexts exist by assumption. Let s0 be a tree of type ao and let be a tree of type ai. Consider the two sequences of trees i o and defined by induction as follows so so Itx Cfsi for i 0 Si for i 1. By a simple induction one can prove that for all i 0 type si aa and typeltf By Lemma 2 for all i 0 sigts Si C sig ti si C si5 si i si . Since there are only finitely many signatures there must be some i 0 such that sigfs sx sig ti sx - Consequently by Lemma 1 the delayed types dtype ao ax and dtype fio ax are equal. We are now ready to show that the language L is typeset dependent. Let s and t be two trees with the same typeset. If this typeset is empty then both trees have one node and consequently the same delayed type. Otherwise one can consider the following four types which describe the sons of s and t ao type s 0 aj type s x fio type t Q fix type t x . We need to prove that dtype fio fii dtype ao of . By assumption that the typesets of s and t are equal both fi0 and fix occur in nonroot nodes of s and both ao and ax occur in nonroot nodes of t. Thus fio a holds for some a e a0 aj and similarly for fix a0 and ax- The
