Abstract
Context-sensitive rewriting was introduced in [7] and consists of syntactical restrictions imposed on a Term Rewriting System indicating how reductions can be performed. So context-sensitive rewriting is a restriction of the usual rewrite relation which reduces the reduction space and allows for a finer control of the reductions of a term. In this paper we extend the concept of context-sensitive rewriting to the framework rewriting modulo an associative-commutative theory in two ways: by restricting reductions and restricting AC-steps, and we then study this new relation with respect to the property of termination.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243–320. Elsevier, 1990.
M. C. F. Ferreira and A. L. Ribeiro. Context-sensitive AC-rewriting (extended version). Draft, 1999.
J.-P. Jouannaud and M. Muñoz. Termination of a set of rules modulo a set of equations. In Proc. of the 7th Int. Conf. on Automated Deduction, volume 170 of LNCS, pages 175–193. Springer, 1984.
J. W. Klop. Term rewriting systems. In Handbook of Logic in Computer Science, volume II, pages 1–116. Oxford University Press, 1992.
D. S. Lankford. Canonical inference. Technical Report Memo ATP-36, Automatic Theorem Proving Project, University of Texas, Austin, 1975.
S. Lucas. Context-sensitive computations in functional and functional logic programs. The Journal of Functional and Logic Programming, 1998(1):1–61.
S. Lucas. Fundamentals of context-sensitive rewriting. In Proc. of the XXII Seminar on Current Trends in Theory and Practice of Informatics, SOFSEM’95, volume 1012 of LNCS, pages 405–412. Springer, 1995.
S. Lucas. Context-sensitive computations in confluent programs. In Proc. of the 8th Int. Symposium PLILP’96-Programming Languages: Implementations, Logics, and Programs, volume 1140 of LNCS, pages 408–422. Springer, 1996.
S. Lucas. Termination of context-sensitive rewriting by rewriting. In Proc. of the 23rd Int. Colloquium on Automata, Languages and Programming, ICALP96, volume 1099 of LNCS, pages 122–133. Springer, 1996.
S. Lucas. Reescritura con Restricciones de Reemplazamiento. PhD thesis, Universidad Politecnica de Valencia, October 1998. In Spanish.
Z. Manna and S. Ness. On the termination of Markov algorithms. In Proc. of the 3rd Hawaii Int. Conf. on System Science, pages 789–792, Honolulu, 1970.
G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28:233–264, 1981.
D. A. Plaisted. Equational reasoning and term rewriting systems. In Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, pages 273–364. Oxford Science Publications, Clarendon Press-Oxford, 1993.
A. Rubio. A fully syntactic AC-RPO. In this volume.
H. Zantema. Termination of context-sensitive rewriting. In Proc. of the 8th Int. Conf. on Rewriting Techniques and Applications, RTA’97, Lecture Notes in Computer Science. Springer, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferreira, M.C.F., Ribeiro, A.L. (1999). Context-Sensitive AC-rewriting. In: Narendran, P., Rusinowitch, M. (eds) Rewriting Techniques and Applications. RTA 1999. Lecture Notes in Computer Science, vol 1631. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48685-2_24
Download citation
DOI: https://doi.org/10.1007/3-540-48685-2_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66201-3
Online ISBN: 978-3-540-48685-5
eBook Packages: Springer Book Archive