Abstract
We investigate termination of rewriting computations guided by strategy annotations. We show that proofs of termination can be obtained by proving(innermost) termination of context-sensitive rewriting( CSR). Hence, we investigate how to prove innermost termination of CSR usingexistingmetho ds for provingtermination of CSR.
Work partially supported by Acción Integrada Hispano-Italiana HI2000-0161, Spanish CICYT, and Conselleria de Cultura i Educació de la Generalitat Valenciana.
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
T. Arts and J. Giesl. ProvingInnermost Normalisation Automatically. In H. Comon, editor, Proc. of 8th International Conference on Rewriting Techniques and Applications, RTA’97, LNCS 1232:157–171, Springer-Verlag, Berlin, 1997.
P. Borovanskí, C. Kirchner, H. Kirchner, P.-E. Moreau, and C. Ringeissen. An Overview of ELAN. In C. Kirchner and H. Kirchner, editors, Proc. of 2nd International Workshop on Rewriting Logic and its Applications, WRLA’98, Electronic Notes in Computer Science, 15(1998):1–16, 1998.
F. Baader and T. Nipkow. Term Rewritingand All That. Cambridge University Press, 1998.
M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Proc. 1st International Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, volume 4, 25 pages, Elsevier Sciences, 1996.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69–115, 1987.
N. Dershowitz and D.A. Plaisted. Rewriting. In A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning, volume 1, chapter 9, Elsevier, 2001.
S. Eker. Term Rewritingwith Operator Evaluation Strategies. In C. Kirchner and H. Kirchner, editors, Proc. of 2nd International Workshop on Rewriting Logic and its Applications, WRLA’98, Electronic Notes in Computer Science, 15(1998):1–20, 1998.
K. Futatsugi, J. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Conference Record of the 12th Annual ACM Symposium on Principles of Programming Languages, POPL’85, pages 52–66, ACM Press, 1985.
O. Fissore, I. Gnaedig, and H. Kirchner. Termination of rewriting with local strategies. In M.P. Bonacina and B. Gramlich, editors, Proc. of 4th International Workshop on Strategies in Automated Deduction, STRATEGIES’01, pages 35–54, 2001.
K. Futatsugi and A. Nakagawa. An Overview of CAFE Specification Environment-An algebraic approach for creating, verifying, and maintainingformal specification over networks-. In Proc. of 1st International Conference on Formal Engineering Methods, 1997.
M.C.F. Ferreira and A.L. Ribeiro. Context-Sensitive AC-Rewriting. In P. Narendran and M. Rusinowitch, editors, Proc. of 10th International Conference on Rewriting Techniques and Applications, RTA’99, LNCS 1631:286–300, Springer-Verlag, Berlin, 1999.
I. Gnaedigand O. Fissore. Personal communication. July 2001.
B. Gramlich and S. Lucas editors. 1st International Workshop on Reduction Strategies in Rewriting and Programming, WRS’01. Proceedings, volume 2359, Servicio de Publicaciones de la Universidad Politécnica de Valencia, 2001. See also: volume 57 of ENTCS, Elsevier, to appear.
J. Giesl and A. Middeldorp. TransformingCon text-Sensitive Rewrite Systems. In P. Narendran and M. Rusinowitch, editors, Proc. of 10th International Conference on Rewriting Techniques and Applications, RTA’99, LNCS 1631:271–285, Springer-Verlag, Berlin, 1999.
J. Giesl and A. Middeldorp. Personal communication. May 2001.
B. Gramlich. On ProvingT ermination by Innermost Termination. In H. Ganzinger, editor, Proc. of 7th International Conference on Rewriting Techniques and Applications, RTA’96, LNCS 1103:97–107, Springer-Verlag, Berlin, 1996.
J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. In J. Goguen and G. Malcolm, editors, Software Engineering with OBJ: algebraic specification in action, Kluwer, 2000.
S. Lucas. Termination of context-sensitive rewritingb y rewriting. In F. Meyer auf der Heide and B. Monien, editors, Proc. of 23rd. International Colloquium on Automata, Languages and Programming, ICALP’96, LNCS 1099:122–133, Springer-Verlag, Berlin, 1996.
S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1):1–61, January 1998.
S. Lucas. Termination of on-demand rewritingand termination of OBJ programs. In Proc. of 3rd International Conference on Principles and Practice of Declarative Programming, PPDP’01, pages 82–93, ACMPress, 2001.
T. Nagaya. Reduction Strategies for Term Rewriting Systems. PhD Thesis, School of Information Science, Japan Advanced Institute of Science and Technology, March 1999.
M. Nakamura and K. Ogata. The evaluation strategy for head normal form with and without on-demand flags. In K. Futatsugi, editor, Proc. of 3rd International Workshop on Rewriting Logic and its Applications, WRLA’00, Electronic Notes in Theoretical Computer Science, volume 36, 17 pages, 2001.
K. Ogata and K. Futatsugi. Implementation of Term Rewritings with the Evaluation Strategy. In H. Glaser and P. Hartel, editors, Proc of 9th International Symposium on Programming Languages, Implementations, Logics and Programs, PLILP’97, LNCS 1292:225–239, Springer-Verlag, Berlin, 1997.
J. van de Pol. Operational semantics of rewritingwith priorities. Theoretical Computer Science, 200:289–312, 1998.
J. van de Pol. Just-in-time: on Strategy Annotations. In [GL01], pages 39–58.
E. Visser. A Survey of Strategies in Program Transformation Systems. In [GL01], pages 97–128.
H. Zantema. Termination of Context-Sensitive Rewriting. In H. Comon, editor, Proc. of 8th International Conference on Rewriting Techniques and Applications, RTA’97, LNCS 1232:172–186, Springer-Verlag, Berlin, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lucas, S. (2001). Termination of Rewriting with Strategy Annotations. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_46
Download citation
DOI: https://doi.org/10.1007/3-540-45653-8_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42957-9
Online ISBN: 978-3-540-45653-7
eBook Packages: Springer Book Archive