A Behavioural Theory of Recursive Algorithms

• Autorzy: Börger Egon , Schewe Klaus-Dieter

Identyfikatory

DOI

10.3233/FI-2020-1978

• Języki publikacji: EN

Abstrakty

EN

“What is an algorithm?” is a fundamental question of computer science. Gurevich’s behavioural theory of sequential algorithms (aka the sequential ASM thesis) gives a partial answer by defining (non-deterministic) sequential algorithms axiomatically, without referring to a particular machine model or programming language, and showing that they are captured by (non-deterministic) sequential Abstract State Machines (nd-seq ASMs). However, recursive algorithms such as mergesort are not covered by this theory, as has been pointed out by Moschovakis, who had independently developed a different framework to mathematically characterize the concept of (in particular recursive) algorithm. In this article we propose an axiomatic definition of the notion of sequential recursive algorithm which extends Gurevich’s axioms for sequential algorithms by a Recursion Postulate and allows us to prove that sequential recursive algorithms are captured by recursive Abstract State Machines, an extension of nd-seq ASMs by a CALL rule. Applying this recursive ASM thesis yields a characterization of sequential recursive algorithms as finitely composed concurrent algorithms all of whose concurrent runs are partial-order runs.

Słowa kluczowe

EN

recursive algorithm; behavioural theory; abstract state machine; concurrent algorithm; partial-order run

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 177, nr 1
• Strony: 1--37
• Opis fizyczny: Bibliogr. 37 poz.

Twórcy

autor

Börger Egon

• Dipartimento di Informatica, Università di Pisa, Pisa, Italy

autor

Schewe Klaus-Dieter

• UIUC Institute, Zhejiang University, Haining, China

Bibliografia

