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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
A.J.J. Dick. Eril equational reasoning: an interactive laboratory. In B. Buchberger, editor, Proceedings of the EUROCAL conference, Springer-Verlag, Linz (Austria), 1985.
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.
H. Ganzinger. Completion Procedure for Conditional Equations. Technical Report 234, Dortmund University, 1987.
M-C. Gaudel. A First Introduction to PLUSS. Meteor Report, LRI, 1984.
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.
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.
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.
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.
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.
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.
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.
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.
J.A. Goguen and J. Meseguer. Remarks on remarks on many-sorted equational logic. Bulletin of EATCS, (30):66–73, October 1986.
J.A. Goguen, J. Meseguer, and D. Plaisted. Programming with parameterized abstract objects in OBJ. Theory And Practice of Software Technology, 163–193, 1982.
J.A. Goguen and U. Montanari. An Abstract Machine for Fast Pattern Matching of Linear Pattern. Technical Report, SRI International, 1987.
C.M. Hoffmann and M.J. O'Donnell. Programming with equations. Transactions on Programming Languages and Systems, 4(1), 1982.
G. Huet and JJ. Levy. Computations in Non-ambiguous Linear Term Rewriting Systems. Technical Report, INRIA Laboria, 1979.
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.
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.
S. Kaplan. A compiler for term rewriting system. In Proceedings Second Conference on Rewriting Techniques and Applications, Springer Verlag, Bordeaux (France), May 1987.
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.
C. Kirchner. Order-sorted equational unification. 1988.
C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ3. Technical Report 87-R-87, Centre de Recherche en Informatique de Nancy, 1987.
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.
A. Megrelis. (S, <, Σ)-algebras and-homomorphisms. Personal communication, March 1986.
J. Meseguer. An algorithm to compile righthand sides. Personal communication, March 1987.
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.
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.
G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery, 28:233–264, 1981.
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.
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.
G.L. Steele. Common Lisp: The Language. Digital Press, 1984.
Y. Toyama. Counterexamples to terminating for the direct sum of term rewriting systems. In Information Processing Letters, pages 141–143, May 1986.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights 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