Context-sensitive dependency pairs, Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, vol.4337, pp.297-308, 2006. ,

Termination of innermost context-sensitive rewriting using dependency pairs, Proceedings of the 6th International Symposium on Frontiers of Combining Systems. lnai, 2007. ,

Correct and complete (positive) strategy annotations for OBJ, Proceedings of the 5th International Workshop on Rewriting Logic and its Applications. Elecronic Notes In Theoretical Computer Science, vol.71, pp.70-89, 2004. ,

Proving innermost normalisation automatically, Proceedings 8th Conference on Rewriting Techniques and Applications, vol.1232, pp.157-171, 1997. ,

Termination of term rewriting using dependency pairs, Theor. Comput. Sci, vol.236, pp.133-178, 2000. ,

Term rewriting and all that, 1998. ,

, Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.55, 2003.

Termination of rewriting systems by polynomial interpretations and its implementation, Sci. Comput. Program, vol.9, issue.2, pp.137-160, 1987. ,

Electronic Notes in Theoretical Computer Science, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, 1998. ,

Complete monotonic semantic path orderings, Proceedings of the 17th International Conference on Automated Deduction, vol.1831, pp.346-364, 2000. ,

The ASF+SDF Meta-Environment: a Component-Based Language Development Environment, Compiler Construction (CC '01, vol.2027, pp.365-370, 2001. ,

Cariboo, a termination proof tool for rewriting-based programming languages with strategies, Version 1.1. Free GPL Licence, APP registration IDDN, 2005. ,

An overview of the Cafe specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks, Proceedings of the 1st IEEE Int. Conference on Formal Engineering Methods, 1997. ,

Decidable approximations of sets of descendants and sets of normal forms, Proceedings of the 9th Conference on Rewriting Techniques and Applications, 1998. ,

URL : https://hal.archives-ouvertes.fr/inria-00098700

, Lecture Notes in Computer Science, vol.1379, pp.151-165

Transforming Context-Sensitive Rewrite Systems, Proceedings of the 10th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science, vol.1631, pp.271-285, 1999. ,

Innermost termination of context-sensitive rewriting, Proceedings of the 6th International Conference on Developments in Language Theory, vol.2450, pp.231-244, 2002. ,

Automated Termination Analysis for Haskell: From term rewriting to programming languages, Proceedings of the 17th International Conference on Rewriting Techniques and Applications, pp.297-312, 2006. ,

The dependency pair framework: Combining techniques for automated termination proofs, Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol.3452, pp.301-331, 2004. ,

Improving dependency pairs, Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol.2850, pp.165-179, 2003. ,

Induction for Positive Almost Sure Termination, Proceedings of the 9th ACMSIGPLAN International Symposium on Principles and Practice of Declarative Programming, pp.167-177, 2007. ,

URL : https://hal.archives-ouvertes.fr/inria-00182435

Computing Constructor Forms with Non Terminating Rewrite Programs, Proceedings of the 8th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming, pp.121-132, 2006. ,

URL : https://hal.archives-ouvertes.fr/inria-00112083

Narrowing, abstraction and constraints for proving properties of reduction relations, Rewriting, Computation and Proof. Essays Dedicated to JeanPierre Jouannaud on the Occasion of His 60th Birthday, vol.4600, pp.44-67, 2007. ,

URL : https://hal.archives-ouvertes.fr/inria-00182434

Induction for Termination, LORIA, 1999. ,

URL : https://hal.archives-ouvertes.fr/inria-00101056

Introducing OBJ3, 1992. ,

Well-founded recursive relations, Proceedings of the 15th International Workshop in Computer Science Logic (CSL'2001), vol.2142, 2001. ,

Abstract relations between restricted termination and confluence properties of rewrite systems, Fundamenta Informaticae, vol.24, pp.3-23, 1995. ,

DOI : 10.1007/3-540-58431-5_14

URL : http://www.logic.tuwien.ac.at/people/gramlich/papers/alp94.ps.gz

On proving termination by innermost termination, Proceedings 7th Conference on Rewriting Techniques and Applications, vol.1103, pp.93-107, 1996. ,

DOI : 10.1007/3-540-61464-8_45

URL : http://www.logic.tuwien.ac.at/people/gramlich/papers/rta96a.ps.gz

Attempts for generalizing the recursive path ordering, 1982. ,

Strategic rewriting, Electr. Notes Theor. Comput. Sci, vol.124, pp.3-9, 2005. ,

DOI : 10.1016/j.entcs.2004.11.017

URL : https://hal.archives-ouvertes.fr/inria-00107802

Deduction with symbolic constraints, vol.4, pp.9-52, 1990. ,

URL : https://hal.archives-ouvertes.fr/inria-00077103

Some characteristics of strong normalization, Theor. Comput. Sci, vol.239, pp.141-164, 2000. ,

DOI : 10.1007/bfb0014330

Well-quasi ordering, the tree theorem and Vazsonyi's conjecture, Trans. Amer. Math. Soc, vol.95, pp.210-225, 1960. ,

DOI : 10.2307/1993287

On proving term rewriting systems are noetherian, 1979. ,

Termination of context-sensitive rewriting by rewriting, Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, vol.1099, pp.122-133, 1996. ,

DOI : 10.1007/3-540-61440-0_122

Termination of on-demand rewriting and termination of OBJ programs, Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp.82-93, 2001. ,

Termination of rewriting with strategy annotations, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol.2250, pp.669-684, 2001. ,

DOI : 10.1007/3-540-45653-8_46

URL : http://www.dsic.upv.es/users/elp/berlanga/slucas/lpar01/lpar01.ps.gz

Context-sensitive rewriting strategies, Inf. Comput, vol.178, pp.294-343, 2002. ,

DOI : 10.1016/s0890-5401(02)93176-7

Completeness results for basic narrowing, Applicable Algebra in Engineering, Communication and Computation, vol.5, pp.213-253, 1994. ,

DOI : 10.1007/bf01190830

URL : http://www.score.is.tsukuba.ac.jp/~ami/research/papers/aaecc94.ps.gz

A Pattern Matching Compiler for Multiple Target Languages, Proceedings of the 12th Conference on Compiler Construction, vol.2622, pp.61-76, 2003. ,

URL : https://hal.archives-ouvertes.fr/inria-00099644

The evaluation strategy for head normal form with and without on-demand flags, Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, WRLA'2000, K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science, Kanazawa City Cultural Halt, pp.211-227, 2000. ,

DOI : 10.1016/s1571-0661(05)80143-4

URL : https://doi.org/10.1016/s1571-0661(05)80143-4

Compact normalisation trace via lazy rewriting, Proceedings of the 1st International Workshop on Reduction Strategies in Rewriting and Programming, vol.57, 2001. ,

DOI : 10.1016/s1571-0661(04)00269-5

URL : https://hal.archives-ouvertes.fr/inria-00107874

TEA: Automatically proving termination of programs in a non-strict higher-order functional language, Proceedings of Static Analysis Symposium'97, vol.1302, pp.345-360, 1997. ,

Well-founded orderings for proving termination of systems of rewrite rules, 1978. ,

Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol.55, 2003. ,

Stratego: A Language for Program Transformation based on Rewriting Strategies. System Description for Stratego 0.5, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, vol.2051, pp.357-361, 2001. ,

DOI : 10.1007/3-540-45127-7_27

URL : http://archive.cs.uu.nl/pub/RUU/CS/techreps/CS-2001/2001-28.pdf

Program transformation with Stratego/XT: Rules, strategies, tools, and systems in StrategoXT-0.9, Lecture Notes in Computer Science, vol.3016, pp.216-238, 2004. ,

DOI : 10.1007/978-3-540-25935-0_13

Termination of term rewriting by semantic labelling, Fundamenta Informaticae, vol.24, pp.89-105, 1995. ,

, Since ? 0 is more general than µ, there exists a substitution ? such that ?? 0 = such that Var (r) ? Var (l), therefore we have Var (? 0 (s[r] p )) ? Var

, = (Var (s) ?Dom(? 0 )) ? Ran(? 0Var (s) ); by hypothesis, Var (s) ? Y. Moreover, since Ran(? 0Var (s) ) ? Ran(? 0 ), we have Var (? 0 (s)) ? (Y ? Dom(? 0 )) ? Ran(? 0 ), according to Proposition A.1, we have Var (? 0 (s))

, Since Var (s) ? Y, we get µs = ?s. Likewise, by hypothesis we have Dom(?) ? Y, Var (r) ? Var (l) and Y ?Var (l) = ?, then we get V ar(r) ? Dom(?) = ?, and then we have µ = ?, From Dom(?) ? Y 1 and V ar(s ) ? Y 1 , we infer Dom(?) ? V ar(s ) ? Y 1. Let us now prove that ?s = t. ?s = µs

, Proposition A.2 (with the notations A for Y 1 , B for Y, µ for ?, ? for ? now suppose

On Dom(?) ? Dom(? i ) ? (Dom(?) ? Dom(? i )), either ? = Id, or ? i = Id, so ?? i = ? i ?. As a consequence, ?(s) = ? i ?(s) = ? i ?? 0 (s) = ?? i ? 0 (s) is reducible at position p with the rule l , which is impossible by definition of reducibility of ?(s) at position p under the strategy S. So the ground substitution ? satisfies i?[1..k] ? i for all By abstraction (resp. narrowing) Lemma, applying Abstract (resp. Narrow), for each reducible ?t in G, there exists a ?t (resp. ? i t i ) in G and such that S-termination of ?t (resp. of the ? i t i ) implies S-termination of ?t. When the inference rule Stop applies on ({t}, A, C):-either A is satisfiable, in which case, by stopping lemma, every term of G = {?t | ? satisfies A} is S-terminating,-or A is unsatisfiable. In this case, G is empty. By emptiness lemma, all previous nodes on the branch correspond to empty sets G i , until an ancestor node, so ?? i = ?. Moreover, as ? is a ground substitution, ? i ? = ?. Thus, ?? i = ? i ? ,

x m ) with g ? D, and any ground instance ?. If f is a constructor, either it is a constant, which is irreducible, by hypothesis, and then S-terminating, or we consider the pattern f (x 1 ,. .. , x m ). The proof then works like in the case of defined symbols, but with only two proof steps, namely abstract and stop. Indeed, f (x 1 ,. .. , x m ) always abstracts into f (x 1, As the process is initialized with {t ref } and a constraint problem satisfiable by any ground substitution, we get that g(?x 1 ,. .. , ?x m ) is S-terminating, for any t ref = g(x 1 ,

, As Ran(? 0 ) only contains fresh variables, we have V ar(A)?Ran(? 0 ) = ?, so V ar(A) \ Ran(? 0 ) = V ar(A), More precisely, on Ran(? 0 ), ? is such that ?? 0 = ? and on V ar(A) \ Ran(? 0 ), ? = ?

u m ) ; ,?i v i for i ? [1..l] and A ? ? i is unsatisfiable for each i, or for i, For any ? satisfying A,-either ?f (u 1 ,. .. , u m ) is irreducible at the top position, but may be reduced at positions i 1 ,

, Thus, as ? satisfies A, ? satisfies A = A ? ( l i=1 ? i ).-or ?f, u m ) is reducible at the top position, and by Lifting Lemma, there is a term v and substitutions ? and ? 0 corresponding to each rewriting step ?f

, steps are effectively produced by Narrow, which is applied in all possible ways on f (u 1 ,. .. , u m ) at the top position. So a term ?v is produced for every LS-rewriting step applying on ?t at the top position. Then termination of the ?v implies termination of ?t for the given LS-strategy. We prove that ? satisfies A ? ? 0 like in the innermost case

, Then, whatever g symbol of t, either g = f and then Rls(g) ? U(t), or g is a symbol occurring in some u i and, U(u i ) ? l?r?Rls(f ) U(r)

, Let R be a rewrite system on a set F of symbols and t ? T

, By definition of U(t), since Var (t) ? X = ?, among all recursive applications of the definition of U in U(t), there is an application U(t ) of U to some term t such that U(t ) = Rls(g) ? i U(t | i ) ? l ?r ?Rls(g) U(r ), Proof. According to the definition of the usable rules, if a term t is such that Var (t) ? X = ?, then U(t) = R, and then the property is trivially true

, Since l ? r ? Rls(g), by definition of U(t ), we have U(r) ? ? l ?r ?Rls(g) U(r ), and then U(r) ? U(t ) ? U(t)

For any ground normalized substitution ? and any rewrite chain ?t ? p1, Let R be a rewrite system on a set F of symbols and t ? T ,

, Let f be the redex symbol of t 1 at a position p, and let us show that f comes either from t or from r 1. Since t 1 = ?t[?r 1 ] p1 , either p is a position of the context ?t[] p1 , which does not change by rewriting, so we already have f as redex symbol of ?t at position p. As ? is normalized, p is a position of t, so f is a symbol of t. Either p corresponds in t 1 to a non variable position of r 1 , so f is a symbol of r 1. Or p corresponds in t 1 to a position p 2 in ?x, for a variable x ? Var (r 1 ) at position q in r 1 : we have p = p 1 qp 2, The property is obviously true for an empty derivation i.e. on ?t. Let us show the property for the first rewriting step ?t ? p1,l1?r1 t 1. By definition of rewriting, ?? : ?l 1 = ?t| p1 and t 1 = ?t

, As ? is normalized, p is a position of t, so f is a symbol of t. Then, let us suppose the property true for any term of the rewrite chain ?t ? p1,l1?r1 t 1 ?. .. ? p k ,l k ?r k t k , i.e. any redex symbol f of t k is also a symbol of t, or a symbol of one of the r i , i ? [1..k], and let us consider t k ? p k+1 ,l k+1 ?r k+1 t k+1. By a similar reasoning than previously, we establish that any redex symbol f of t k+1 is also a symbol of t k , or a symbol of r k+1, Moreover, as p is a redex position in t 1 , then by definition of the innermost strategy, there is no suffix redex position of p in t 1. As t 1 | p = ?t| p , then similarly p is a redex position in ?t

For any ground instance ?t of t and any rewrite chain ?t ? p1, Lemma 6.2. Let R be a rewrite system on a set F of symbols and t ? T ,

, We then consider in the following that t ? T (F, X A ), and then that ? is a (ground) normalized substitution. We proceed by induction on T (F, X A ) and on the length of the derivation. The property is trivially true if ?t is in normal form, If a variable x ? X occurs in t, then U(t) = R and the property is trivially true

Let us now suppose the property is true for any derivation chain starting from ?t whose length is less or equal to k, and consider the chain: ?t ? p1, pp.2-2 ,

3 with a derivation of length k, we have two cases:-either the symbol f at position p k+1 in t k is a symbol of t; then, thanks to Lemma C.1 on t, we get Rls(f ) ? U(t) ,

, Moreover, since ? satisfies A i , then it satisfies in particular A i?1. Then, by induction hypothesis, ?t ref ?x and, since ? satisfies x = x , we also have ?t ref ?x

, Since ?t ref ?x , we have ?t ref ?C[z] and then, by subterm property, ?t ref ?z. Or z ? Var (t i?1 ) ; by the same reasoning as in the previous point for x, Then, as ? satisfies A i , ? is such that ?x = ?C