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.
While the intent in @cite_12 is to capture algorithms executing steps in isolation from the environment, a degree of is accommodated in the ASM literature since @cite_15 : (i) using the import command to create new elements, and (ii) marking certain functions as and allowing the environment to provide the values of external functions. One pretends that the interaction is inter-step. This requires the environment to anticipate some actions of the algorithm. Also, in @cite_15 , nesting of external functions was prohibited; the first study of ASMs with nested external functions was @cite_21 . The notion of determines whether interaction is allowed, see @cite_15 @cite_12 for precise definitions and discussion.
@cite_15 @cite_21 @cite_12
1969402593 1998333922
2 Static Algebras and Updates 4 2.1 Static Algebras: Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Vocabularies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Definition of Static Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.5 Locations and Updates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.6 Update Sets and Families of Update Sets . . . . . . . . . . . . . . . . . . . . . . . . 6 2.7 Conservative Determinism vs. Local Nondeterminism . . . . . . . . . . . . . . . . . . 7 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.