Background, Reserve, and Gandy Machines
Proceedings of CSL 2000, Springer Lecture Notes in Computer Science |
Algorithms often need to increase their working space, and it may be convenient to pretend that the additional space was really there all along but was not previously used. In particular, abstract state machines have, by definition [Evolving Algebra 1993: Lipari Guide], an infinite reserve. Although the reserve is a naked set, it is often desirable to have some external structure over it. For example, in [Choiceless Polynominal Time] every state was required to include all finite sets of its atoms, all finite sets of these, etc. In this connection, we define the notion of a background class of structures. Such a specifies the constructions (like finite sets or lists) available as “background” for algorithms.
The importation of reserve elements must be non-deterministic, since an algorithm has no way to distinguish one reserve element from another. But this sort of non-determinism is much more benign than general non-determinism. We capture this intuition with the notion of inessential non-determinism. Alternatively, one could insist on specifying a particular one of the available reserve elements to be imported. This is the approach used in [Robin Gandy, “Church’s thesis and principles for mechanisms” in: “The Kleene Symposium” (Ed. Jon Barwise et al.), North-Holland, 1980, 123-148.]. The price of this insistence is that the specification cannot be algorithmic. We show how to turn a Gandy-style deterministic, non-algorithmic process into a non-deterministic algorithm of the sort described above, and we prove that Gandy’s notion of “structural” for his processes corresponds to our notion of “inessential non-determinism.”