Abstract
Term rewriting systems provide a very important computational paradigm with widespread applications. The fundamental problem in computing with term rewriting systems is normalization. Consequently, efficient algorithms for finding normal forms of given terms have been the subject of considerable research. However most known normalization algorithms are oblivious, i.e., they do not remember earlier computations and so they are likely to repeat them. In this paper, we present new nonoblivious normalization algorithms for several important classes of confluent rewrite systems. These are the first such algorithms which do not require left-linearity from the rewrite system. We devise and prove certain strong structural properties of reductions in nonlinear systems for justifying the steps in our algorithms. Two interesting consequences of our work are as follows. First, in the absence of overlaps left-linearity can be exchanged with termination for nonoblivious normalization. In analogy, note that for confluence also the same exchange holds in the absence of overlaps. Second, we have devised a new technique for proving certain strong properties of reductions in rewrite systems. This technique appears to be useful for proving other properties also.
Research supported in part by a research initiation grant from the University of Houston
Research supported in part by NSF under grant number CCR-8805734
Preview
Unable to display preview. Download preview PDF.
References
Paul Chew. An improved algorithm for computing with equations. In Proceedings of the IEEE Conference on Foundations of Computer Science, volume 21, pages 108–117, 1980.
Nachum Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69–116, 1987.
K. Futatsugi, J. Goguen, J.A. Jounnaud, and J.-P. Meseguer. Principles of OBJ2. In Proceedings of the ACM Symposium on Principles of Programming Languages, 1985.
J. Guttag, E. Horowitz, and D. Musser. Abstract data types and software validation. Information Science Research Report ISI/RR-76-48, University of Southern California, 1976.
G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797–821, 1980. Also in the 18th IEEE Symposium on Foundations of Computer Science, 1977.
J.W. Klop. Combinatory Reduction Systems. PhD thesis, Mathematisch Centrum, Amsterdam, 1980.
D.E. Knuth and P. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Oxford, Pergammon Press, 1970.
Michael J. O'Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer-Verlag, 1977.
Michael J. O'Donnell. Equational Logic as a Programming Language. MIT Press, 1985.
B.K. Rosen. Tree manipulating systems and church-rosser theorems. Journal of the Association for Computing Machinery, 20:160–187, 1973. Also in the 2nd ACM Symposium on Theory of Computing.
Rakesh M. Verma and I.V. Ramakrishnan. Nonoblivious graph reduction for declarative programs. Technical Report UH-CS-90-05, University of Houston, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Verma, R.M., Ramakrishnan, I.V. (1990). Nonoblivious normalization algorithms for nonlinear rewrite systems. In: Paterson, M.S. (eds) Automata, Languages and Programming. ICALP 1990. Lecture Notes in Computer Science, vol 443. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032045
Download citation
DOI: https://doi.org/10.1007/BFb0032045
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52826-5
Online ISBN: 978-3-540-47159-2
eBook Packages: Springer Book Archive