Interactive Small-Step Algorithms I: Axiomatization

TL;DR

This paper extends the axiomatization of interactive small-step algorithms, allowing for non-ordinary behaviors such as partial steps and order-dependent responses, thereby broadening the theoretical understanding of these algorithms.

Contribution

It generalizes the axiomatization of interactive small-step algorithms to include non-ordinary behaviors, enhancing the theoretical framework of abstract state machines.

Findings

Extended axiomatization to non-ordinary algorithms

Captured partial step completion without waiting for all replies

Included order of reply reception in the model

Abstract

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.