Ordinary Interactive Small-Step Algorithms, II

This is the second in a series of papers extending the proof of the Abstract State Machine Thesis — that arbitrary algorithms are behaviorally equivalent to abstract state machines — to algorithms that can interact with their environments during a step rather than only between steps. As in the first paper of the series, we are concerned here with ordinary, small-step, interactive algorithms. This means that the algorithms (1) proceed in discrete, global steps, (2) perform only a bounded amount of work in each step, (3) use only such information from the environment as can be regarded as answers to queries, and (4) never complete a step until all queries from that step have been answered. After reviewing the previous paper’s formal description of such algorithms and the definition of behavioral equivalence, we define ordinary, interactive small-step, abstract state machines (ASM’s). Except for very minor modifications, these are the machines commonly used in the ASM literature. We define their semantics in the framework of ordinary algorithms, and we show that they satisfy the postulates for these algorithms. Our main theorem is that all ordinary algorithms, as defined by the postulates, are equivalent to ASMs. We also discuss some possible variations of and additions to the ASM semantics.