• [1] Börger E. Computability, Complexity, Logic, volume 128 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1989. ISBN-10:0444874062, 13:978-0444874061.
• [2] Gurevich Y. A New Thesis. Abstracts, American Mathematical Society, 1985. 6(4):317.
• [3] Gurevich Y. Sequential abstract-state machines capture sequential algorithms. ACM Trans. Comp. Logic, 2000. 1(1):77-111. doi:10.1145/343369.343384.
• [4] Börger E, Stärk RF. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, 2003. doi:10.1007/978-3-642-18216-7.
• [5] Abrial JR. Modeling in Event-B - System and Software Engineering. Cambridge University Press, 2010. ISBN-10:0521895561, 13:978-0521895569.
• [6] Abrial JR. The B-book - Assigning programs to meanings. Cambridge University Press, 1996. ISBN-0521496195, 9780521496193.
• [7] Moschovakis YN. Abstract recursion as a foundation of the theory of algorithms. In: Börger E, Oberschelp W, Richter M, Schinzel B, W Thomas (eds.), Computation and Proof Theory, volume 1104 of Lecture Notes in Mathematics, p. 289364. Springer, 1984. ISBN-978-3-540-13901-0.
• [8] Moschovakis YN. On founding the theory of algorithms. In: Dales HG, Oliveri G (eds.), Truth in mathematics, pp. 71-104. Clarendon Press, 1998.
• [9] Moschovakis YN. Abstract Recursion and Intrinsic Complexity. Cambridge University Press, 2019. Lecture Notes in Logic. ISBN-10:110841558X, 13:978-1108415583.
• [10] Moschovakis YN. What is a Algorithm? In: Engquist B, Schmid W (eds.), Mathematics Unlimited - 2001 and Beyond, pp. 919-936. Springer, 2001. ISBN-978-3-642-56478-9.
• [11] Blass A, Gurevich Y. Algorithms vs. Machines. Bulletin of the EATCS, 2002. 77:96-119. doi:10.1142/9789812562494_0048.
• [12] Gurevich Y. Evolving algebras 1993: Lipari Guide. In: E Börger (ed.), Specification and Validation Methods, pp. 9-36. Oxford University Press, 1995.
• [13] Gurevich Y, Spielmann M. Recursive Abstract State Machines. J. UCS, 1997. 3(4):233-246. doi:10.3217/jucs-003-04-0233.
• [14] Börger E, Bolognesi T. Remarks on Turbo ASMs for Functional Equations and Recursion Schemes. In: Börger E, et al. (eds.), Abstract State Machines, Advances in Theory and Practice, 10th International Workshop (ASM 2003), volume 2589 of Lecture Notes in Computer Science. Springer, 2003 pp. 218-228. doi:10.1007/3-540-36498-6_12.
• [15] Vardi MY. What is an algorithm? Commun. ACM, 2012. 55(3):5. doi:10.1145/2093548.2093549.
• [16] Börger E, Schewe KD. Concurrent Abstract State Machines. Acta Informatica, 2016. 53(5):469-492. doi:10.1007/s00236-015-0249-7.
• [17] Lamport L. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers, 1979. 28(9):690-691. doi:10.1109/TC.1979.1675439.
• [18] Börger E, Schewe KD. A Characterization of Distributed ASMs with Partial-order Runs. In: Raschke A, Mery D, Houdek F (eds.), Rigorous State-Based Methods (Proc. ABZ 2020), volume 12071 of LNCS. Springer, 2020 pp. 79-92. doi:10.1007/978-3-030-48077-6_6.
• [19] Mayr R. Process Rewrite Systems. Information and Computation, 1999. 156:264-286. doi:10.1006/inco.1999.2826.
• [20] Börger E, Raschke A. Modeling Companion for Software Practitioners. Springer, 2018. doi:10.1007/978-3-662-56641-1.
• [21] Ferrarotti F, Schewe KD, Tec L, Wang Q. A New Thesis Concerning Synchronised Parallel Computing - Simplified Parallel ASM Thesis. Theor. Comp. Sci., 2016. 649: 25-53. doi: 10.1016/j.tcs.2016.08.013.
• [22] Börger E, Schewe KD. Communication in Abstract State Machines. J. Univ. Comp. Sci., 2017. 23(2):129-145. doi:10.3217/jucs-023-02-0129.
• [23] Blass A, Gurevich Y. Abstract State Machines Capture Parallel Algorithms. ACM Trans. Computational Logic, 2003. 4(4):578-651. doi:10.1145/937555.937561.
• [24] Blass A, Gurevich Y. Abstract State Machines Capture Parallel Algorithms: Correction and Extension. ACM Trans. Comp. Logic, 2008. 9(3). doi:10.1145/1352582.1352587.
• [25] Schewe KD, Wang Q. A Customised ASM Thesis for Database Transformations. Acta Cybernetica, 2010. 19(4):765-805.
• [26] Schewe KD, Wang Q. A Simplified Parallel ASM Thesis. In: Derrick J, et al. (eds.), Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), volume 7316 of LNCS. Springer, 2012 pp. 341-344. doi:10.1007/978-3-642-30885-7_27.
• [27] Dershowitz N, Falkovich-Derzhavetz E. On the Parallel Computation Thesis. Logic Journal of the IGPL, 2016. 24(3):346-374. doi:10.1093/jigpal/jzw008.
• [28] Lynch N. Distributed Algorithms. Morgan Kaufmann, 1996. ISBN-10:9781558603486, 13:978-1558603486.
• [29] Agha G. A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, Mass., 1986.
• [30] Bergstra J, Ponse A, Smolka S. Handbook of Process Algebra. Elsevier, 2001. ISBN-978-0-444-82830-9.
• [31] Best E. Semantics of sequential and parallel programs. Prentice Hall, 1996. ISBN-978-0-13-460643-9.
• [32] Genrich HJ, Lautenbach K. System Modelling with High-Level Petri Nets. Theoretical Computer Science, 1981. 13(1):109-136. doi:10.1016/0304-3975(81)90113-4.
• [33] Mazurkiewicz A. Trace Theory. volume 255 of LNCS. Springer, 1987 pp. 279-324. doi:10.1007/3-540-17906-2_30.
• [34] Schewe KD, Ferrarotti F, Tec L, Wang Q, An W. Evolving Concurrent Systems - Behavioural Theory and Logic. In: Proceedings of the Australasian Computer Science Week Multiconference (ACSW 2017). ACM, 2017 pp. 77:1-77:10. doi:10.1145/3014812.3017446.
• [35] Ferrarotti F, González S, Schewe KD. BSP Abstract State Machines Capture Bulk Synchronous Parallel Computations. Sci. Comput. Program., 2019. 184. doi:10.1016/j.scico.2019.102319.
• [36] Schewe KD, Ferrarotti F. Behavioural Theory of Reflective Algorithms I: Reflective Sequential Algorithms, 2018. Submitted for publication, available at http://arxiv.org/abs/2001.01873.
• [37] Ferrarotti F, Schewe KD, Tec L. A Behavioural Theory for Reflective Sequential Algorithms. In: Petrenko AK, Voronkov A (eds.), Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference (PSI 2017), volume 10742 of LNCS. Springer, 2017 pp. 117-131. doi:10.1007/978-3-319-74313-4_10.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).