Published in Volume XXXII, Issue 2, 2022, pages 285-319, doi: 10.7561/SACS.2022.2.285
Authors: C.A. Middelburg
Abstract
This paper presents an algebraic theory of instruction sequences with instructions for a random access machine (RAM) as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such behaviours and RAM memories. This theory provides a setting for the development of theory in areas such as computational complexity and analysis of algorithms that distinguishes itself by offering the possibility of equational reasoning to establish whether an instruction sequence computes a given function and being more general than the setting provided by any known version of the RAM model of computation. In this setting, a semi-realistic version of the RAM model of computation and a bit-oriented time complexity measure for this version are introduced. Under the time measure concerned, semi-realistic RAMs can be simulated by multi-tape Turing machines with quadratic time overhead.
Full Text (PDF)References
[1] Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley Series in Computer Science and Information Processing. Addison-Wesley Publishing Company, 1974.
[2] Andrea Asperti and Wilmer Ricciotti. A formalization of multi-tape Turing machines. Theoretical Computer Science, 603:23-42, 2015. doi:10.1016/j.tcs.2015.07.013.
[3] Jos C. M. Baeten and W. Peter Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990. doi:10.1017/CBO9780511624193.
[4] Jan A. Bergstra and Marijke E. Loots. Program algebra for sequential code. Journal of Logic and Algebraic Programming, 51(2):125-156, 2002. doi:10.1016/S1567-8326(02)00018-8.
[5] Jan A. Bergstra and Cornelis A. Middelburg. Inversive meadows and divisive meadows. Journal of Applied Logic, 9(3):203-220, 2011. doi:10.1016/j.jal.2011.03.001.
[6] Jan A. Bergstra and Cornelis A. Middelburg. Instruction sequence processing operators. Acta Informatica, 49(3):139-172, 2012. doi:10.1007/s00236-012-0154-2.
[7] Jan A. Bergstra and Cornelis A. Middelburg. Instruction Sequences for Computer Science, volume 2 of Atlantis Studies in Computing. Atlantis Press, 2012. doi:10.2991/978-94-91216-65-7.
[8] Jan A. Bergstra and Cornelis A. Middelburg. Instruction sequence expressions for the secure hash algorithm SHA-256. CoRR, abs/1308.0219, 2013. arXiv:1308.0219.
[9] Jan A. Bergstra and Cornelis A. Middelburg. Instruction sequence based non-uniform complexity classes. Scientific Annals of Computer Science, 24(1):47-89, 2014. doi:10.7561/SACS.2014.1.47.
[10] Jan A. Bergstra and Cornelis A. Middelburg. On algorithmic equivalence of instruction sequences for computing bit string functions. Fundamenta Informaticae, 138(4):411-434, 2015. doi:10.3233/FI-2015-1219.
[11] Jan A. Bergstra and Cornelis A. Middelburg. Instruction sequence size complexity of parity. Fundamenta Informaticae, 149(3):297-309, 2016. doi:10.3233/FI-2016-1450.
[12] Jan A. Bergstra and Cornelis A. Middelburg. Instruction sequences expressing multiplication algorithms. Scientific Annals of Computer Science, 28(1):39-66, 2018. doi:10.7561/sacs.2018.1.39.
[13] Jan A. Bergstra and Cornelis A. Middelburg. A short introduction to program algebra with instructions for Boolean registers. Computer Science Journal of Moldova, 26(3):199-232, 2018.
[14] Jan A. Bergstra and Cornelis A. Middelburg. Program algebra for Turing-machine programs. Scientific Annals of Computer Science, 29(2):113-139, 2019. doi:10.7561/SACS.2019.2.113.
[15] Jan A. Bergstra and Cornelis A. Middelburg. On the complexity of the correctness problem for non-zeroness test instruction sequences. Theoretical Computer Science, 802:1-18, 2020. doi:10.1016/j.tcs.2019.03.040.
[16] Jan A. Bergstra and John V. Tucker. The rational numbers as an abstract data type. Journal of the ACM, 54(2):7, 2007. doi:10.1145/1219092.1219095.
[17] Manfred Broy, Walter Dosch, Bernhard Möller, and Martin Wirsing. Gotos – A study in the algebraic specification of programming languages (extended abstract). In Wilfried Brauer, editor, GI – 11. Jahrestagung in Verbindung mit Third Conference of the European Co-operation in Informatics (ECI), volume 50 of Informatik-Fachberichte, pages 109-121. Springer, 1981. doi:10.1007/978-3-662-01089-1_13.
[18] Manfred Broy, Martin Wirsing, and Peter Pepper. On the algebraic definition of programming languages. ACM Transactions on Programming Languages and Systems, 9(1):54-99, 1987. doi:10.1145/9758.10501.
[19] Stephen A. Cook and Robert A. Reckhow. Time bounded random access machines. Journal of Computer and System Sciences, 7(4):354-375, 1973. doi:10.1016/S0022-0000(73)80029-7.
[20] Claus Diem. On the notion of bit complexity. Bulletin of the EATCS, 103:35–52, 2011.
[21] Hartmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer, 1985. doi:10.1007/978-3-642-69962-7.
[22] Joseph A. Goguen. Theorem proving and algebra. CoRR,, abs/2101.02690, 2021. arXiv:2101.02690.
[23] Joseph A. Goguen and Grant Malcolm. Algebraic Semantics of Imperative Programs. Foundations of Computing Series. MIT Press, 1996. doi:10.7551/mitpress/1188.001.0001.
[24] Juris Hartmanis and Janos Simon. On the power of multiplication in random access machines. In 15th Annual Symposium on Switching and Automata Theory (SWAT), pages 13-23. IEEE Computer Society, 1974. doi:10.1109/SWAT.1974.20.
[25] Cornelis A. Middelburg. Instruction sequences as a theme in computer science, 2021. URL: https://instructionsequence.wordpress.com
[26] Bernard M. E. Moret. Theory of Computation. Addison-Wesley-Longman, 1998.
[27] Michael Norrish. Mechanised computability theory. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Second International Conference on Interactive Theorem Proving, (ITP 2011), volume 6898 of Lecture Notes in Computer Science, pages 297-311. Springer, 2011. doi:10.1007/978-3-642-22863-6_22.
[28] Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
[29] Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2012. doi:10.1007/978-3-642-17336-3.
[30] Arnold Schönhage. On the power of random access machines. In Hermann A. Maurer, editor, 6th Colloquium on Automata, Languages and Programming, volume 71 of Lecture Notes in Computer Science, pages 520-529. Springer, 1979. doi:10.1007/3-540-09510-1_42.
[31] Peter van Emde Boas. Machine models and simulations. In Jan van Leeuwen, editor, Algorithms and Complexity, Handbook of Theoretical Computer Science, pages 1-66. Elsevier, Amsterdam, 1990. doi:10.1016/B978-0-444-88071-0.50006-0.
[32] Rob J. van Glabbeek and Frits W. Vaandrager. Modular specification of process algebras. Theoretical Computer Science, 113(2):293-348, 1993. doi:10.1016/0304-3975(93)90006-F.
[33] Martin Wirsing. Algebraic specification. In Jan van Leeuwen, editor, Formal Models and Semantics, Handbook of Theoretical Computer Science, pages 675-788. Elsevier, Amsterdam, 1990. doi:10.1016/B978-0-444-88074-1.50018-4.
[34] Jian Xu, Xingyuan Zhang, and Christian Urban. Mechanising Turing machines and computability theory in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, 4th International Conference on Interactive Theorem Proving (ITP 2013), volume 7998 of Lecture Notes in Computer Science, pages 147-162. Springer, 2013. doi:10.1007/978-3-642-39634-2_13.
Bibtex
@article{sacscuza:middelburg22paramp,
title={Program Algebra for Random Access Machine Programs},
author={C.A. Middelburg},
journal={Scientific Annals of Computer Science},
volume={32},
number={2},
organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
year={2022},
pages={285-319},
publisher={Alexandru Ioan Cuza University Press, Ia\c si},
doi={10.7561/SACS.2022.2.285}
}