Data machines and interfaces
FThAM Frank Pieper · TU/e Research Portal · 1989
A few days later, when Marc read the formalization I had made at that time, he advised that I should build in the possibility that the actions in a single "simulating sequence" depend on feedback provided by the information system.This was an enrichment that neither Jan nor I had thought of yet.Indeed, its effect was the conversion to what I considered to be the most general fonn of simulation between information systems.But it was harder to formalize, and even after it had been formalized, I still had my doubt~ about provability of the resulting relation's transitivity.So I tried to demonstrate this property: the subject of Chapter 6 was born.Jn August 1987, I had made considerable progress in both the research and the presentation of its results.But then a calamity occurred.Reflecting once more on the nature of this "most general" simulation mechanism, I found that it did not cover a particular case that, intuitively speaking, should have been covered.This case is described in Example 2 of Section 5.6.Technically speaking.it was because I had only introduced solid interfaces, cf.Section 8.2.The repair consisted of a few small changes in some basic definitions, but the consequences were huge: the largest and most complicated definitions and proofs had lost their validity and had to be rewritten.And so I did.The result is the thesis now in front of you.Eindhoven, spring 1989.Frank Pieper.extension in U), and pref U =pre U iff U contains only mples.If pre Ur;; U , which is equivalent to pro U -v := lwepost(u): u=v•w.For a postfix w of u, more than one prefix v of u may meet u =v•w in case u is infinite and from some index on periodic.That is why we define u-<w := lvepref{u}:u=v•w A Vxepref(u}:u =x•w ~ vr;;;,x; this is the shonest of these prefixes.of X;+i , then we write Lim X (read: the limit of X) for LJ rng X , which is the smallest sequence of which every X; is a prefix.This is a tuple if3Ne /P:Vn <:: N:Xn =XN, and a series otherwise. RELATIONS Any set of ordered pairs is a relation. The relation R is said to be a relation on A if A is the set domRurngR.The words reflexive, symmetric, anti-symmetric, and transitive have their usual meanings.The tenn quasi-order will be used to indicate a relation that is reflexive and transitive.An antisymmetric quasi-order is called an order relation, and an equivalence relation is a quasi-order that is symmetric.A Janice is an ordered pair (A; S) of a set A and an order relation s on A , such that any two elcc ments of A have a least upper bound and a greatest lower bound.