Termination of rewriting under strategies

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Termination of rewriting under strategies

Full text

Pdf (729 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 10 , Issue 2 (February 2009) table of contents

Article No. 10

Year of Publication: 2009

ISSN:1529-3785

Authors

Isabelle Gnaedig	INRIA and LORIA, Vandoeuvre lès Nancy Cedex France
Hélène Kirchner	INRIA and LORIA, Vandoeuvre lès Nancy Cedex France

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 92, Citation Count: 2

Additional Information:

appendices and supplements abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1462179.1462182 What is a DOI?

APPENDICES and SUPPLEMENTS

Gnaedig Appendix

Online appendix to termination of rewriting under strategies. The appendix supports the information on article 10.

ABSTRACT

A termination proof method for rewriting under strategies, based on an explicit induction on the termination property, is presented and instantiated for the innermost, outermost, and local strategies. Rewriting trees are simulated by proof trees generated with an abstraction mechanism, narrowing and constraints representing sets of ground terms. Abstraction introduces variables to represent normal forms without computing them and to control the narrowing mechanism, well known to easily diverge. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. It is established that termination under strategy is equivalent to the construction of finite proof trees schematizing terminating rewriting trees. Sufficient effective conditions to ensure finiteness are studied and the method is illustrated on several examples for each specific strategy.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Alarcón, B., Gutiérrez, R., and Lucas, S. 2006. Context-Sensitive dependency pairs. In Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 4337. Springer, 297 --308.
	2	Beatriz Alarcón , Salvador Lucas, Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs, Proceedings of the 6th international symposium on Frontiers of Combining Systems, September 10-12, 2007, Liverpool, UK [doi>10.1007/978-3-540-74621-8_5]
	3	Alpuente, M., Escobar, S., and Lucas, S. 2004. Correct and complete (positive) strategy annotations for OBJ. In Proceedings of the 5th International Workshop on Rewriting Logic and its Applications. Electronic Notes In Theoretical Computer Science, vol. 71, 70--89.
	4	Thomas Arts , Jürgen Giesl, Proving Innermost Normalisation Automatically, Proceedings of the 8th International Conference on Rewriting Techniques and Applications, p.157-171, June 02-05, 1997
	5	Thomas Arts , Jürgen Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, v.236 n.1-2, p.133-178, April 6, 2000 [doi>10.1016/S0304-3975(99)00207-8]
	6	Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
	7	Barendsen, E., Bethke, I., Heering, J., Kennaway, R., Klint, P., van Oostrom, V., van Raamsdonk, F., de Vries, F.-J., and Zantema, H. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press.
	8	Ahlem Ben Cherifa , Pierre Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming, v.9 n.2, p.137-159, October 1, 1987 [doi>10.1016/0167-6423(87)90030-X]
	9	Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E., and Ringeissen, C. 1998. An Overview of ELAN. In Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, C. Kirchner and H. Kirchner, Eds. Electronic Notes in Theoretical Computer Science. Elsevier Science (North-Holland).
	10	Cristina Borralleras , Maria Ferreira , Albert Rubio, Complete Monotonic Semantic Path Orderings, Proceedings of the 17th International Conference on Automated Deduction, p.346-364, June 17-20, 2000
	11	Mark G. J. van den Brand , Arie van Deursen , Jan Heering , H. A. de Jong , Merijn de Jonge , Tobias Kuipers , Paul Klint , Leon Moonen , Pieter A. Olivier , Jeroen Scheerder , Jurgen J. Vinju , Eelco Visser , Joost Visser, The ASF+SDF Meta-environment: A Component-Based Language Development Environment, Proceedings of the 10th International Conference on Compiler Construction, p.365-370, April 02-06, 2001
	12	Cirstea, H. and Kirchner, C. 2001. The rewriting calculus — Part I and II. Logic J. Interest Group Pure App. Logics 9, 427--498.
	13	Cirstea, H., Kirchner, C., Liquori, L., and Wack, B. 2003. Rewrite strategies in the rewriting calculus. In Electronic Notes in Theoretical Computer Science, Vol. 86, B. Gramlich and S. Lucas, Eds. Elsevier.
	14	Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., and Talcott, C. 2003. The Maude 2.0 system. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications, R. Nieuwenhuis, Ed. Lecture Notes in Computer Science, vol. 2706. Springer, 76--87.
	15	Comon, H. 1991. Disunification: A survey. In Computational Logic. Essays in honor of Alan Robinson, J.-L. Lassez and G. Plotkin, Eds. The MIT press, Cambridge, MA, Chapter 9, 322--359.
	16	Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., and Tommasi, M. 1997. Tree automata techniques and applications. Release October, 1st 2002.
	17	Dershowitz, N. 1982. Orderings for term rewriting systems. Theor. Comput. Sci. 17, 279--301.
	18	Nachum Dershowitz , Charles Hoot, Natural termination, Theoretical Computer Science, v.142 n.2, p.179-207, May 15, 1995
	19	Dershowitz, N. and Jouannaud, J.-P. 1990. Handbook of Theoretical Computer Science. Vol. B. Elsevier Science (North-Holland), Chapter 6: Rewrite systems, 244--320. Also as Res. rep. 478, LRI.
	20	Dershowitz, N. and Plaisted, D. 2001. Rewriting. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier Science, Chapter 9, 535--610.
	21	Eker, S. 1998. Term rewriting with operator evaluation strategies. In Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, C. Kirchner and H. Kirchner, Eds.
	22	Fernández, M.-L., Godoy, G., and Rubio, A. 2005. Orderings for innermost termination. In Proceedings of the 16th International Conference on Rewriting Techniques and Applications, J. Giesl, Ed. Lecture Notes in Computer Science, vol. 3467. Springer, 17--31.
	23	Fissore, O. 2003. Terminaison de la réécriture sous stratégies. Ph.D. thesis, Université Henri Poincaré-Nancy I, France.
	24	Fissore, O., Gnaedig, I., and Kirchner, H. 2001. Termination of rewriting with local strategies. In Selected Papers of the 4th International Workshop on Strategies in Automated Deduction, M. P. Bonacina and B. Gramlich, Eds. Electronic Notes in Theoretical Computer Science, vol. 58. Elsevier Science (North-Holland).
	25	Olivier Fissore , Isabelle Gnaedig , Hélène Kirchner, System Presentation -- CARIBOO: An induction based proof tool for termination with strategies, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.62-73, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571164]
	26	Fissore, O., Gnaedig, I., and Kirchner, H. 2002b. Outermost ground termination. In Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications. Electronic Notes in Theoretical Computer Science, vol. 71. Elsevier Science (North-Holland).
	27	Fissore, O., Gnaedig, I., and Kirchner, H. 2002c. Outermost ground termination — Extended version. Tech. rep. A02-R-493, LORIA, Nancy, France. December.
	28	Fissore, O., Gnaedig, I., and Kirchner, H. 2003a. CARIBOO: A multi-strategy termination proof tool based on induction. In Proceedings of the 6th International Workshop on Termination, A. Rubio, Ed, 77--79.
	29	Olivier Fissore , Isabelle Gnaedig , Hélène Kirchner, Simplification and termination of strategies in rule-based languages, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.124-135, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888264]
	30	Fissore, O., Gnaedig, I., and Kirchner, H. 2004. A proof of weak termination providing the right way to terminate. In Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing. Lecture Notes in Computer Science, vol. 3407. Springer, 356--371.
	31	Fissore, O., Gnaedig, I., Kirchner, H., and Moussa, L. 2005. Cariboo, A termination proof tool for rewriting-based programming languages with strategies, version 1.1. Free GPL Licence, APP registration IDDN.FR.001.170013.001.S.P.2005.000.10600. Available at http://cariboo.loria.fr/.
	32	K. Futatsugi , A. Nakagawa, An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks, Proceedings of the 1st International Conference on Formal Engineering Methods, p.170, November 12-14, 1997
	33	Thomas Genet, Decidable Approximations of Sets of Descendants and Sets of Normal Forms, Proceedings of the 9th International Conference on Rewriting Techniques and Applications, p.151-165, March 30-April 01, 1998
	34	Jürgen Giesl , Aart Middeldorp, Transforming Context-Sensitive Rewrite Systems, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, p.271-287, July 02-04, 1999
	35	Giesl, J. and Middeldorp, A. 2003. Innermost termination of context-sensitive rewriting. In Proceedings of the 6th International Conference on Developments in Language Theory (DLT'02). Lecture Notes in Computer Science, vol. 2450. Springer, 231--244.
	36	Giesl, J., Swiderski, S., Schneider-Kamp, P., and Thiemann, R. 2006. Automated termination analysis for Haskell: From term rewriting to programming languages. In Proceedings of the 17th International Conference on Rewriting Techniques and Applications, 297--312.
	37	Giesl, J., Thiemann, R., and Schneider-Kamp, P. 2004. The dependency pair framework: Combining techniques for automated termination proofs. In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Artificial Intelligence, vol. 3452. Springer, 301--331.
	38	Giesl, J., Thiemann, R., Schneider-Kamp, P., and Falke, S. 2003. Improving dependency pairs. In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Artificial Intelligence, vol. 2850. Springer, 165 --179.
	39	Isabelle Gnaedig, Induction for positive almost sure termination, Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland [doi>10.1145/1273920.1273943]
	40	Isabelle Gnaedig , Hélène Kirchner, Computing constructor forms with non terminating rewrite programs, Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy [doi>10.1145/1140335.1140351]
	41	Gnaedig, I. and Kirchner, H. 2007. Narrowing, abstraction and constraints for proving properties of reduction relations. In Rewriting, Computation and Proof. Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, H. Comon-Lundh, et al., Eds. Lecture Notes in Computer Science, vol. 4600. Springer, 44--67.
	42	Gnaedig, I., Kirchner, H., and Genet, T. 1999. Induction for termination. Tech. rep. 99.R.338, LORIA, Nancy, France. December.
	43	Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., and Jouannaud, J. 1992. Introducing OBJ3. Tech. rep., Computer Science Laboratory, SRI International. March.
	44	Jean Goubault-Larrecq, Well-Founded Recursive Relations, Proceedings of the 15th International Workshop on Computer Science Logic, p.484-497, September 10-13, 2001
	45	Gramlich, B. 1995. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundam. Info. 24, 3--23.
	46	Bernhard Gramlich, On Proving Termination by Innermost Termination, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, p.93-107, July 27-30, 1996
	47	Kamin, S. and Lévy, J.-J. 1982. Attempts for generalizing the recursive path ordering. Inria, Rocquencourt.
	48	Kirchner, C. 2005. Strategic rewriting. Electronic. Notes in Theoretical Computer. Science, vol. 124, 2, 3--9.
	49	Kirchner, C., Kirchner, H., and Rusinowitch, M. 1990. Deduction with symbolic constraints. Revue d'Intelligence Artificielle 4, 3, 9--52. (Special issue on automatic deduction.)
	50	M. R. K. Krishna Ras, Some characteristics of strong innermost normalization, Theoretical Computer Science, v.239 n.1, p.141-164, May 17, 2000 [doi>10.1016/S0304-3975(99)00215-7]
	51	Kruskal, J. B. 1960. Well-Quasi ordering, the tree theorem and Vazsonyi's conjecture. Trans. Amer. Math. Soc. 95, 210--225.
	52	Lankford, D. S. 1979. On proving term rewriting systems are noetherian. Tech. rep., Louisiana Technical University, Mathematics Deptartment, Ruston Louisiana.
	53	Salvador Lucas, Termination of Context-Sensitive Rewriting by Rewriting, Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, p.122-133, July 08-12, 1996
	54	Salvador Lucas, Termination of on-demand rewriting and termination of OBJ programs, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.82-93, September 05-07, 2001, Florence, Italy [doi>10.1145/773184.773194]
	55	Salvador Lucas, Termination of Rewriting With Strategy Annotations, Proceedings of the Artificial Intelligence on Logic for Programming, p.669-684, December 03-07, 2001
	56	Salvador Lucas, Context-sensitive rewriting strategies, Information and Computation, v.178 n.1, p.294-343, October 10, 2002 [doi>10.1016/S0890-5401(02)93176-7]
	57	Middeldorp, A. and Hamoen, E. 1994. Completeness results for basic narrowing. Appl. Algebra Eng. Commun. and Comput. 5, 3-4, 213--253.
	58	Moreau, P.-E., Ringeissen, C., and Vittek, M. 2003. A pattern matching compiler for multiple target languages. In Proceedings of the 12th Conference on Compiler Construction, G. Hedin, Ed. Lecture Notes in Computer Science, vol. 2622. Springer, 61--76.
	59	Nakamura, M. and Ogata, K. 2000. The evaluation strategy for head normal form with and without on-demand flags. In Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications (WRLA'00), K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science, 211--227.
	60	Nguyen, Q.-H. 2001. Compact normalisation trace via lazy rewriting. In Proceedings of the 1st International Workshop on Reduction Strategies in Rewriting and Programming (WRS' 01), S. Lucas and B. Gramlich, Eds. Vol. 57. Elsevier Science Publishers (North-Holland). http://www.elsevier.com/locate/entcs/volume57.html.
	61	Sven Eric Panitz , Manfred Schmidt-Schauß, TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language, Proceedings of the 4th International Symposium on Static Analysis, p.345-360, September 08-10, 1997
	62	Plaisted, D. 1978. Well-Founded orderings for proving termination of systems of rewrite rules. Tech. rep. R-78-932, Department of Computer Science, Univesity of Illinois at Urbana Champaign. July.
	63	van Oostrom, V. and de Vrijer, R. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Chapter 9. Strategies.
	64	Eelco Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, p.357-362, May 22-24, 2001
	65	Visser, E. 2004. Program transformation with Stratego/XT: Rules, strategies, tools, and systems in StrategoXT-0.9. In Domain-Specific Program Generation, C. Lengauer et al., Eds. Lecture Notes in Computer Science, vol. 3016. Spinger, 216--238.
	66	Zantema, H. 1995. Termination of term rewriting by semantic labelling. Fundam. Inf. 24, 89--105.

CITED BY 2

	Claude Kirchner , Hélène Kirchner , Anderson Santana de Oliveira, Analysis of Rewrite-Based Access Control Policies, Electronic Notes in Theoretical Computer Science (ENTCS), 234, p.55-75, March, 2009
	Matthias Raffelsieper , Hans Zantema, A Transformational Approach to Prove Outermost Termination Automatically, Electronic Notes in Theoretical Computer Science (ENTCS), 237, p.3-21, April, 2009