The computable kernel of Abstract State Machines

AbstractAbstract State Machines (ASMs) were introduced as “a computation model that is more powerful and more universal than standard computation models”, by Yuri Gurevich in 1985. ASMs gained much attention as a specification method. It is extremely flexible because any mathematical structure may serve as a state. Gurevich characterized the expressive power of ASMs in terms of intuitively convincing postulates.The core result of this paper shows that the next-state function M of an Abstract State Machine M can be described on a symbolic level, notwithstanding the generality of the model: The successor state M(S) of a state S is fully specified by the equivalence ∼S induced by S on the terms over the signature of M. Consequently, M(S) is computable in case ∼S is decidable. Furthermore, this result implies a notion of computability for general structures, e.g. for algorithms operating on real numbers