Program Algebra for Turing-Machine Programs – Facultatea de Informatică

Published in Volume XXIX, Issue 2, 2019, pages 113-139, doi: 10.7561/SACS.2019.2.113

Authors: J.A. Bergstra, C.A. Middelburg

Abstract

This paper presents an algebraic theory of instruction sequences with instructions for Turing tapes as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such behaviours and Turing tapes provided by an execution environment. This theory provides a setting for the development of theory in areas such as computability and computational complexity that distinguishes itself by offering the possibility of equational reasoning and being more general than the setting provided by a known version of the Turing-machine model of computation. The theory is essentially an instantiation of a parameterized algebraic theory which is the basis of a line of research in which issues relating to a wide variety of subjects from computer science have been rigorously investigated thinking in terms of instruction sequences.

Full Text (PDF)

References

[1] A.V. Aho, J.E. Hopcroft, J.D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, MA, 1974.

[2] S. Arora, B. Barak. Computational Complexity: A Modern Approach. Cambridge University Press, Cambridge, 2009.

[3] A. Asperti, W. Ricciotti. A Formalization of Multi-tape Turing Machines. Theoretical Computer Science 603, 23-42, 2015. doi:10.1016/j.tcs.2015.07.013.

[4] J.A. Bergstra, M.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] J.A. Bergstra, C.A. Middelburg. Instruction Sequence Processing Operators. Acta Informatica 49(3), 139-172, 2012. doi:10.1007/s00236-012-0154-2.

[6] J.A. Bergstra, C.A. Middelburg. Instruction Sequences for Computer Science, volume 2 of Atlantis Studies in Computing. Atlantis Press, Amsterdam, 2012. doi:10.2991/978-94-91216-65-7.

[7] J.A. Bergstra, C.A. Middelburg. Instruction Sequence Expressions for the Secure Hash Algorithm SHA-256. 2013. arXiv:1308.0219.

[8] J.A. Bergstra, C.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.

[9] J.A. Bergstra, C.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.

[10] J.A. Bergstra, C.A. Middelburg. Instruction Sequence Size Complexity of Parity. Fundamenta Informaticae 149(3), 297-309, 2016. doi:10. 3233/fi-2016-1450.

[11] J.A. Bergstra, C.A. Middelburg. Instruction Sequences Expressing Multiplication Algorithms. Scientific Annals of Computer Science 28(1), 39-66, 2018. doi:10.7561/sacs.2018.1.39.

[12] J.A. Bergstra, C.A. Middelburg. A Short Introduction to Program Algebra with Instructions for Boolean Registers. Computer Science Journal of Moldova 26(3), 199-232, 2018.

[13] J.A. Bergstra, C.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.

[14] M. Broy, W. Dosch, B. Möller, M. Wirsing. GOTOs – A Study in the Algebraic Specification of Programming Languages (Extended Abstract). In W. Brauwer (Ed.) GI – 11. Jahrestagung, volume 50 of Informatik-Fachberichte, 109-121, 1981. doi:10.1007/978-3-662-01089-1_13.

[15] M. Broy, M. Wirsing, P. 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.

[16] H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification I: Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science 6, 1985. doi:10.1007/978-3-642-69962-7.

[17] J.A. Goguen, G. Malcolm. Algebraic Semantics of Imperative Programs. Foundations of Computing. MIT Press, Cambridge, MA, 1996. doi:10.7551/mitpress/1188.001.0001.

[18] O. Goldreich. Computational Complexity: A Conceptual Perspective. Cambridge University Press, Cambridge, 2008. doi:10.1017/CBO9780511804106.

[19] S. Homer, A.L. Selman. Computability and Complexity Theory. Springer-Verlag, Berlin, second edition, 2011. doi:10.1007/978-1-4614-0682-2.

[20] D.C. Kozen. Theory of Computation. Springer-Verlag, Berlin, 2006. doi:10.1007/1-84628-477-5.

[21] C.A. Middelburg. Instruction Sequences as a Theme in Computer Science. 2015. Springer-Verlag, Berlin, 2006. https://instructionsequence.wordpress.com/.

[22] M. Norrish. Mechanised Computability Theory. In M. van Eekelen, H. Geuvers, J. Schmaltz, F. Wiedijk (Eds.) Interactive Theorem Proving (ITP 2011), Lecture Notes in Computer Science 6898, 297-311, 2011. doi:10.1007/978-3-642-22863-6_22.

[23] D. Sannella, A. Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Seriess. Springer-Verlag, 2012. doi:10.1007/978-3-642-17336-3.

[24] M. Sipser. Introduction to the Theory of Computation. Cengage Learning, Boston, MA, third edition, 2013.

[25] A.M. Turing. On Computable Numbers, with an Application to the Entscheidungs Problem. Proceedings of the London Mathematical Society, Series 2, 42, 230-265, 1937. doi:10.1112/plms/s2-42.1.230. Correction: ibid 43, 544-546, 1938. doi:10.1112/plms/s2-43.6.544.

[26] R.J. van Glabbeek, F.W. Vaandrager. Modular Specification of Process Algebras. Theoretical Computer Science 113(2), 293{348, 1993. doi:10.1016/0304-3975(93)90006-F.

[27] M. Wirsing. Algebraic Specification. In J. van Leeuwe (Ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, 675-788. Elsevier, 1990. doi:10.1016/B978-0-444-88074-1.50018-4.

[28] J. Xu, X. Zhang, C. Urban. Mechanising Turing Machines and Computability Theory in Isabelle/HOL. In S. Blazy, C. Paulin-Mohring, D. Pichardie (Eds.) Proceedings 4th International Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science 7998, 147-162, 2013. doi:10.1007/978-3-642-39634-2_13.

Bibtex

@article{sacscuza:bergstra2019patmp,
  title={Program Algebra for Turing-Machine Programs},
  author={J. A. Bergstra, C. A. Middelburg},
  journal={Scientific Annals of Computer Science},
  volume={29},
  number={2},
  organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
  year={2019},
  pages={113–139},
  publisher={Alexandru Ioan Cuza University Press, Ia\c si},
  doi={10.7561/SACS.2019.2.113}
}