Skip to main content
SpringerLink
Log in
Book cover

International Conference on Algebraic and Logic Programming

International Symposium on Programming Language Implementation and Logic Programming

ALP 1998, PLILP 1998: Principles of Declarative Programming pp 230–249Cite as

A compiler for rewrite programs in associative-commutative theories

  • Conference paper
  • First Online:

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

Abstract

We address the problem of term normalisation modulo associative-commutative (AC) theories, and describe several techniques for compiling many-to-one AC matching and reduced term construction. The proposed matching method is based on the construction of compact bipartite graphs, and is designed for working very efficiently on specific classes of AC patterns. We show how to refine this algorithm to work in an eager way. General patterns are handled through a program transformation process. Variable instantiation resulting from the matching phase and construction of the resulting term are also addressed. Our experimental results with the system ELAN provide strong evidence that compilation of many-to-one AC normalisation using the combination of these few techniques is crucial for improving the performance of algebraic programming languages.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Bachmair, T. Chen, and I. V. Ramakrishnan. Associative-commutative discrimination nets. In M.-C. Gaudel and J.-P. Jouannaud, editors, TAPSOFT '93: Theory and Practice of Software Development, 4th International Joint Conference CAAP/FASE, LNCS 668, pages 61–74, Orsay, France, Apr. 13–17, 1993. Springer-Verlag.

    Google Scholar 

  2. D. Benanav, D. Kapur, and P. Narendran. Complexity of matching problems. Journal of Symbolic Computation, 3(1 & 2):203–216, Apr. 1987.

    Article  MATH  MathSciNet  Google Scholar 

  3. P. Borovanský, C. Kirchner, and H. Kirchner. Controlling rewriting by rewriting. In J. Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4 of Electronic Notes in Theoretical Computer Science, Asilomar (California), Sept. 1996.

    Google Scholar 

  4. P. Borovanský, C. Kirchner, and H. Kirchner. Rewriting as a unified specification tool for logic and control:the elan language. In Proceedings of International Workshop on Theory and Practice of Algebraic Specifications ASF+SDF 97, Workshops in Computing, Amsterdam, Sept. 1997. Springer-Verlag.

    Google Scholar 

  5. R. Bündgen. Reduce the redex ← ReDuX. In C. Kirchner, editor, Rewriting Techniques and Applications, 5th International Conference, RTA-93, LNCS 690, pages 446–450, Montreal, Canada, June 16–18, 1993. Springer-Verlag.

    Google Scholar 

  6. J. Christian. Flatterms, discrimination nets, and fast term rewriting. Journal of Automated Reasoning, 10(1):95–113, Feb. 1993.

    Article  MathSciNet  Google Scholar 

  7. M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4, Asilomar (California), Sept. 1996. Electronic Notes in Theoretical Computer Science.

    Google Scholar 

  8. E. Contejean, C. Marché, and L. Rabehasaina. Rewrite systems for natural, integral, and rational arithmetic. In H. Comon, editor, Proceedings of 8-th International Conference Rewriting Techniques and Applications, Lecture Notes in Computer Science, pages 98–112, Sitges, Spain, 1997. Springer-Verlag.

    Google Scholar 

  9. S. Eker. Associative-commutative matching via bipartite graph matching. Computer Journal, 38(5):381–399, 1995.

    Article  Google Scholar 

  10. S. Eker. Fast matching in combinations of regular equational theories. In J. Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4, Asilomar (California), Sept. 1996. Electronic Notes in Theoretical Computer Science.

    Google Scholar 

  11. K. Fukuda and T. Matsui. Finding all the perfect matchings in bipartite graphs. Technical Report B-225, Department of Information Sciences, Tokyo Institute of Technology, Oh-okayama, Meguro-ku, Tokyo 152, Japan, 1989.

    Google Scholar 

  12. J. A. Goguen and T. Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, 333, Ravenswood Ave., Menlo Park, CA 94025, Aug. 1988.

    Google Scholar 

  13. A. Gräf. Left-to-rigth tree pattern matching. In R. V. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), volume 488 of Lecture Notes in Computer Science, pages 323–334. Springer-Verlag, Apr. 1991.

    Google Scholar 

  14. P. Graf. Term Indexing, volume 1053 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1996.

    Google Scholar 

  15. J. E. Hopcroft and R. M. Karp. An n 5/2 algorithm for maximum matchings in bipartite graphs. SIAM Journal of Computing, 2(4):225–231, 1973.

    Article  MATH  MathSciNet  Google Scholar 

  16. J.-M. Hullot. Compilation de Formes Canoniques dans les Théories équationelles. Thèse de Doctorat de Troisième Cycle, Université de Paris Sud, Orsay (France), 1980!

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  18. D. Kapur and H. Zhang. RRL: A rewrite rule laboratory. In Proceedings 9th International Conference on Automated Deduction, Argonne (Ill., USA), volume 310 of Lecture Notes in Computer Science, pages 768–769. Springer-Verlag, 1988.

    Google Scholar 

  19. C. Kirchner, H. Kirchner, and M. Vittek. Designing constraint logic programming languages using computational systems. In P. Van Hentenryck and V. Saraswat, editors, Principles and Practice of Constraint Programming. The Newport Papers., chapter 8, pages 131–158. The MIT press, 1995.

    Google Scholar 

  20. E. Kounalis and D. Lugiez. Compilation of pattern matching with associative commutative functions. In 16th Colloquium on Trees in Algebra and Programming, volume 493 of Lecture Notes in Computer Science, pages 57–73. Springer-Verlag, 1991.

    Google Scholar 

  21. D. Lugiez and J.-L. Moysset. Tree automata help one to solve equational formulae in AC-theories. Journal of Symbolic Computation, 18(4):297–318, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  22. W. W. McCune. Otter 3.0: Reference manual and guide. Technical Report 6, Argonne National Laboratory, 1994.

    Google Scholar 

  23. P.-E. Moreau and H. Kirchner. Compilation Techniques for Associative-Commutative Normalisation. In A. Sellink, editor, Second International Workshop on the Theory and Practice of Algebraic Specifications, Electronic Workshops in Computing, eWiC web site: http://ewic.springer.co.uk/, Amsterdam, Sept. 1997. Springer-Verlag. 12 pages.

    Google Scholar 

  24. N. Nedjah, C. Walter, and E. Eldrige. Optimal left-to-right pattern-matching automata. In M. Hanus, J. Heering, and K. Meinke, editors, Proceedings 6th International Conference on Algebraic and Logic Programming, Southampton (UK), volume 1298 of Lecture Notes in Computer Science, pages 273–286. Springer-Verlag, Sept. 1997.

    Google Scholar 

  25. T. Nipkow. Combining matching algorithms: The regular case. Journal of Symbolic Computation, pages 633–653, 1991.

    Google Scholar 

  26. G. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28:233–264, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  27. C. Ringeissen. Combining decision algorithms for matching in the union of disjoint equational theories. Information and Computation, 126(2):144–160, May 1996.

    Article  MATH  MathSciNet  Google Scholar 

  28. M. Vittek. A compiler for nondeterministic term rewriting systems. In H. Ganzinger, editor, Proceedings of RTA '96, volume 1103 of Lecture Notes in Computer Science, pages 154–168, New Brunswick (New Jersey), July 1996. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LORIA-CNRS & INRIA-Lorraine, BP 239, 54506, Vand∄uvre-lès-Nancy Cedex, France

    Pierre-Etienne Moreau & Hélène Kirchner

Authors
  1. Pierre-Etienne Moreau
    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

Editor information

Catuscia Palamidessi Hugh Glaser Karl Meinke

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Moreau, PE., Kirchner, H. (1998). A compiler for rewrite programs in associative-commutative theories. In: Palamidessi, C., Glaser, H., Meinke, K. (eds) Principles of Declarative Programming. ALP PLILP 1998 1998. Lecture Notes in Computer Science, vol 1490. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0056617

Download citation

  • DOI: https://doi.org/10.1007/BFb0056617

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65012-6

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation