Normalization via Rewrite Closures
We present an abstract completion-based method for finding normal forms of terms with respect to given rewrite systems. The method uses the concept of a rewrite closure, which is a generalization of the idea of a congruence closure. Our results generalize previous results on congruence closure-based normalization methods. The description of known methods within our formalism also allows a better understanding of these procedures.
KeywordsNormal Form Inference Rule Transformation Rule Ground Term Detection Rule
Unable to display preview. Download preview PDF.
- L. Bachmair. Canonical equational proofs. Birkhäuser, Boston, 1991.Google Scholar
- L. P. Chew. An improved algorithm for computing with equations. In 21st Annual Symposium on Foundations of Computer Science, 1980.Google Scholar
- L. P. Chew. Normal forms in term rewriting systems. PhD thesis, Purdue University, 1981.Google Scholar
- N. Dershowitz and J. P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B: Formal Models and Semantics), Amsterdam, 1990. North-Holland.Google Scholar
- D. Kapur. Shostak’s congruence closure as completion. In H. Comon, editor, Proc. 8th Intl. RTA, pages 23–37, 1997. LNCS 1232, Springer, Berlin.Google Scholar
- J. W. Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, chapter 6, pages 2–116. Oxford University Press, Oxford, 1992.Google Scholar
- D. J. Sherman and N. Magnier. Factotum: Automatic and systematic sharing support for systems analyzers. In Proc. TACAS, LNCS 1384, 1998.Google Scholar
- R. M. Verma and I. V. Ramakrishnan. Nonoblivious normalization algorithms for nonlinear systems. In Proc. of the Int. Colloquium on Automata, Languages and Programming, New York, 1990. Springer-Verlag.Google Scholar