Abstract
This paper surveys the use of rewriting for prototyping languages based on equations as are algebraic specifications. The option is to stress the variety of questions expressed as logical queries that can be solved by using rewriting techniques, without hiding the limitations of the method. Using rewriting itself as a specification language is investigated next. Recent trends in rewriting are briefly sketched.
This work was parly supported by the ”Greco de programmation du CNRS”, and the ESPRIT working group COMPASS.
Preview
Unable to display preview. Download preview PDF.
References
Leo Bachmair. Proof by consistency in equational theories. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.
Leo Bachmair. Canonical Equational Proofs. Birkhäuser, Boston, 1991.
Leo Bachmair and Nachum Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6(1):1–18, 1988.
Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for equational proofs. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., pages 346–357, June 1986.
Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation and superposition. In Deepak Kapur, editor, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, LNCS 607. Springer-Verlag, June 1992.
Franco Barbanera and Maribel Fernández. Combining first and higher order rewrite systems with type assignment systems. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, Utrecht, Holland, 1993.
Franco Barbanera and Maribel Fernández. Modularity of termination and confluence in combinations of rewrite systems with λω. In Proceedings of the 20th International Colloquium on Automata, Languages, and Programming, 1993.
Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic confluence. Information and Computation. to appear.
A-C. Caron, J.-L. Coquidé, and M. Dauchet. Encompassment properties and automata with constraints. In Proc. RTA 93, 1993.
Hubert Comon. Unification et disunification: Théorie et applications. Thèse de Doctorat, Institut National Polytechnique de Grenoble, France, 1988.
Hubert Comon. Inductive proofs by specifications transformation. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, pages 76–91. Springer-Verlag, April 1989.
Hubert Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387–411, 1990.
Hubert Comon. Disunification: a survey. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.
Hubert Comon. Completion of rewrite systems with membership constraints. In W. Kuich, editor, Proc. 19th Int. Coll. on Automata, Languages and Programming, LNCS 623, Vienna, 1992. Springer-Verlag. An extended version is available as LRI Research Report number 699, Sept. 1991.
Nachum Dershowitz. Applications of the Knuth-Bendix completion procedure. In Proceedings of the Seminaire d'Informatique Theorique, pages 95–111, Paris, France, December 1982.
Nachum Dershowitz. A taste of rewrite systems. In Proc. Functional Programming, Concurrency, Simulation and Automated Reasonning, 1993.
Nachum Dershowitz. Trees, ordinals and termination. In Proc. CAAP 93, LNCS 668, 1993.
Nachum Dershowitz and Charles Hoot. Topics in termination. In Proc. 5th Rewriting Techniques and Applications, Montréal, LNCS 690, 1993.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.
Nachum Dershowitz, Stéphane Kaplan, and David A. Plaisted. Infinite normal forms. In Proc. 16th Int. Coll. on Automata, Languages and Programming, LNCS 372, pages 249–262, Stresa, Italy, July 1989. European Association of Theoretical Computer Science.
Hervé Devie. Une approche algébrique de la réécriture de preuves équationnelles et son application à la dérivation de procédures de complétion. Thèse de Doctorat, Université de Paris-Sud, France, Octobre 1991.
Volker Diekert. On the Knuth-Bendix completion for concurrent processes. Universität München.
K. Drosten. On termination in combined term rewriting systems:theoretical back-ground and application to prototyping parametric algebraic specifications. TU Braunshweig.
M. Fay. First-order unification in an equational theory. In Proc. 4th Workshop on Automated Deduction, Austin, Texas, pages 161–167, 1979.
Maribel Fernández. Narrowing based procedures for equational disunification. Applicable Algebra in Engineering Communication and Computing, 3:1–26, 1992.
Laurent Fribourg. A strong restriction of the inductive completion procedure. Journal of Symbolic Computation, 8:253–276, 1989.
J. A. Goguen. How to prove inductive hypothesis without induction. In Proc. 5th Conf. on Automated Deduction, Les Arcs, France, LNCS 87, July 1980.
J. A. Goguen, T. Winkler, José Meseguer, K. Futatsugi, and Jean-Pierre Jouannaud. Applications of Algebraic Specifications Using OBJ, chapter Introducing OBJ. Cambridge University Press, 1991. D. Coleman, R. Gallimore and J. Goguen eds.
G. Gonthier, J.-J. Lévy, and P.-A. Mellies. An abstract standardisation theorem. In Proc. 7th IEEE Symp. on Logic in Computer Science, Santa Cruz, CA, 1992.
Jieh Hsiang and Michaël Rusinowitch. On word problems in equational theories. In Proc. in 14th ICALP Karlsruhe, July 1987.
Gérard Huet. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, October 1980.
Gérard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences, 23:11–21, 1981.
Gérard Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2), 1982.
Gérard Huet. and Jean-Jacques Lévy. Computations in orthogonal term rewriting systems. In Gordon Plotkin and Jean-Louis Lassez, editors, Computational Logic: essays in Honour of Alan Robinson. MIT Press, 1990.
J.-M. Hullot. Canonical forms and unification. In Proc. 5th Conf. on Automated Deduction, Les Arcs, France, LNCS 87. Springer-Verlag, July 1980.
Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, 1991.
Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155–1194, 1986.
Jean-Pierre Jouannaud and Emmanuel Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.
Jean-Pierre Jouannaud and Mitsuhiro Okada. Executable higher-order algebraic specification languages. In Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam, pages 350–361, 1991.
Jean-Pierre Jouannaud and Mitsuhiro Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In Proc. 18th Int. Coll. on Automata, Languages and Programming, Madrid, LNCS 510, 1991.
Deepak Kapur, Paliath Narendran, and Hantao Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Informatics, 24(4):395–415, 1987.
J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Transfinite reductions in orthogonal term rewriting systems. In Proc. 4th Rewriting Techniques and Applications, Como, LNCS 488, 1991.
Jan Willem Klop and Aart Middeldorp. Sequenliality in orthogonal term rewriting systems. Technical report, CWI, Amsterdam, 1989.
Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.
G. Kucherov and M. Tajine. Decidability of regularity and related properties of ground normal form languages. Research Report 92-R-062, CRIN, Nancy, France, 1992. To appear in Information and Computation.
Mahahito Kurihara and Azuma Ohuchi. Non-copying term rewriting and modularity of termination. Hokkaido University.
Yves Lafont. Penrose diagrams and 2-dimensional rewriting, October 1991. extended abstract.
Claude Marché. Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certains classes de théories équationnelles. Thèse de Doctorat, Université de Paris-Sud, France, 1993.
José Meseguer. General logics. Technical Report SRI-CSL-89-05, SRI International, March 1989. Proc. Logic Colloquium'87.
José Meseguer. Conditional rewriting logic as a unified model of concurrency. Technical Report SRI-CSL-91-05, SRI International, February 1991. TCS 96 (1992) 73–155.
Y. Métivier. About the rewriting systems produced by the knuth-bendix completion algorithm. Information Processing Letters, 16(1):31–34, 1983.
A. Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, pages 263–277. Springer-Verlag, 1989.
A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In Proc. 4th Rewriting Techniques and Applications, Como, LNCS 488, 1991.
Aart Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Free University of Amsterdam, Netherland, 1990.
D. Musser. Proving inductive properties of abstract data types. In Proc. 7th ACM Symp. Principles of Programming Languages, Las Vegas, 1980.
M. H. A. Newman. On theories with a combinatorial definition of ‘equivalence'. Ann. Math., 43(2):223–243, 1942.
Robert Nieuwenhuis and Albert Rubio. Completion of first-order clauses by basic superposition with ordering constraints. Tech. report, Dept. L.S.I., Univ. Polit. Catalunya, 1991. To appear in Proc. 11th Conf. on Automated Deduction, Saratoga Springs, 1992.
Robert. Nieuwenhuis and Albert Rubio. Basic superposition is complete. In B. Krieg-Bruckner, editor, Proc. European Symp. on Programming, LNCS 582, pages 371–389, Rennes, 1992. Springer-Verlag.
W. Nutt, P. Réty, and Gert Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7(3/4):295–318, 1989.
Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233–264, April 1981.
David Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182–215, 1985.
David A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65(2–3):182–215, May/June 1985.
C. C. Squier. Word problems and a homological finiteness condition for monoids. Journal of Pure and Applied Algebra, 49:201–217, 1987.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 134–191. Elsevier, 1990.
Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, April 1987.
Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128–143, April 1987.
Ralf Treinen. A new method for undecidability proofs of first order theories. Tech. Report. A-09/90, Universität des Saarladandes, Saarbrücken, May 1990.
H. Zhang. Automated proof of ring commutativity problems by algebraic methods. Journal of Symbolic Computation, 9:423–427, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jouannaud, JP. (1994). Rewriting techniques for software engineering. In: Ehrig, H., Orejas, F. (eds) Recent Trends in Data Type Specification. ADT COMPASS 1992 1992. Lecture Notes in Computer Science, vol 785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57867-6_2
Download citation
DOI: https://doi.org/10.1007/3-540-57867-6_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57867-3
Online ISBN: 978-3-540-48361-8
eBook Packages: Springer Book Archive