Abstract
Recent analysis of sequential algorithms resulted in their axiomatization and in a representation theorem stating that, for any sequential algorithm, there is an abstract state machine (ASM) with the same states, initial states and state transitions. That analysis, however, abstracted from details of intra-step computation, and the ASM, produced in the proof of the representation theorem, may and often does explore parts of the state unexplored by the algorithm. We refine the analysis, the axiomatization and the representation theorem. Emulating a step of the given algorithm, the ASM, produced in the proof of the new representation theorem, explores exactly the part of the state explored by the algorithm. That frugality pays off when state exploration is costly. The algorithm may be a high-level specification, and a simple function call on the abstraction level of the algorithm may hide expensive interaction with the environment. Furthermore, the original analysis presumed that state functions are total. Now we allow state functions, including equality, to be partial so that a function call may cause the algorithm as well as the ASM to hang. Since the emulating ASM does not make any superfluous function calls, it hangs only if the algorithm does.
Blass was partially supported by NSF grant DMS-0653696. Dershowitz was partially supported by Israel Science Foundation grant 250/05. Part of the work reported here was performed during visits of the first two authors to Microsoft.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
ASM Michigan Webpage, http://www.eecs.umich.edu/gasm/ , maintained by J. K. Huggins (Viewed June 4, 2010)
Bernot, G., Bidoit, M., Choppy, C.: Abstract data types with exception handling. Theoret. Comp. Sci. 46, 13–45 (1986)
Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)
Blum, L., Shub, M., Smale, S.: On a theory of computation and complexity over the real numbers. Bulletin of Amer. Math. Soc. (NS) 21, 1–46 (1989)
Blass, A., Gurevich, Y.: Algorithms vs. Machines. Bull. European Assoc. Theoret. Comp. Sci. 77, 96–118 (2002); Reprinted in Paun, G., et al. (eds.): Current Trends in Theoretical Computer Science: The Challenge of the New Century, vol. 2, pp. 215–236. World Scientific, Singapore (2004)
Blass, A., Gurevich, Y.: Algorithms: A Quest for Absolute Definitions. Bull. Euro. Assoc. for Theor. Computer Sci. 81, 195–225 (2003); Reprinted in Paun, G., et al. (eds.): Current Trends in Theoretical Computer Science, 283–311, World Scientific, Singapore (2004); Olszewski, A., et al. (eds.) Church’s Thesis After 70 Years, 24–57, Ontos (2006)
Börger, E., Stärk, R.: Abstract State Machines. Springer, Heidelberg (2003)
Boker, U., Dershowitz, N.: The Church-Turing Thesis over arbitrary domains. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 199–229. Springer, Heidelberg (2008)
Dershowitz, N., Gurevich, Y.: A natural axiomatization of computability and proof of Church’s Thesis. Bulletin of Symbolic Logic 14, 299–350 (2008)
xrc (exact reals in C), http://keithbriggs.info/xrc.html (viewed on June 4, 2010)
Gowland, P., Lester, D.: A survey of exact arithmetic implementations. In: Blanck, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 30–47. Springer, Heidelberg (2001)
Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)
Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic 1, 77–111 (2000)
Kolmogorov, A.N.: On the concept of algorithm. Uspekhi Matematicheskikh Nauk 8(4), 175–176 (1953) (in Russian); English version in [27, 18–19]
Korovina, M.: Gandy’s theorem for abstract structures without the equality test. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 290–301. Springer, Heidelberg (2003)
Kushner, B.A.: Lectures on Constructive Mathematical Analysis. Translations of Mathematical Monographs, vol. 60. American Mathematical Society, Providence (1984); The Russian original published by Nauka (1973)
Lambov, B.: The RealLib Project, http://www.brics.dk/~barnie/RealLib/ (viewed on June 4, 2010)
Markov, A.A.: The Theory of Algorithms. American Mathematical Society Translations, series 15(2), 1–14 (1960)
Meseguer, J., Roşu, G.: A total approach to partial algebraic specification. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 572–584. Springer, Heidelberg (2002)
Moschovakis, Y.: On founding the theory of algorithms. In: Dales, H.G., Olivieri, G. (eds.) Truth in Mathematics, pp. 71–104. Clarendon Press, Oxford (1998)
Moschovakis, Y.: What is an algorithm? In: Engquist, B., Schmid, W. (eds.) Mathematics Unlimited — 2001 and Beyond, pp. 919–936. Springer, Heidelberg (2001)
Müller, N.: iRRAM - Exact Arithmetic in C++, http://www.informatik.uni-trier.de/iRRAM/ (viewed on June 4, 2010)
Naughton, T.J.: Continuous-space model of computation is Turing universal. Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series, vol. 4109, pp. 121–128 (2000)
Nowack, A.: Complexity theory via abstract state machines. Master’s thesis, RWTH-Aachen (2000)
Spec. Explorer, http://msdn.microsoft.com/en-us/devlabs/ee692301.aspx (viewed on June 04, 2010)
Computable Real Numbers, http://www.haible.de/bruno/MichaelStoll/reals.html (viewed on June 4, 2010)
Uspensky, V.A., Semenov, A.L.: Algorithms: Main Ideas and Applications. Kluwer, Dordrecht (1993)
Weihrauch, K.: Computable Analysis — An introduction. Springer, Heidelberg (2000)
Winskel, G.: Event Structures — Lecture Notes for the Advanced Course on Petri Nets. Univ. of Cambridge Computer Lab. Tech. Report 95, UCAM-CL-TR-95 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blass, A., Dershowitz, N., Gurevich, Y. (2010). Exact Exploration and Hanging Algorithms. In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-15205-4_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15204-7
Online ISBN: 978-3-642-15205-4
eBook Packages: Computer ScienceComputer Science (R0)