Exact Exploration
Andreas Blass, Nachum Dershowitz, Yuri Gurevich

TL;DR
This paper refines the abstract state machine framework to precisely model the intra-step behavior of classical algorithms, including those with partial functions and partial equality, enhancing the theoretical understanding of algorithm execution.
Contribution
It introduces a refined abstract state machine model that captures exact intra-step behavior and state tests, extending the axiomatization of classical algorithms.
Findings
Exact state transition emulation by abstract state machines
Inclusion of algorithms with partial functions and equality
Enhanced framework for modeling intra-step behavior
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Logic, programming, and type systems · Logic, Reasoning, and Knowledge
