, 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