On the Combination of Congruence Closure and Completion - Artificial Intelligence and Symbolic Computation - page 116

7 Conclusion and Future Work

We have presented a new graph-based method for constructing a congruence clo-
sure of a given set of ground equalities. The method combines the key ideas of
two approaches, completion and standard congruence closure, in a natural way
by relying on a data structure, called “SER graphs,” that represents a special-
ized and optimized version of the more general, but less e cient, SOUR-graphs.
We believe that our approach allows for e cient implementations and a visual
presentation that better illuminates the basic ideas underlying the construction
of congruence closures. In particular it clarifies the role of original and extended
signatures and the impact of rewrite techniques for ordering equalities. Our ap-
proach should therefore be suitable for educational purposes.
A first implementation of our method is available. The method we described
processes all equalities at once during construction of the initial graph. It is rel-
atively straightforward to devise a more flexible, incremental approach, in which
equalities are processed one at a time. Once the first equality is represented by a
graph, transformation rules are applied until a “partial” congruence closure has
been obtained. Then the next equation is processed by extending the current
graph to represent any new subterms, followed by another round of graph trans-
formations. This process continues until all equations have been processed. An
advantage of the incremental approach is that simplifying graph transformations
can be applied earlier. We expect to make implementations of both incremental
and non-incremental available.

Acknowledgments

The authors would like to thank Eugene Kipnis, student at Pace University for
the implementation of the work presented in this article, and the anonymous
reviewers for their comments.

References

1. Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press
(1998).
2. Bachmair, L., Ramakrishnan, I.V., Tiwari, A., Vigneron, L.: Congruence Clo-
sure Modulo Associativity and Commutativity. 3rd Intl Workshop FroCoS 2000,
Kirchner, H. and Ringeissen, C. Editors, Lecture Notes in Artificial Intelligence,
Springer-Verlag, 1794 (2000) 245-259.
3. Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. of Auto-
mated Reasoning, Kluwer Academic Publishers 31(2) (2003) 129-168.
4. Dershowitz, N., Jouannaud, J.-P.: Handbook of Theoretical Computer Science,
Chapter 6: Rewrite Systems. Elsevier Science Publishers B (1990) 244-320.
5. Downey, P. J., Sethi, R.,Tarjan, R. E.: Variations on the common subexpression
problem. Journal of the ACM 27(4) (1980) 758-771.
6. Kapur, D.L: Shostak's congruence closure as completion. Proceedings of the 8th
International Conference on Rewriting Techniques and Applications, H. Comon
Editor, Lecture Notes in Computer Science, Springer-Verlag 1232 (1997).