Interactive Small-Step Algorithms I: Axiomatization

  • Andreas Blass ,
  • Yuri Gurevich ,
  • Dean Rosenzweig ,
  • Benjamin Rossman

MSR-TR-2006-170 |

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.