Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exact Exploration

Andreas Blass, Nachum Dershowitz, Yuri Gurevich

TL;DR

The paper strengthens the Abstract State Machine (ASM) framework by refining the axioms to account for exact intra-step exploration, enabling ASMs to emulate not only state transitions but also the precise tests performed to determine the next move. It introduces the exact exploration postulate, with state-dependent explore sets Γ(X) and a discrimination order, and extends the ASM theorem to guarantee clash-free emulations that explore only the locations actually used by the original algorithm. By handling partial equality and partial operations, and by incorporating case statements and richer intra-step queries, the work broadens ASM universality to algorithms operating over partial algebras and computable reals, thereby reinforcing the Church-Turing thesis from first principles. The findings have significant implications for modeling computation with partial information, and for achieving faithful, parsimonious representations of sequential algorithms across diverse data representations. Overall, the results establish ASMs as a precise, universal, and robust model for sequential computation with refined control over exploration and partiality.

Abstract

Recent analysis of classical algorithms resulted in their axiomatization as transition systems satisfying some simple postulates, and in the formulation of the Abstract State Machine Theorem, which assures us that any classical algorithm can be emulated step-by-step by a most general model of computation, called an ``abstract state machine''. We refine that analysis to take details of intra-step behavior into account, and show that there is in fact an abstract state machine that not only has the same state transitions as does a given algorithm but also performs the exact same tests on states when determining how to proceed to the next state. This enhancement allows the inclusion -- within the abstract-state-machine framework -- of algorithms whose states only have partially-defined equality, or employ other native partial functions, as is the case, for instance, with inversion of a matrix of computable reals.

Exact Exploration

TL;DR

The paper strengthens the Abstract State Machine (ASM) framework by refining the axioms to account for exact intra-step exploration, enabling ASMs to emulate not only state transitions but also the precise tests performed to determine the next move. It introduces the exact exploration postulate, with state-dependent explore sets Γ(X) and a discrimination order, and extends the ASM theorem to guarantee clash-free emulations that explore only the locations actually used by the original algorithm. By handling partial equality and partial operations, and by incorporating case statements and richer intra-step queries, the work broadens ASM universality to algorithms operating over partial algebras and computable reals, thereby reinforcing the Church-Turing thesis from first principles. The findings have significant implications for modeling computation with partial information, and for achieving faithful, parsimonious representations of sequential algorithms across diverse data representations. Overall, the results establish ASMs as a precise, universal, and robust model for sequential computation with refined control over exploration and partiality.

Abstract

Recent analysis of classical algorithms resulted in their axiomatization as transition systems satisfying some simple postulates, and in the formulation of the Abstract State Machine Theorem, which assures us that any classical algorithm can be emulated step-by-step by a most general model of computation, called an ``abstract state machine''. We refine that analysis to take details of intra-step behavior into account, and show that there is in fact an abstract state machine that not only has the same state transitions as does a given algorithm but also performs the exact same tests on states when determining how to proceed to the next state. This enhancement allows the inclusion -- within the abstract-state-machine framework -- of algorithms whose states only have partially-defined equality, or employ other native partial functions, as is the case, for instance, with inversion of a matrix of computable reals.

Paper Structure

This paper contains 36 sections, 11 theorems, 26 equations, 2 figures, 2 tables.

Table of Contents

  1. Keywords:
  2. Introduction
  3. Significance
  4. Universality.
  5. Fidelity.
  6. Parsimony.
  7. Background
  8. Axiomatization of Algorithms
  9. Sequential Time
  10. Abstract State
  11. Bounded Exploration
  12. Classical Algorithms
  13. Abstract State Machines
  14. ASM Programs
  15. Update Sets of ASMs
  16. ...and 21 more sections

Key Result

Theorem 6

Every classical algorithm, satisfying Postulates P1--BE, has an equivalent ASM, with the exact same states and state-transition function.

Figures (2)

  • Figure 1: An abstract-state-machine program for sorting.
  • Figure 2: Exploration tree.

Theorems & Definitions (34)

  • Definition 1: Classical Algorithm
  • Definition 2: ASM
  • Example 3
  • Example 4
  • Example 5
  • Theorem 6: ASM Theorem Gurevich00
  • Example 7
  • Example 8
  • Example 9
  • Example 10
  • ...and 24 more