Algorithmic Completeness of Imperative Programming Languages

• Autorzy: Marquer Yoann

Identyfikatory

DOI

10.3233/FI-2019-1824

• Języki publikacji: EN

Abstrakty

EN

According to the Church-Turing Thesis, effectively calculable functions are functions computable by a Turing machine. Models that compute these functions are called Turing-complete. For example, we know that common imperative languages (such as C, Ada or Python) are Turing complete (up to unbounded memory). Algorithmic completeness is a stronger notion than Turing-completeness. It focuses not only on the input-output behavior of the computation but more importantly on the step-by-step behavior. Moreover, the issue is not limited to partial recursive functions, it applies to any set of functions. A model could compute all the desired functions, but some algorithms (ways to compute these functions) could be missing (see [10, 27] for examples related to primitive recursive algorithms). This paper’s purpose is to prove that common imperative languages are not only Turing-complete but also algorithmically complete, by using the axiomatic definition of the Gurevich’s Thesis and a fair bisimulation between the Abstract State Machines of Gurevich (defined in [16]) and a version of Jones’ While programs. No special knowledge is assumed, because all relevant material will be explained from scratch.

Słowa kluczowe

EN

algorithm; ASM; completeness; computability; imperative; simulation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 168, nr 1
• Strony: 51--77
• Opis fizyczny: Bibliogr. 31 poz., rys.

Twórcy

autor

Marquer Yoann

• Université Paris-Est Créteil (UPEC), Laboratoire d’Algorithmique, Complexité et Logique (LACL), IUT Sénart-Fontainebleau, France

Bibliografia

