×

Transformations and confluence for rewrite systems. (English) Zbl 0872.68078

Summary: Many important applications of rewrite systems, e.g., automated reasoning, algebraic specifications of abstract data types, and functional/equational programming, rely either wholly or in part on rewrite systems that are constructor-based. We study general transformations of rewrite systems that preserve confluence and normal forms. In 1985, S. Thatte [Inf. Process. Lett. 20, 83-85 (1985; Zbl 0566.68036)]showed that an orthogonal system can be transformed into an orthogonal constructor-based system that preserves normal forms up to a certain simple homomorphism. In 1988, S. Thatte [Theor. Comput. Sci. 61, 83-92 (1988; Zbl 0659.68048)]claimed that this transformation works for all semiregular (confluent+nonoverlapping) systems. We show that Thatte’s transformation fails to preserve confluence and normal forms for semiregular systems. We then introduce the concept of weak persistence and show that Thatte’s transformation is correct for all weakly persistent confluent systems. We also give some general conditions that imply weak persistence and show that this class includes as subclasses the following: left-linear, nonoverlapping systems with confluent root overlaps (generalization of orthogonal systems), nonoverlapping noetherian systems with confluent root overlaps, and the nonlinear systems with no overlaps proved confluent by J. W. Klop [Combinatory reduction systems (Mathematical Centre Tracts 127 (1980; Zbl 0446.03006)]. We show that our transformation scheme for convergent systems can also be applied to systems in which the innermost rewritingrelation is confluent. Our results indicate that persistence plays a role in arbitrary confluent systems that is analogous to the role of the no-overlaprestriction in left-linear systems; and similarly weak persistence plays a role that is analogous to that of the nonoverlapping restriction for left-linear systems.

MSC:

68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bouhoula, A.; Rusinowitch, M., Automatic case analysis in proof by induction, (Proc. Internat. Joint Conf. on Artificial Intelligence (1993))
[2] Chew, P., An improved algorithm for computing with equations, (Proc. IEEE Symp. on Foundations of Computer Science, 21 (1980)), 108-117
[3] Chew, P., Unique normal forms in term rewriting systems with repeated variables, (Proc. ACM Symp. on Theory of Computing, 13 (1981)), 7-18
[4] Dershowitz, N.; Jouannaud, J. P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), Elsevier: Elsevier Amsterdam), Ch. 6 · Zbl 0900.68283
[5] Goguen, J. A., How to prove algebraic inductive hypotheses without induction, (Proc. Conf. on Automated Deduction (1980)), 356-373 · Zbl 0438.68043
[6] Guttag, J.; Horning, J. J., The algebraic specification of abstract data types, Acta Inform., 10, 27-52 (1978) · Zbl 0369.68010
[7] Guttag, J.; Horowitz, E.; Musser, D., Abstract data types and software validation, (Information Science Research Report ISI/RR-76-48 (1976), University of Southern California) · Zbl 0387.68012
[8] Hoffmann, C. M.; O’Donnell, M. J., Programming with equations, ACM Trans. Programming Languages Systems, 4, 83-112 (1982) · Zbl 0481.68008
[9] Hudak, P., Conception, evolution, and application of functional programming languages, ACM Comput. Surveys, 21, 359-411 (1989)
[10] Huet, G.; Hullot, J.-M., Proofs by induction in equational theories with constructors, (Proc. IEEE Symp. on Foundations of Computer Science (1980)), 96-107
[11] Klop, J. W., Combinatory reduction systems, (Ph.D. Thesis (1980), Mathematisch Centrum: Mathematisch Centrum Amsterdam) · Zbl 0466.03006
[12] Laville, A., Lazy pattern matching in the ML language, (Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science (1987)) · Zbl 0636.68011
[13] Musser, D., On proving inductive properties of abstract data types, (Proc. ACM Symp. on Principles of Programming Languages (1980)), 154-162
[14] Newman, M. H.A., On theories with a cominatorial definition of equivalence, Ann. Math., 43, 223-243 (1942) · Zbl 0060.12501
[15] O’Donnell, M. J., Equational Logic as a Programming Language (1985), MIT Press: MIT Press Cambridge, MA · Zbl 0636.68004
[16] Sekar, R. C.; Pawagi, S.; Ramakrishnan, I. V., Transforming strongly sequential rewrite systems with constructors for efficient parallel execution, (Proc. Conf. on Rewriting Techniques and Applications (1989)) · Zbl 1522.68136
[17] Sekar, R. C.; Ramakrishnan, I. V., Programming with equations: a framework for lazy parallel evaluation, (Proc. Conf. on Automated Deduction (1992)) · Zbl 0803.68060
[18] Thatte, S., On the correspondence between two classes of reduction systems, Inform. Process. Lett., 20, 83-85 (1985) · Zbl 0566.68036
[19] Thatte, S., Implementing first-order rewriting with constructor systems, Theoret. Comput. Sci., 61, 83-92 (1988) · Zbl 0659.68048
[20] Verma, R. M., Equations, nonoblivious normalization, and term matching problems, (Ph.D. Thesis (1989), State University of New York: State University of New York Stony Brook)
[21] Verma, R. M., A theory of using history for equational systems with applications, (Proc. IEEE Symp. on Foundations of Computer Science (1991)), 348-357
[22] Verma, R. M.; Ramakrishnan, I. V., Nonoblivious normalization algorithms for nonlinear systems, (Proc. Internat. Coll. on Automata, Languages and Programming, 443 (1990), Springer: Springer Berlin), 370-385 · Zbl 0765.68067
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.