In earlier work, the Abstract State Machine Thesis -- that arbitrary algorithms are behaviorally equivalent to abstract state machines -- was established for several classes of algorithms, including ordinary, interactive, small-step algorithms. This was accomplished on the basis of axiomatizations of these classes of algorithms. Here we extend the axiomatization and, in a companion paper, the proof, to cover interactive small-step algorithms that are not necessarily ordinary. This means that the algorithms (1) can complete a step without necessarily waiting for replies to all queries from that step and (2) can use not only the environment's replies but also the order in which the replies were received.
Thus @cite_27 sets modeling interaction as its goal. Different forms of interaction, such as message-passing, database queries, remote procedure calls, inputs, outputs, signals, all reduce to a single universal form: a single-reply zero-or-more-arguments not-necessarily-blocking . All arguments and the reply (if any) should be elements of the state if they are to make sense to the algorithm. For a formal definition of queries see @cite_27 ; a reminder is given in the next section. For a detailed discussion and arguments for the universality of the query-reply approach see @cite_27 .
@cite_27
197061278
In earlier work, the Abstract State Machine Thesis — that arbitrary algorithms are behaviorally equivalent to abstract state machines — was established for several classes of algorithms, including ordinary, interactive, small-step algorithms. This was accomplished on the basis of axiomatizations of these classes of algorithms. Here we extend the axiomatization and the proof to cover interactive smallstep algorithms that are not necessarily ordinary. This means that the algorithms (1) can complete a step without necessarily waiting for replies to all queries from that step and (2) can use not only the environment’s replies but also the order in which the replies were received. In order to prove the thesis for algorithms of this generality, we extend the definition of abstract state machines to incorporate explicit attention to the relative timing of replies and to the possible absence of replies. ∗Partially supported by NSF grant DMS–0070723 and by a grant from Microsoft Research. Address: Mathematics Department, University of Michigan, Ann Arbor, MI 48109–1043, U.S.A., ablass@umich.edu. Much of this paper was written during a visit to Microsoft Research. †Microsoft Research, One Microsoft Way, Redmond, WA 98052, U.S.A. gurevich@microsoft.com ‡Microsoft Research; and University of Zagreb, FSB, I. Lucica 5, 10000 Zagreb, Croatia, dean@math.hr §Microsoft Research; current address: Computer Science Dept., M.I.T., Cambridge, MA 02139, U.S.A., brossman@mit.edu