Skip to main content
SpringerLink
Log in

Operational semantics of OBJ-3

  • Conference paper
  • First Online:
Book cover Automata, Languages and Programming (ICALP 1988)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 317))

Included in the following conference series:

Abstract

An efficient operational semantics for order-sorted algebras is given, based on the notion of equational order-sorted rewriting with improvements such as general variables allowing to discard sort checks, and such as partition of the set of rewrite rules allowing fast selection of the rewrite rule to be applied. These improvements imply a process of specialization of the rules given in an OBJ-3 module. Under some conditions on a hierarchy of modules, this specialization can be incremental.

Extended Abstract

Supported by Office of Naval Research Contract N00014-85-C-0417 and GRECO de Programmation (CNRS France).

Part of this work has been done at SRI-CSL during the academic year 85–86.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R.M. Burstall, D.B. MacQueen, and D.T. Sannella. Hope: an experimental applicative language. In Conference Record of the 1980 LISP Conference, pages 136–143, Stanford (Californie, USA), 1980.

    Google Scholar 

  2. A.J.J. Dick. Eril equational reasoning: an interactive laboratory. In B. Buchberger, editor, Proceedings of the EUROCAL conference, Springer-Verlag, Linz (Austria), 1985.

    Google Scholar 

  3. K. Futatsugi, J.A. Goguen, J.P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings of 12th ACM Symposium on Principles of Programming Languages Conference, 1985.

    Google Scholar 

  4. H. Ganzinger. Completion Procedure for Conditional Equations. Technical Report 234, Dortmund University, 1987.

    Google Scholar 

  5. M-C. Gaudel. A First Introduction to PLUSS. Meteor Report, LRI, 1984.

    Google Scholar 

  6. I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in order-sorted algebras. In M. Dauchet and M. Nivat, editors, Proceedings of the 13th Colloquium on Trees in Algebra and Programming, pages 165–184, Springer-Verlag, Nancy (France), 1988.

    Google Scholar 

  7. J. Goguen, C. Kirchner, H. Kirchner, A. Megrelis, J. Meseguer, and T. Winkler. An introduction to OBJ 3. In J-P. Jouannaud and S. Kaplan, editors, Proceedings of the first international workshop on conditional term rewriting systems, Springer-Verlag, Orsay (France), June 1988. Also as internal report CRIN: 88-R-001.

    Google Scholar 

  8. J. Goguen, C. Kirchner, and J. Meseguer. Concurrent term rewriting as a model of computation. In Proceedings of the workshop on graph reduction, September 1986.

    Google Scholar 

  9. J. Goguen, C. Kirchner, J. Meseguer, and T. Winkler. OBJ as a language for concurrent programming. In Proceedings of the second international conference on supercomputing, May 1987.

    Google Scholar 

  10. J. Goguen and J. Meseguer. Order-Sorted Algebra I: Partial and Overloaded Operations, Errors and Inheritance. Technical Report To appear, SRI International, Computer Science Lab, 1988. Given as lecture at Seminar on Types, Carnegie-Mellon University, June 1983.

    Google Scholar 

  11. J.A. Goguen, J.P. Jouannaud, and J. Meseguer. Operational semantics for order-sorted algebra. In Proceeding of the 12th ICALP, Nafplion (Greece), pages 221–231, 1985.

    Google Scholar 

  12. J.A. Goguen, C. Kirchner, S. Leinwand, J. Meseguer, and T. Winkler. Progress report on the rewrite rule machine. IEEE Computer Architecture Technical Commitee Newsletter, 7–21, march 1986.

    Google Scholar 

  13. J.A. Goguen and J. Meseguer. Order-sorted algebra solves the constructor-selector, multiple representation and coercion problem. In Proceeding of the second symposium on Logic In Computer Science, 1987.

    Google Scholar 

  14. J.A. Goguen and J. Meseguer. Remarks on remarks on many-sorted equational logic. Bulletin of EATCS, (30):66–73, October 1986.

    Google Scholar 

  15. J.A. Goguen, J. Meseguer, and D. Plaisted. Programming with parameterized abstract objects in OBJ. Theory And Practice of Software Technology, 163–193, 1982.

    Google Scholar 

  16. J.A. Goguen and U. Montanari. An Abstract Machine for Fast Pattern Matching of Linear Pattern. Technical Report, SRI International, 1987.

    Google Scholar 

  17. C.M. Hoffmann and M.J. O'Donnell. Programming with equations. Transactions on Programming Languages and Systems, 4(1), 1982.

    Google Scholar 

  18. G. Huet and JJ. Levy. Computations in Non-ambiguous Linear Term Rewriting Systems. Technical Report, INRIA Laboria, 1979.

    Google Scholar 

  19. G. Huet and D. Oppen. Equations and rewrite rules: a survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, Academic Press, 1980.

    Google Scholar 

  20. J.P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15(4), 1986. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City, 1984.

    Google Scholar 

  21. S. Kaplan. A compiler for term rewriting system. In Proceedings Second Conference on Rewriting Techniques and Applications, Springer Verlag, Bordeaux (France), May 1987.

    Google Scholar 

  22. C. Kirchner. Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories équationnelles. Thèse d'état de l'Université de Nancy I, 1985.

    Google Scholar 

  23. C. Kirchner. Order-sorted equational unification. 1988.

    Google Scholar 

  24. C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ3. Technical Report 87-R-87, Centre de Recherche en Informatique de Nancy, 1987.

    Google Scholar 

  25. H. Kirchner. Preuves par complétion dans les variétés d'algèbres. Thèse d'état de l'Université de Nancy I, 1985.

    Google Scholar 

  26. A. Megrelis. (S, <, Σ)-algebras and-homomorphisms. Personal communication, March 1986.

    Google Scholar 

  27. J. Meseguer. An algorithm to compile righthand sides. Personal communication, March 1987.

    Google Scholar 

  28. J. Meseguer and J.A. Goguen. Initiality, induction and computability. In M. Nivat and J. Reynolds, editors, Algebraic Methods in Semantics, Cambridge University Press, 1985.

    Google Scholar 

  29. J. Meseguer, J.A. Goguen, and G. Smolka. Order sorted unification. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, May 1987.

    Google Scholar 

  30. G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery, 28:233–264, 1981.

    Google Scholar 

  31. M. Schmidt-Schauss. Unification in many sorted equational theories. In J. Siekmann, editor, Proceedings 8th Conference on Automated Deduction, Oxford, Springer Verlag, Oxford (England), 1986.

    Google Scholar 

  32. G. Smolka, W. Nutt, J.A. Goguen, and J. Meseguer. Order sorted equational computation. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, May 1987.

    Google Scholar 

  33. G.L. Steele. Common Lisp: The Language. Digital Press, 1984.

    Google Scholar 

  34. Y. Toyama. Counterexamples to terminating for the direct sum of term rewriting systems. In Information Processing Letters, pages 141–143, May 1986.

    Google Scholar 

  35. Y. Toyama. On the church-rosser property for the direct sum of term rewriting systems. Journal of the Association for Computing Machinery, 34(1):128–143, January 1986.

    Google Scholar 

  36. D.A. Turner, Miranda: a non-strict functional language with polymorphic types. In Proc. 2nd Conf. on Functional Programming Languages and Computer Architecture, pages 1–16, Springer Verlag, Nancy (France), 1985.

    Google Scholar 

  37. C. Walther. Unification in many sorted theories. In T. O'Shea, editor, Proceedings of the European Conference on Artificial Intelligence, Pisa, Italy, pages 593–602, ECAI, 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LORIA & CRIN, BP 239, 54506, Vandœuvre-lès-Nancy Cedex, France

    Claude Kirchner & Hélène Kirchner

  2. SRI International, Computer Science Laboratory, 333 Ravenswood Avenue, 94025, Menlo Park, CA, USA

    José Meseguer

Authors
  1. Claude Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hélène Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Timo Lepistö Arto Salomaa

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kirchner, C., Kirchner, H., Meseguer, J. (1988). Operational semantics of OBJ-3. In: Lepistö, T., Salomaa, A. (eds) Automata, Languages and Programming. ICALP 1988. Lecture Notes in Computer Science, vol 317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19488-6_123

Download citation

  • DOI: https://doi.org/10.1007/3-540-19488-6_123

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19488-0

  • Online ISBN: 978-3-540-39291-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation