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.
Preview
Unable to display preview. Download preview PDF.
References
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.
D. Benanav, D. Kapur, and P. Narendran. Complexity of matching problems. Journal of Symbolic Computation, 3(1 & 2):203–216, Apr. 1987.
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.
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.
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.
J. Christian. Flatterms, discrimination nets, and fast term rewriting. Journal of Automated Reasoning, 10(1):95–113, Feb. 1993.
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.
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.
S. Eker. Associative-commutative matching via bipartite graph matching. Computer Journal, 38(5):381–399, 1995.
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.
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.
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.
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.
P. Graf. Term Indexing, volume 1053 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1996.
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.
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!
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.
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.
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.
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.
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.
W. W. McCune. Otter 3.0: Reference manual and guide. Technical Report 6, Argonne National Laboratory, 1994.
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.
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.
T. Nipkow. Combining matching algorithms: The regular case. Journal of Symbolic Computation, pages 633–653, 1991.
G. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28:233–264, 1981.
C. Ringeissen. Combining decision algorithms for matching in the union of disjoint equational theories. Information and Computation, 126(2):144–160, May 1996.
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.
Author information
Authors and Affiliations
Editor information
Rights 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