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.
Paper @cite_12 was the first of a series of papers offering for the thesis, for particular classes of algorithms. They all follow the same general pattern; Describe axiomatically a class A of algorithms. Define behavioral equivalence of A algorithms. Define a class M of abstract state machines. Prove the following characterization theorem for A : @math , and every @math is behaviorally equivalent to some @math . The characterization provides a theoretical programming language for A and opens the way for more practical languages for A . The justification of the ASM Thesis thus obtained is speculative in two ways: The claim that A captures the intuitive class of intended algorithms is open to criticism. Definition of behavioral equivalence is open to criticism. But the characterization of A by M is precise, and in this sense the procedure the ASM thesis for the class of algorithms A modulo the chosen behavioral equivalence.
@cite_12
1998333922
We examine sequential algorithms and formulate a sequential-time postulate, an abstract-state postulate, and a bounded-exploration postulate . Analysis of the postulates leads us to the notion of sequential abstract-state machine and to the theorem in the title. First we treat sequential algorithms that are deterministic and noninteractive. Then we consider sequential algorithms that may be nondeterministic and that may interact with their environments.