Abstract
Random Access Machines (RAMs) are a deterministic Turing-complete formalism especially well suited for being encoded in other formalisms. This is due to the fact that RAMs can be defined starting from very primitive concepts and operations, which are unbounded natural numbers, tuples, successor, predecessor and test for equality to zero. Since these concepts are easily available also in theorem-provers and proof-assistants, RAMs are good candidates for proving Turing-completeness of formalisms using a proof-assistant. In this paper we describe an encoding in Coq of RAMs into a Linda Calculus endowed with the Ordered Semantics. We discuss the main difficulties that must be faced and the techniques we adopted to solve them.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Busi, N., Gorrieri, R., Zavattaro, G.: On the Expressiveness of Linda Coordination Primitives. Information and Computation 156(1/2), 90–121 (2000)
The Coq proof-assistant, http://coq.inria.fr/
Hofmann, M.: Extensional concepts in intensional type theory. Ph.D. thesis, University of Edinburgh (July 1995)
McBride, C.: Dependently Typed Functional Programs and their Proofs. Ph.D. thesis, University of Edinburgh (2000)
Gelernter, D.: Generative Communication in Linda. ACM Transactions on Programming Languages and Systems 7(1), 80–112 (1985)
Gelernter, D., Carriero, N.: Coordination Languages and their Significance. Communications of the ACM 35(2), 97–102 (1992)
Barthe, G., Courtieu, P.: Efficient Reasoning about executable specifications in Coq. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 31–46. Springer, Heidelberg (2002)
Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical Knowledge Management in HELM. In: On-Line Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM 2001), RISCLinz, Austria (September 2001)
Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: XML, Stylesheets and the re-mathematization of Formal Content. In: On-Line Proceedings of EXTREME 2001 (2001)
Milner, R.: The Polyadic π-Calculus: A Tutorial Technical Report, Department of Computer Science, University of Edinburgh, ECS-LFCS-91-180 (October 1991)
Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Englewood Cliffs (1967)
Shepherdson, J.C., Sturgis, J.E.: Computability of recursive functions. Journal of the ACM 10, 217–255 (1963)
Busi, N., Gorrieri, R., Zavattaro, G.: A Process Algebraic View of Linda Coordination Primitives. Theoretical Computer Science 192(2), 167–199 (1998)
Busi, N., Zavattaro, G.: On the Expressiveness of Movement in Pure Mobile Ambients. In: Gregori, E., Cherkasova, L., Cugola, G., Panzieri, F., Picco, G.P. (eds.) NETWORKING 2002. LNCS, vol. 2376, Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coen, C.S. (2003). A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics. In: Blundo, C., Laneve, C. (eds) Theoretical Computer Science. ICTCS 2003. Lecture Notes in Computer Science, vol 2841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45208-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-45208-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20216-5
Online ISBN: 978-3-540-45208-9
eBook Packages: Springer Book Archive