Abstract
We show that lambda calculus is a computation model which can step by step simulate any sequential deterministic algorithm for any computable function over integers or words or any datatype. More formally, given an algorithm above a family of computable functions (taken as primitive tools, i.e., kind of oracle functions for the algorithm), for every constant K big enough, each computation step of the algorithm can be simulated by exactly K successive reductions in a natural extension of lambda calculus with constants for functions in the above considered family.
The proof is based on a fixed point technique in lambda calculus and on Gurevich sequential Thesis which allows to identify sequential deterministic algorithms with Abstract State Machines.
This extends to algorithms for partial computable functions in such a way that finite computations ending with exceptions are associated to finite reductions leading to terms with a particular very simple feature.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Atrubin, A.J.: A One-Dimensional Real-Time Iterative Multiplier. Trans. on Electronic Computers EC 14(3), 394–399 (1965)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Barendregt, H.P.: The Lambda calculus. Its syntax and semantics. North-Holland, Amsterdam (1984)
Barendregt, H., Statman, R.: Böhm’s Theorem, Church’s Delta, Numeral Systems, and Ershov Morphisms. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 40–54. Springer, Heidelberg (2005)
Biedl, T., Buss, J.F., Demaine, E.D., Demaine, M.L., Hajiaghayi, M., Vinaĭ, T.: Palindrome recognition using a multidimensional tape. Theoretical Computer Science 302(1-3), 475–480 (2003)
Börger, E.: The Origins and the Development of the ASM Method for High Level System Design and Analysis. Journal of Universal Computer Science 8(1), 2–74 (2002)
Church, A., Rosser, J.B.: Some properties of conversion. Trans. Amer. Math. Soc. 39, 472–482 (1937)
Church, A.: The Calculi of Lambda Conversion. Princeton University Press, Princeton (1941)
Curry, H., Feys, R.: Combinatory logic, vol. I. North-Holland, Amsterdam (1958)
Dershowitz, N., Gurevich, Y.: A natural axiomatization of computability and proof of Church’s Thesis. Bulletin. of Symbolic Logic 14(3), 299–350 (2008)
Gurevich, Y.: Reconsidering Turing’s Thesis: towards more realistic semantics of programs. Technical Report CRL-TR-38-84, EEC Department. University of Michigan (1984)
Gurevich, Y.: A new Thesis. Abstracts, American Math. Soc., Providence (1985)
Gurevich, Y.: Evolving Algebras: An Introductory Tutorial. Bulletin of the European Association for Theoretical Computer Science 43, 264–284 (1991); Reprinted in Current Trends in Theoretical Computer Science, pp. 266–269. World Scientific, Singapore (1993)
Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)
Gurevich, Y.: May 1997 Draft of the ASM Guide. Tech. Report CSE-TR-336-97, EECS Dept., University of Michigan (1997)
Gurevich, Y.: The Sequential ASM Thesis. Bulletin of the European Association for Theoretical Computer Science 67, 93–124 (1999); Reprinted in Current Trends in Theoretical Computer Science, pp. 363–392. World Scientific, Singapore (2001)
Gurevich, Y.: Sequential Abstract State Machines capture Sequential Algorithms. ACM Transactions on Computational Logic 1(1), 77–111 (2000)
Hennie, F.C.: One-tape off-line Turing machine complexity. Information and Computation 8, 553–578 (1965)
Hankin, C.: Lambda calculi. In: A guide for computer scientists. Graduate Texts in Computer. Oxford University Press, Oxford (1994)
Kolmogorov, A.N.: On the definition of algorithm. Uspekhi Mat. Nauk. 13(4), 3–28 (1958); Translations Amer. Math. Soc. 29, 217–245 (1963)
Knuth, D.: The Art of Computer Programming, 3rd edn., vol. 2. Addison-Wesley, Reading (1998)
Krivine, J.L.: A call-by-name lambda-calculus machine. Higher Order and Symbolic Computation 20, 199–207 (2007)
Mogensen, T.: Efficient Self-Interpretation in Lambda Calculus. J. of Functional Programming 2(3), 345–363 (1992)
Paul, W.: Kolmogorov complexity and lower bounds. In: Budach, L. (ed.) Second Int. Conf. on Fundamentals of Computation Theory, pp. 325–334. Akademie, Berlin (1979)
Ronchi Della Rocca, S., Paolini, L.: The Parametric Lambda-calculus. In: A Metamodel for Computation. Springer, Heidelberg (2004)
Statman, R.: Church’s Lambda Delta Calculus. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 293–307. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ferbus-Zanda, M., Grigorieff, S. (2010). ASMs and Operational Algorithmic Completeness of Lambda Calculus. In: Blass, A., Dershowitz, N., Reisig, W. (eds) Fields of Logic and Computation. Lecture Notes in Computer Science, vol 6300. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15025-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-15025-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15024-1
Online ISBN: 978-3-642-15025-8
eBook Packages: Computer ScienceComputer Science (R0)