• [1] Andary P, Patrou B, Valarcher P.: A theorem of representation for primitive recursive algorithms, Fundamenta Informaticae XX. 2010 pp. 1-18.
• [2] Arsac J.: Algorithmique et langages de programmation, Bulletin de l’EPI. 1991; 64:115-124.
• [3] Biedl T, Buss JF, Demaine ED, Demaine ML, Hajiaghayi M, Vinar T.: Palindrome recognition using a multidimensional tape, Theoretical Computer Science. 2003; 302(1-3):475-480. URL https://doi.org/10.1016/S0304-3975(03)00086-0.
• [4] Blass A, Gurevich Y. : Algorithms vs. Machines, Bulletin of the European Association for Theoretical Computer Science Number. 2002; 77:96-118.
• [5] Blass A, Gurevich Y. : Abstract state machines capture parallel algorithms, ACM transactions on Computational Logic. 2008; 9(3):19:1-19:32. doi:10.1145/1352582.1352587.
• [6] Blass A, Dershowitz N, and Gurevich Y. : When are two algorithms the same?, Bull. Symbolic Logic. 2009; 15(2):145-168. URL https://www.jstor.org/stable/25478250.
• [7] Blum M. : A Machine-Independent Theory of the Complexity of Recursive Functions, Journal of the ACM. 1967; 14(2):322-336. doi:10.1145/321386.321395.
• [8] Börger E. : Abstract State Machines: A Unifying View of Models of Computation and of System Design Frameworks, Annals of Pure and Applied Logic. 2005; 133(1-3):149-171. URL https://doi.org/10.1016/j.apal.2004.10.007.
• [9] Cégielski P, Guessarian I. : Normalization of Some Extended Abstract State Machines, Fields of Logic and Computation, Lecture Notes in Computer Science. 2010; 6300:165-180. doi:10.1007/978-3-642-15025-8_9.
• [10] Colson L. : About primitive recursive algorithms, Theoretical Computer Science. 1991; 83(1):57-69. URL https://doi.org/10.1016/0304-3975(91)90039-5.
• [11] Cori R, Lascar D, and Pelletier D. : Mathematical Logic: A Course With Exercises : Part I and II, Paris, Oxford University Press (2000, 2001). ISBN-10:0198500483, 13:978-0198500483. doi:10.2307/3621399.
• [12] Ferbus-Zanda M, Grigorieff S. : ASM and Operational Algorithmic Completeness of Lambda Calculus, Fields of Logic and Computation. 2010. doi: 10.1007/978-3-642-15025-8_16.
• [13] Glaesser U, Gurevich Y, Veanes M. : Universal Plug and Play Machine Models, Proc. of IFIP World Computer Congress, Stream 7 on Distributed and Parallel Embedded Systems. 2002 pp. 21-30. doi:10.1007/978-0-387-35599-3_3.
• [14] Grigorieff S, Valarcher P. : Evolving Multialgebras unify all usual models for computation in sequential time, Symposium on Theoretical Aspects of Computer Science. 2010. doi:10.4230/LIPIcs.STACS.2010.2473.
• [15] Grigorieff S, Valarcher S. : Classes of Algorithms: Formalization and Comparison, Bulletin of the EATCS. 2012; 107:95-127.
• [16] Gurevich Y. : Sequential Abstract State Machines Capture Sequential Algorithms, ACM Transactions on Computational Logic. 2000; 1(1):77-111. doi:10.1145/343369.343384.
• [17] Gurevich Y. : Interactive Algorithms, Mathematical Foundations of Computer Science. 2005 pp. 26-38. doi:10.1007/11549345_3.
• [18] Huggins JK, and Shen W. : The Static and Dynamic Semantics of C, Technical Report. 2000.
• [19] Jones ND. : LOGSPACE and PTIME characterized by programming languages, Theoretical Computer Science. 1999; 228(1-2):151-174. doi:10.1016/S0304-3975(98)00357-0.
• [20] Kleene SC. : Recursive predicates and quantifiers, Transactions of the AMS. 1943;53(1):41-73. URL https://doi.org/10.2307/2267986.
• [21] Krivine J-L. : A call-by-name lambda-calculus machine, Higher Order and Symbolic Computation. 2007; 20(3):199-207. doi:10.1007/s10990-007-9018-9.
• [22] Marquer Y. : Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif ou polynomial, dr-apeiron.net/doku.php/en:research:thesis-defense (thesis defended in 2015). URL https://tel.archives-ouvertes.fr/tel-01280467.
• [23] Marquer Y. : Algorithmic Completeness of Imperative Programming Languages (Long Version), dr-apeiron.net/doku.php/en:research:fi-while (2016, technical report).
• [24] Marquer Y. : An Imperative Language Complete for PTime Algorithms, dr-apeiron.net/ doku.php/en:research:ploopc (2016, in review).
• [25] Meyer A, Ritchie D. : The complexity of loop programs, ACM 22nd national conference. 1967 pp. 465-469. doi:10.1145/800196.806014.
• [26] Moschovakis YN. : What is an algorithm?, Mathematics Unlimited. 2001 pp. 919-936. doi:10.1007/978-3-642-56478-9_46.
• [27] Moschovakis YN. : On Primitive Recursive Algorithms and the Greatest Common Divisor Function, Theoretical Computer Science. 2003; 301(1-3):1-30. URL https://doi.org/10.1016/S0304-3975(02)00487-5.
• [28] Soare RI. : Computability and Recursion, Bulletin of Symbolic Logic. 1996; 2(3):284-321. doi:10.2307/420992.
• [29] Turing AM. : On Computable Numbers, with an Application to the Entscheidungsproblem, Proc. London Math. Soc. 1937; 42(2):230-265. URL https://doi.org/10.1112/plms/s2-42.1.230.
• [30] Yanofsky NS. : Towards a Definition of an Algorithm, Journal of Logic and Computation. 2010; 21(2): 253-286. URL https://doi.org/10.1093/logcom/exq016.
• [31] Yanofsky NS. : Galois Theory of Algorithms, Kolchin Seminar in Differential Algebra. 2010. arXiv:1011.0014.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).