Soit s'un sous-terme de ra (éventuellement non strict) et ql E Q'. Par induction sur la taille de s', nous montrons maintenant que Norma(s' -+ ql) ç ~I implique s' -+~I ql: -si Si = ql, alors on a trivialement s ,
tel que q" f. q' alors, pqr le cas 2 de la définition de N orm, on obtient que NormO/(s' -+ Q') = {s' -+ Q'}. Puisque Normoe(s' -+ Q') ç 6 ,
en appliquant le cas 3 de la définition de Norm, on obtient que Ca) {g(a(td,··· ,a(tm)) -+ ql} ç ~I, et (b) U~=l NormO/(ti -+ a(ti» ç 6.', où Vi = 1 ... n, a{td E Qnew ç Q'. En appliquant l'hypothèse d'induction à (b), on déduit que Vi = 1. .. n, ti -+~I a(ti)' D'autre part, (a) implique que g(a(td, ... , a(tm)) -+ ~' Q' ,
,tm ) -+~I g(a(td,· .. ,a(tm )} -+~I q ,
ra -+ q) ç 6.' implique ra -+~I q, et la condition de la proposition 6.1 est satisfaite par Tn t (A) ,
arité des symboles de F est finie, si Q est fini et si l'ensemble des nouveaux états Qnew est fini, alors Q' = Qu Qnew est fini, le nombre de transition pouvant être ajoutées à 6. 1 est fini, et donc l'automate Tn t (A) est fini Comme nous ne considérons que le cas où :F et Q sont finis, afin de prouver que Tn t (A) est fini, il est suffisant de montrer que Qnew is. Dans le cas particulier de l'approximation ancêtre, ) Qnew = {1fi(r(l-+ r,q)) 1 l-+ r E R,q E QI,1 ::; i ::; Card(Pos.r(r))} ,
on obtient que Qnew = QI U Q2 où: QI ={1fi(r(l -+ r,q)) l -+ r E R,q E Q,l ::; i ::; Card ,
l ::; i ::; Card(Pos.:F(r))} sorted(nil) -> true. sorted(cons(x2, nil» -> true. sorted(cons(x2,cons(xl,x4») -> false if, pp.2-3 ,
leq(O,s(x) -> true. leq(s(x),s(y» -> Ieq(x,y) ,
append(cons(x,y),z) -> cons(x,append(y,z». rotate(null) -> null. rotate(cons(x,y» -> append(y,cons(x,null». even(null) -> true. even(cons(x,null» -> false. even(cons(xl,cons(x2,y») -> even(y). opposite(null,y) -> false. opposite(x,null) -> false. opposite(cons(xl,yl),cons(x2,y2» -> paired(xl,x2). pairedlist(null) -> true. pairedlist(cons(x,null» -> true. pairedIist(cons(xl,cons(x2,x») -> pairedIist(x) if [paired(xl,x2) = true]. pairedlist(cons(xl,cons(x2,x») -> false if [paired(xl,x2)=false] . alter(null) -> true, pp.2-3 ,
fact(s(x)) -> mult(s(x) , fact(x». fact(O) -> seO). mult(O, x) -> O. mult(s(x), y) -> plus(mult(x, y), y). pIus(x, 0) -> x. plus(x, s(y») -> s(plus(x, y). end. 7.3. Quelques systèmes de réécriture et leur preuve de terminaison Solving is successful Precedence: Car > minus, ar > fact, ar > div, tact> muIt, mult > plus, plus> s] Termination proof done in 0.42 seconds, fact(minus ,
Comme dans le cas précédent, en ajoutant les états et transitions de l'automate B, un des problèmes principaux reste d ,
Automatically proving termination where simplification orderings fail, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, pp.261-272, 1997. ,
Proving innermost normalisation automatically, Proceedings 8th Conference on Rewriting Techniques and Applications, Sitges (Spain), pp.157-171, 1997. ,
DOI : 10.1007/3-540-62950-5_68
Termination of rewriting using dependency pairs, 1997. ,
Modularity of termination using dependency pairs, Proceedings 9th Conference on Rewriting Techniques and Applications, pp.226-240, 1998. ,
DOI : 10.1007/BFb0052373
Termination by absence of infinite chains of dependency pairs, Proceedings 21st International Colloquium on Trees in Algebra and Programming, pp.196-210, 1996. ,
DOI : 10.1007/3-540-61064-2_38
Automatically proving termination and innermost normalisation of term rewriting systems, 1997. ,
Vérification automatique de programmes réactifs, 1998. ,
An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities beteween polynomial interpretations, Proceedings 8th International Conference on Automated Deduction, pp.42-51, 1986. ,
ELAN, Proceedings of the First International Workshop on Rewriting Logic, 1996. ,
DOI : 10.1016/S1571-0661(04)00032-5
URL : https://hal.archives-ouvertes.fr/inria-00098518
SPIKE, an automatic theorem prover, Proceedings of the lst International Conference on Logic Programming 201 ,
DOI : 10.1007/BFb0013087
Termination by completion, Applicable Algebra in Engineering, Communication and Computing, vol.3, issue.2, pp.79-96, 1990. ,
DOI : 10.1145/322217.322230
URL : https://hal.archives-ouvertes.fr/inria-00075384
Preuves A utomatiques par Récurrence dans les Théories Conditionnelles, Thèse de Doctorat d'Université, 1994. ,
Thee generating regular systems, Information and Control, vol.14, pp.217-231, 1969. ,
Automata with equality test, 1991. ,
Equality and disequality constraints on direct subterms in tree automata, Proceedings of the 9th Symposium on Theoretical Computer Science, pp.161-172, 1992. ,
DOI : 10.1007/3-540-55210-3_181
An Introduction to Maude (Beta Version), 1998. ,
Bottom-up tree pushdown automata and rewrite systems, Proceedings 4th Conference on Rewriting Techniques and ApplicationsCorn] H. Comon. About proofs by consistency. Invited talk at RTA'98, pp.287-298, 1991. ,
DOI : 10.1007/3-540-53904-2_104
Sufficient completeness, term rewriting system and anti-unification, Proceedings 8th International Conference on Automated Deduction, pp.128-140, 1986. ,
Solving Inequations in term algebras, Proceedings 5th IEEE Symposium on Logic in Computer Science, pp.62-69, 1990. ,
How to characterize the language of ground normal forms, Technical Report, vol.676, 1987. ,
URL : https://hal.archives-ouvertes.fr/inria-00075877
Simulation of Turing machines by a left-linear rewrite ruie, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N. C., USA), pp.109-120, 1989. ,
Orderings for term-rewriting systems. Theoretical Compute?' Science, pp.279-301, 1982. ,
Termination of rewriting, Special issue on Rewriting Techniques and Applications, pp.69-116, 1987. ,
Hierarchical termination, Proceedings 4th International Workshop on Conditional Term Rewriting Systems, pp.89-105, 1995. ,
Natural termination, Theoretical Computer Science, vol.142, issue.2, pp.179-207, 1995. ,
DOI : 10.1016/0304-3975(94)00275-4
Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pp.244-320, 1990. ,
Proving termination with multiset orderings, Communications of the ACM, vol.22, issue.8, pp.465-476, 1979. ,
DOI : 10.1145/359138.359142
1onical conditional rewrite systems, Proceedings 9th International Conference on Automated Deduction, Argonne (Ill., USA), 1988. ,
The theory of ground rewrite systems is decidable, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.242-248, 1990. ,
DOI : 10.1109/LICS.1990.113750
An incremental algorithm for proving termination of term rewriting systems, Proceedings lst Conference on Rewriting Techniques and Applications, pp.255-270, 1985. ,
T'ermination of Rewriting, 1995. ,
Reve: A term rewriting system generator with failure-resistant Knuth-Bendix, 1984. ,
A first introduction to pluss. Meteor report, LRI, 1984. ,
Reductions in tree replacement systems, Theoretical Computer Science, vol.37, pp.123-150, 1985. ,
DOI : 10.1016/0304-3975(85)90089-1
Decidable approximations of sets of descendants and sets of normal forms (extended version), 1997. ,
URL : https://hal.archives-ouvertes.fr/inria-00073364
Proving termination of sequential reduction relation using tree automata, 1997. ,
Decidable approximations of sets of descendants and sets of normal forms, Proceedings 9th Conference on Rewriting Techniques and Applications, pp.151-165, 1998. ,
Overlap closure and termination of term rewriting systems, 1989. ,
Termination proofs using gpo ordering constraints, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, pp.249-260, 1997. ,
DOI : 10.1007/BFb0030601
URL : https://hal.archives-ouvertes.fr/inria-00073604
Termination proofs using gpo ordering constraints (extended version), 1997. ,
URL : https://hal.archives-ouvertes.fr/inria-00073604
Larch: Languages and Tools for Formal Specification, 1993. ,
DOI : 10.1007/978-1-4612-2704-5
URL : http://www.ii.uib.no/~magne/i123-tekster/larchbook-1993-utdrag.ps
Generating polynomial orderings for termination proofs, Proceedings 6th Conference on Rewriting Techniques and Applications, 1995. ,
Polo -a system for termination proofs using polynomial orderings, 1995. ,
Termination of order-sorted rewriting, Proceedings 3m International Conference on Aigebraic and Logic Programming, pp.37-52, 1992. ,
Generalized sufficient conditions for modular termination of rewriting, Applicable Algebra in Engineering, Communication and Computation, vol.5, pp.131-158, 1994. ,
Termination and Confluence Properties of Structured Rewrite Systems, 1996. ,
Regular tree languages and rewrite systems, Fundamenta Informaticae, vol.24, pp.157-175, 1995. ,
URL : https://hal.archives-ouvertes.fr/inria-00538882
Introducing OBJ3, 1988. ,
On the uniform halting problem for term rewriting systems, Proof of termination of the rewriting system SUBST on CCL. Theoretical Computer Science, pp.205305-312, 1978. ,
Termination of non-simple rewrite systems, 1997. ,
Automates d'arbres et réécriture de termes, 1996. ,
Decidable approximations of term rewriting systems, Proceedings 7th Conference on Rewriting Techniques and Applications, pp.362-376, 1996. ,
On multiset orderings, Information Processing Letters, vol.15, issue.2, pp.57-63, 1982. ,
DOI : 10.1016/0020-0190(82)90107-7
Solving simplification ordering constraints ,
DOI : 10.1007/BFb0016865
Reductive conditional term rewriting systems ,
Fair conditional term rewriting systems: Unification, termination, and confluence Simplifying conditional term rewriting systems: Unification, termination and confluence, Journal of Symbolic Computation, vol.4, issue.3, pp.295-334, 1984. ,
Simple word problems in universal algebras ,
Modular term rewriting systems and the termination, Information Processing Letters, vol.34, issue.1, pp.1-4, 1990. ,
DOI : 10.1016/0020-0190(90)90221-I
Two generalizations ofthe recursive path ordering, 1980. ,
Attempts for generalizing the recursive path ordering, 1982. ,
The ASF+SDF Meta-environment User's Guide, 1993. ,
A note on recursive path ordering, Theoretical Computer Science, pp.323-328, 1985. ,
On sufficient-completeness and related properties of term rewriting systems, Acta Informatica, vol.6, issue.5, pp.395-415, 1987. ,
DOI : 10.1016/B978-0-08-012975-4.50028-X
Modular term rewriting systems with shared constructors, Journal of Information Processing of Japan, vol.14, issue.3, pp.357-358, 1991. ,
DOI : 10.1016/0304-3975(92)90015-8
URL : https://doi.org/10.1016/0304-3975(92)90015-8
Completeness in data type specifications, Proceedings EUROCAL Conference, Linz (Austria), pp.348-362, 1985. ,
Well-quasi ordering, the tree theorem and Vazsonyi's conjecture, Trans. Amer. Math. Soc, vol.95, pp.210-225, 1960. ,
Canonical algebraic simplifications, 1975. ,
On proving term rewriting systems are noetherian, 1979. ,
Computer experiments with the REVE term rewriting systems generator, Proceedings of 10th ACM Symposium on Principles of Programming Languages, pp.99-108, 1983. ,
Uniform termÏnation of term rewriting systems Recursive decomposition ordering with status A finite termÏnation criterion, Proceedings 9th Colloquium on Trees in Aigebra and Programming, pp.182-194, 1978. ,
E-unification by means of tree tuple synchronized grammars, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, pp.429-440, 1997. ,
DOI : 10.1007/BFb0030616
URL : https://hal.archives-ouvertes.fr/hal-00809528
Sour graphs for efficient completion, 1995. ,
URL : https://hal.archives-ouvertes.fr/hal-00958899
Simple termination is difficult, Applicable Aigebra in Engineering, Communication and Computation, 1994. ,
DOI : 10.1007/bf01225647
URL : http://www.score.is.tsukuba.ac.jp/~ami/research/papers/aaecc95.ps.gz
A sufficient condition for the termination of the direct sum of term rewriting systems, Proceedings 4th IEEE Symposium on Logic in Computer Science, pp.396-401, 1989. ,
Modular Properties of Term Rewriting Systems, 1990. ,
On the termination of markov algorithms, Third Hawai International Conference on System Sciences, pp.789-792, 1970. ,
Transformations de noyaux reconnaissables d'arbres ,
A choice-point library for backtrack programming, JICSLP'9S Post-Conference Workshop on Implementation Technologies for Programming Languages based on Logic, 1998. ,
ECLiPSe User Manual, ECRC, 1993. ,
On theories with a combinatorial definition of equivalence, Annals of Math, pp.223-243, 1942. ,
Simple LPO constraint solving methods, Information Processing Letters, vol.47, issue.2, 1993. ,
DOI : 10.1016/0020-0190(93)90226-Y
URL : http://www.lsi.upc.es/~roberto/papers/ipl93.ps.gz
Theorem proving with ordering constrained clauses ,
DOI : 10.1007/3-540-55602-8_186
A decidability result about sufficient-completeness of axiomatically specified abstract data types, 6th GI Conference, pp.257-268, 1983. ,
DOI : 10.1007/BFb0036486
Order-sorted termination: The unsorted way, Michael Hanus and Mario Hanus Proceedings 5th International Conference on Aigebraic and Logic Programming, pp.92-106, 1996. ,
DOI : 10.1007/3-540-61735-3_6
Modular Properties of Composable Term Rewriting Systems, 1994. ,
Polynomial time termination and constraint satisfaction tests, Proceedings 5th Conference on Rewriting Techniques and Applications, pp.405-420, 1993. ,
Modularité dans les spécifications algébriques, 1997. ,
On termination of the direct sum of term rewriting systems, Information Processing Letters, vol.26, issue.2, pp.65-70, 1987. ,
Deterministic Tree Pushdown Automata and Monadic Tree Rewriting Systems, Journal of Computer and System Sciences, vol.37, pp.367-394, 1988. ,
Check your ordering -termination proofs and open problems, 1993. ,
Extensions and comparisons of simplification orderings, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N. C., USA), pp.434-448, 1989. ,
Generating polynomial orderings, Information Processing Letters, vol.49, issue.2, pp.85-93, 1994. ,
DOI : 10.1016/0020-0190(94)90032-9
Simplification orderings: history of results, Fundamenta Informaticae, vol.24, pp.47-87, 1995. ,
Counterexamples to termination for the direct sum of term rewriting systems, Information Processing Letters, vol.25, issue.3, pp.141-143, 1986. ,
DOI : 10.1016/0020-0190(87)90122-0
On proving the termination of algorithms by machine, Artificial Intelligence, vol.71, issue.1, 1994. ,
DOI : 10.1016/0004-3702(94)90063-9
Termination of term rewriting: interpretation and type elimination, Journal of Symbolic Computation, vol.17, issue.1, pp.23-50, 1994. ,
DOI : 10.1006/jsco.1994.1003
Termination of term rewriting by semantic labelling, Fundamenta Informaticae, vol.24, pp.89-105, 1995. ,