Finite Work

In the appendix of "Sequential Abstract State Machines Capture Sequential Algorithms" (A.C.M. Trans. Computational Logic 1 (2000), 77-111), Gurevich defines the notion of finite exploration for small-step algorithms which do not intrastep interact with the environment. Although satisfying finite exploration is a seemingly weaker property than satisfying bounded exploration, he proves the two notions are equivalent for this class of algorithms. We investigate what happens in the case of ordinary small-step algorithms – in particular, these algorithms do intrastep interact with the environment – as described by Blass and Gurevich in "Ordinary Interactive Small-Step Algorithms, I" (to appear in ACM Trans. Computational Logic). Our conclusion is that every algorithm satisfying the appropriate version of finite exploration is equivalent to an algorithm satisfying bounded exploration. We provide a counterexample to the stronger statement that every algorithm satisfying finite exploration satisfies bounded exploration. This statement becomes true if the definition of bounded exploration is modified slightly. The proposed modification is natural for algorithms operating in isolation, but not for algorithms belonging to a larger systems of computation. We believe the results generalize to general interactive small-step algorithms.

PDF file


InstitutionMicrosoft Research
> Publications > Finite Work