×

A behavioural theory of recursive algorithms. (English) Zbl 1497.68552

Summary: “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 (nondeterministic) 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.

MSC:

68W01 General topics in the theory of algorithms
03D75 Abstract and axiomatic computability and recursion theory

Software:

Rodin
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] B¨orger E. Computability, Complexity, Logic, volume 128 ofStudies 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. · Zbl 1365.68258
[4] B¨orger E, St¨ark RF. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, 2003. doi:10.1007/978-3-642-18216-7. · Zbl 1040.68042
[5] Abrial JR. Modeling in Event-B - System and Software Engineering. Cambridge University Press, 2010. ISBN-10:0521895561, 13:978-0521895569. · Zbl 1213.68214
[6] Abrial JR. The B-book - Assigning programs to meanings. Cambridge University Press, 1996. ISBN0521496195, 9780521496193. · Zbl 0915.68015
[7] Moschovakis YN. Abstract recursion as a foundation of the theory of algorithms. In: B¨orger E, Oberschelp W, Richter M, Schinzel B, WThomas (eds.), Computation and Proof Theory, volume 1104 ofLecture Notes in Mathematics, p. 289364. Springer, 1984. ISBN-978-3-540-13901-0. · Zbl 0599.03052
[8] Moschovakis YN. On founding the theory of algorithms. In: Dales HG, Oliveri G (eds.), Truth in mathematics, pp. 71-104. Clarendon Press, 1998. · Zbl 0924.03073
[9] Moschovakis YN. Abstract Recursion and Intrinsic Complexity. Cambridge University Press, 2019. Lecture Notes in Logic. ISBN-10:110841558X, 13:978-1108415583. · Zbl 1412.03004
[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. · Zbl 1025.03037
[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: EB¨orger (ed.), Specification and Validation Methods, pp. 9-36. Oxford University Press, 1995. · Zbl 0852.68053
[13] Gurevich Y, Spielmann M. Recursive Abstract State Machines.J. UCS, 1997.3(4):233-246. doi: 10.3217/jucs-003-04-0233. · Zbl 0960.68091
[14] B¨orger E, Bolognesi T. Remarks on Turbo ASMs for Functional Equations and Recursion Schemes. In: B¨orger E, et al. (eds.), Abstract State Machines, Advances in Theory and Practice, 10th International Workshop (ASM 2003), volume 2589 ofLecture Notes in Computer Science. Springer, 2003 pp. 218-228. doi:10.1007/3-540-36498-6 12. · Zbl 1021.68035
[15] Vardi MY. What is an algorithm?Commun. ACM, 2012.55(3):5. doi:10.1145/2093548.2093549.
[16] B¨orger E, Schewe KD. Concurrent Abstract State Machines.Acta Informatica, 2016.53(5):469-492. doi:10.1007/s00236-015-0249-7. · Zbl 1352.68176
[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. · Zbl 0419.68045
[18] B¨orger 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 ofLNCS. Springer, 2020 pp. 79-92. doi:10.1007/978-3-030-48077-6 6. · Zbl 1497.68174
[19] Mayr R. Process Rewrite Systems.Information and Computation, 1999.156:264-286. doi:10.1006/ inco.1999.2826. · Zbl 1046.68566
[20] B¨orger E, Raschke A. Modeling Companion for Software Practitioners. Springer, 2018. doi:10.1007/9783-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. · Zbl 1355.68087
[22] B¨orger 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. · Zbl 1365.68253
[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. · Zbl 1367.68097
[25] Schewe KD, Wang Q. A Customised ASM Thesis for Database Transformations.Acta Cybernetica, 2010. 19(4):765-805. · Zbl 1224.68029
[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 ofLNCS. 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. · Zbl 1407.68186
[28] Lynch N. Distributed Algorithms. Morgan Kaufmann, 1996. ISBN-10:9781558603486, 13:9781558603486. · Zbl 0877.68061
[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. Elsevierl, 2001. ISBN-978-0-444-82830-9. · Zbl 0971.00006
[31] Best E. Semantics of sequential and parallel programs. Prentice Hall, 1996. ISBN-978-0-13-460643-9. · Zbl 0860.68065
[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. · Zbl 0454.68052
[33] Mazurkiewicz A. Trace Theory. volume 255 ofLNCS. Springer, 1987 pp. 279-324. doi:10.1007/3-54017906-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´alez 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 athttp://arxiv.org/abs/2001.01873.
[37] Ferrarotti F, Schewe KD, Tec L.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.