Advertisement

Semantic Specifications for the Rewrite Rule Machine

  • Joseph A. Goguen
Part of the Advances in Formal Methods book series (ADFM, volume 2)

Abstract

This paper presents three semantic specifications for the Rewrite Rule Machine. This machine consists of a large number of parallel rewrite processors operating independently, each implemented as a VLSI chip. The first specification, called parallel rewriting, provides an abstract operational semantics for the rewrite processor. The second specification, called the cell machine model, provides a more concrete operational semantics for this processor, using algebraic semantics (in OBJ) and set theory. The third specification, called concurrent rewriting, gives an abstract semantics for the Rewrite Rule Machine as a whole.

Keywords

Operational Semantic Single Instruction Multiple Data Fibonacci Number Equational Logic Cell Machine 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Hitoshi Aida, Joseph Goguen, and Josè Meseguer. Compiling concurrent rewriting onto the Rewrite Rule Machine. Technical Report SRI-CSL90–03, Computer Science Lab, SRI International, February 1990. To appear in Proceedings, International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, 1990.Google Scholar
  2. [2]
    Hitoshi Aida, Sany Leinwand, and Josè Meseguer. Architectural design of the Rewrite Rule Machine ensemble. Technical Report to appear, Computer Science Lab, SRI International, 1990. Also, to appear in Proceedings, International Workshop on VLSI for Artificial Intelligence and Neural Nets, edited by Will Moore and A. Delgado-Frias, Oxford, 1990.Google Scholar
  3. [3]
    Rod Burstall and Joseph Goguen. Algebras, theories and freeness: An introduction for computer scientists. In Martin Wirsing and Gunther Schmidt, editors, Theoretical Foundations of Programming Methodology, pages 329–350. Reidel, 1982. Proceedings, 1981 Marktoberdorf NATO Summer School, NATO Advanced Study Institute Series, Volume C91.Google Scholar
  4. [4]
    Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud, and José Meseguer. Principles of OBJ2. In Brian Reid, editor, Proceedings, Twelfth ACM Symposium on Principles of Programming Languages, pages 5266. Association for Computing Machinery, 1985.Google Scholar
  5. [5]
    Kokichi Futatsugi, Joseph Goguen, José Meseguer, and Koji Okada. Parameterized programming in OBJ2. In Robert Balzer, editor, Proceedings, Ninth International Conference on Software Engineering, pages 51–60. IEEE Computer Society, March 1987.Google Scholar
  6. [6]
    Joseph Goguen. How to prove algebraic inductive hypotheses without induction: with applications to the correctness of data type representations. In Wolfgang Bibel and Robert Kowalski, editors, Proceedings, Fifth Conference on Automated Deduction, pages 356–373. Springer, 1980. Lecture Notes in Computer Science, Volume 87.Google Scholar
  7. [7]
    Joseph Goguen. Parameterized programming. Transactions on Software Engineering, SE-10(5): 528–543, September 1984.Google Scholar
  8. [8]
    Joseph Goguen. Graphical programming by generic example. In Steven Kartashev and Svetlana Kartashev, editors, Proceedings, Second International Supercomputing Conference, Volume Ipages 209–216. International Supercomputing Institute, Inc. (St. Petersburg FL), 1987. Google Scholar
  9. [9]
    Joseph Goguen. OBJ as a theorem prover, with application to hardware verification. In V.P. Subramanyan and Graham Birtwhistle, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 218–267. Springer, 1989. Also Technical Report SRI-CSL-88–4R2, SRI International, Computer Science Lab, August 1988.Google Scholar
  10. [10]
    Joseph Goguen. Principles of parameterized programming. In Ted Biggerstaff and Alan Perlis, editors, Software Reusability, Volume I: Concepts and Modelspages 159–225. Addison-Wesley, 1989. Google Scholar
  11. [11]
    Joseph Goguen. Proving and rewriting. In Proceedings, Second International Conference on Algebraic and Logic Programmingpages 1–24. Springer, 1990. Lecture Notes in Computer Science, Volume 463. Google Scholar
  12. [12]
    Joseph Goguen, Claude Kirchner, Sany Leinwand, José Meseguer, and Timothy Winkler. Progress report on the Rewrite Rule Machine. IEEE Computer Architecture Technical Committee Newsletter, March: 7–21, 1986.Google Scholar
  13. [13]
    Joseph Goguen, Claude Kirchner, and José Meseguer. Concurrent term rewriting as a model of computation. In Robert Keller and Joseph Fasel, editors, Proceedings, Graph Reduction Workshop, pages 53–93. Springer, 1987. Lecture Notes in Computer Science, Volume 279.Google Scholar
  14. [14]
    Joseph Goguen, Claude Kirchner, José Meseguer, and Timothy Winkler. OBJ as a language for concurrent programming. In Steven Kartashev and Svetlana Kartashev, editors, Proceedings, Second International Supercomputing Conference, Volume I, pages 195–198. International Supercomputing Institute, Inc. (St. Petersburg FL ), 1987.Google Scholar
  15. [15]
    Joseph Goguen, Sany Leinwand, José Meseguer, and Timothy Winkler. The Rewrite Rule Machine, 1989. Technical Report Technical Monograph PRG-76, Programming Research Group, Oxford University, 1989.Google Scholar
  16. [16]
    Joseph Goguen and José Meseguer. Eqlog: Equality, types, and generic modules for logic programming. In Douglas DeGroot and Gary Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 295–363. Prentice-Hall, 1986. An earlier version appears in Journal of Logic Programming, Volume 1, Number 2, pages 179–210, September 1984.Google Scholar
  17. [17]
    Joseph Goguen and José Meseguer. Models and equality for logical programming. In Hartmut Ehrig, Giorgio Levi, Robert Kowalski, and Ugo Montanari, editors, Proceedings, 1987 TAPSOFT, pages 1–22. Springer, 1987. Lecture Notes in Computer Science, Volume 250.Google Scholar
  18. [18]
    Joseph Goguen and José Meseguer. Unifying functional, object-oriented and relational programming, with logical semantics. In Bruce Shriver and Peter Wegner, editors, Research Directions in Object-Oriented Programming, pages 417–477. MIT, 1987. Preliminary version in SIGPLAN Notices, Volume 21, Number 10, pages 153–162, October 1986.Google Scholar
  19. [19]
    Joseph Goguen and José Meseguer. Software for the Rewrite Rule Machine. In Proceedings, International Conference on Fifth Generation Computer Systems 1988, pages 628–637. Institute for New Generation Computer Technology (ICOT), 1988.Google Scholar
  20. [20]
    Joseph Goguen and José Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Technical Report SRI-CSL-89–10, SRI International, Computer Science Lab, July 1989. Given as lecture at Seminar on Types, Carnegie-Mellon University, June 1983; many draft versions exist.Google Scholar
  21. [21]
    Joseph Goguen, James Thatcher, and Eric Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. Technical Report RC 6487, IBM T.J. Watson Research Center, October 1976. In Current Trends in Programming Methodology, IV, Raymond Yeh, editor, Prentice-Hall, 1978, pages 80–149.Google Scholar
  22. [22]
    Joseph Goguen et al. Introducing OBJ3. This volume.Google Scholar
  23. [23]
    Joseph Goguen and David Wolfram. On types and FOOPS. In Proceedings, IFIP TC2 Conference on Object Oriented Databases. IFIP, to appear 1990. Google Scholar
  24. [24]
    Gérard Huet and Derek Oppen. Equations and rewrite rules: A survey. In Ron Book, editor, Formal Language Theory: Perspectives and Open Problemspages 349–405. Academic, 1980. Google Scholar
  25. [25]
    R.M. Lea. ASP: A cost-effective parallel microcomputer. IEEE Micro, 8 (5): 10–29, 1988.CrossRefGoogle Scholar
  26. [26]
    Sany Leinwand and Joseph Goguen. Architectural options for the Rewrite Rule Machine. In Steven Kartashev and Svetlana Kartashev, editors, Proceedings, Second International Supercomputing Conference, Volume Ipages 63–70. International Supercomputing Institute, Inc. (St. Petersburg FL), 1987. Google Scholar
  27. [27]
    Sany Leinwand, Joseph Goguen, and Timothy Winkler. Cell and ensemble architecture of the Rewrite Rule Machine. In Proceedings, International Conference on Fifth Generation Computer Systems 1988pages 869–878. Institute for New Generation Computer Technology (ICOT), 1988. Google Scholar
  28. [28]
    José Meseguer. Rewriting as a unified model of concurrency. In Proceedings, Concur’90 Conference,number 458 in Lecture Notes in Computer Science, pages 384–400, Amsterdam, August 1990. Springer. Also, Technical Report SRI-CSL-90–02R, Computer Science Lab, SRI International.Google Scholar
  29. [29]
    José Meseguer and Joseph Goguen. Initiality, induction and computability. In Maurice Nivat and John Reynolds, editors, Algebraic Methods in Semanticspages 459–541. Cambridge, 1985. Google Scholar
  30. [30]
    Peter M. Sewell. Cell machine correctness via parallel jungle rewriting, 1990. MSc Thesis, Programming Research Group, University of Oxford.Google Scholar
  31. [31]
    David Shu, Lap-Wai Chow, Greg Nash, and Charles Weems. A content addressable, bit-serial associative processor. In Proceedings, IEEE Workshop on VLSI Signal Processingpages 120–128. IEEE Computer Society, 1988. Google Scholar
  32. [32]
    David Shu, Greg Nash, and Charles Weems. Image understanding architecture and applications. In Jorge Sanz, editor, Machine Vision. Springer, 1988.Google Scholar
  33. [33]
    Timothy Winkler. Numerical computation on the RRM. Technical report, SRI International, Computer Science Lab, November 1988. Technical Note SRI-CSL-TN88–3.Google Scholar
  34. [34]
    Timothy Winkler, Sany Leinwand, and Joseph Goguen. Simulation of concurrent term rewriting. In Steven Kartashev and Svetlana Kartashev, editors, Proceedings, Second International Supercomputing Conference, Volume I, pages 199–208. International Supercomputing Institute, Inc. (St. Petersburg FL ), 1987.Google Scholar

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • Joseph A. Goguen
    • 1
  1. 1.Department of Computer Science and EngineeringUniversity of California at San DiegoUSA

Personalised recommendations