Decomposition Ordering as a Tool to Prove the Termination of Rewriting Systems

1. tnt reduction

In this paper, a term is a pair formed by an operator and a list of terms. In other words, no restriction exists on the arity of operators. Here are some definitions about ordering on terms. More information can be found in [1] and (4).

• An ordering on terms is monotonic if for all operators f

• It has the subterm property if

• It has the deletion property if

• A monotonic ordering which has the subterm property and the deletion property is a simplification ordering.
• An orderina is well -founded if there exists no infinite strictly decreasing sequence

Dershowitz [ 1] proved that if {Ri-+Li} is a rewriting system for which exists a simplification ordering < such that for all i and for all ground substitutions a, a(Li)<a(Ri)' then ~ is well -founded, which means no infinite sequence t 0 -->t 1 -+ ... -+tn-+ ... exists. The ~-.~stem is said to have the termination property. However, Huet and Lankford (5) showed that the termination problem for rewriting systems is undecidable; therefore no uniform method based, for instance, on orderings can exist. But proving termination of particular rewriting system is an essential problem in many areas where rewriting systems are used. In simplification systems this insures that the process will terminate. In the Knuth-Bendix method, proving termination of the system is necessary, to deduce global confluence from local confluence [7] . For example the system {A--+8, A-·C, 8--+A, 8-+D} is locally confluent but not globally confluent. If the Knuth-Bendix algorithm is used to transfcrm a set of rewrite rules into a canonical one. Huet [3) showed that uniform termination ordering is necessary for all rules which appear in the process. Several authors propose simplification orderings based on syntactical properties of terms: ordering based on weight by Knuth and Bendix (7), recursive palh of subterms ordering by Plaisted [ 1 0], recursive pnth ordering by Dershowitz [ 1 ), non-ascending property by Pettorossi [9] , generalized recursive path ordering by Kamin and Levy [6) . In this paper a new ordering called the decomposition ordering is defined. Its definition is relatively simple, it allows efficient implementation and it has interesting generalizations which are currently being worked upon. As do the other cited orderings, it derives from an ordering on operators. It is based on a decomposition of terms in three parts, on which comparisons are recursively performed. When the basic ordering is total, decomposition ordering is equivalent to the orderings proposed by Plaisted and Dcrshowitz. But their respective implementations are quite different. A comparative analysis of these methods is proposed in [8] for monadic terms. Here, only decomposition ordering on terms without variables, on a totally ordered set of operators, is given. Such an ordering can be used in simplification systems.

1. This work was supported by National Science Foundation and Centre National de Ia Recherche Scir.ntiliQue.

2. Definition of decomposition ordering

Let T(F) be the set of terms on the set F of operators. F is assumed to be totally ordered by < . The decomposition ordering is denoted -<-

s:f(s 1 , ... ,sm) is a left-weighted term if s 1 , ... ,sm are left-weighted and s 1 ::::; ... :::Ssm· where s:::St means for left-weighted that s-<t or s is equal tot.

In order to compare two terms u and v, sort the terms from leal to roots, yielding s and t. II s = t, then u and v are decomposition equivalent, which means m = n and there exists a permutation a on [1..m] such that U; is decomposition equivalent to va(i) · Otherwise compare s and t using the decomposition ordering method. In this and the following section, assume that all terms are left-weighted.

The decomposition of a left-weighted term s is the unique triple [1 5 ;s';s"(O)) such that s = s"(l 5 (s 1 ' , ... ,sP')) where s"(v) is the terms given by substituting term v in place of 0, where 1 5 is the first occurrence of the maximal operator in s on its most left branch, s'=<s 1 ', . .. ,sP'> is a sequence of terms and s"(O) is a term with a unique constant subterm denoted by the symbol 0; the set of such terms will be written T(F;O). It will be assumed that the term 0 is less than any other term.

For instance, the following term:

decomposes into [b;<b,a>;a(O,b(a))), as described by the following figure.

Note that s" (O) is not left-weighted. Except lor the first immediate subterm, the term is left-weighted; this is recursively true lor each first subterm of this term. Such terms will be called almost-left -weighted.

Definition 1: A terms of T(F;O) is almost-left -weighted iff

Note that a term is almost -left -weighted if it is left -weighted. The decomposition ordering can be given for almost-left-weighted terms of T(F;O) as follows:

Definition 2: The decomposition ordering on almost-left-weighted terms s and t is defined as:

where -<rex is the lexicographic ordering deduced from -<

3. An implementation of decomposition ordering

Using this definition, it is possible to associate with each term. a term on a heterogeneous algebra with five phyla: operator (the operators of F), triple (representing the decomposition of left-weighted terms), list (representing the list of the decompositions of the almo:;t-left-weighted terms), atmosUrlple (representing lhe decompositions of almost -left-weighted terms), almosUist (representing the list of decompositions, the first element in the list being the decomposition of an almost-left .. weighted term). Five heterogeneous operators are given:

at : (operator, almosUist, almost_triple)

af : (almost_trlple, triple·)

-+ almost_llst

It must be noticed that the two operators li and a/ are associative, which means their profile is not a tuple on phyla but any sequence having a given form: for li any sequence on triple, and lor a/ any sequence beginning by almost_triple followed by any sequence on triple. The decomposition of the term of the previous example is represented by:

The mapping associating a tree with its decomposition term is one-to-one. To compare two decomposition terms, traverse them in prefix order until the first difference appears. This first difference can occur in one of three cases.

1. The operators are different. Then the lesser operator belongs to the lesser term.
2. In the traversal , one list finished before the other one. Then the shorter list belongs to the lesser term.
3. A subterm with phylum almost_triple corresponds to 0 in one decomposition term and corresponds to a term with a root at in the other one. Then 0 belongs to the lesser term.

The structure presented is voluntarily redundant for pedagogical reasons. It could be encoded by a linear list containing only relevant information.

4. Conclusion and Perspectives

Decomposition ordering gives an easy way t~ order a pair of terms. It boils down to comparing two decomposition terms using a simple algorithm studied by Flajolet and Steyaert in their analysis of pattern matching [2]. They consider the Catalan statistics where the average performance of the algorithm i:J determined over the set of all possible shapes of decomposition terms of given sizes. They show that, before termination, this algorithm performs on the average a constant number of tests lor that statistics. In [B) we use a statistics where all terms of T(F) are equiprobable. By elementary methods, we prove that on monadic terms, the algorithm stops after approximately 1 + 1 /v + 1 /nv + t tests when one term has length 1, the other has length n and, the set F has v elements and where t is 0(n/v 2 ) as n/v -+ 0. It would be interesting to adapt Flajolet and Steyaert's method to this more natural statistics. On the other hand we are currently designing an efficient algorithm to build the decomposition term from term on T(F). Generalizations of decomposition ordering to terms with variables on partially ordered set of operators are possible, but the definitions are more complex [11 ). For instance, the concept of "left -weighted" term does not exist anymore and must be extended.

5. References

• [1) N. Dershowitz: Ordering lor Term Rewriting Systems, Proc. 20th Symposium on Foundations of Computer Science, (1979), 123-131 .
• [2) P. Flajolet, J. -M. Steyaert: On the analysis of tree-matching algorithms 7th ICALP, Lecture Notes in Computer Science 85, pp 208-219.
• G. t-luet: A complete proof of correctness of the Knuth-Bendix Completion algorithm, Rapport INRIA 25, INRIA Rocquencourt, France.
• [4) G. Huet, D.C. Oppen: Equations and Rewrite Rules: a Survey, in Formal Languages perspectives and Open Problems, Ed. Book R., Academic Press, (1980).
• G. Huet, D.S. Lankford: On the Uniform Halting Problem lor Term Rewriting Systems, Rapport Laboria 283, IRIA, Mars 197B, INRIA Rocquencourt, France.
• [6) S. Kamin, J. J. LEwy: Attempts for generalizing the Recursive Path Ordering (unpublished manuscript 1980).
• [7) D.E. Knuth, P. Bendix: Simple Word Problems in Universal Algebra, in Computational Problems in Abstract Algebra, Ed. Leech J., Pergamon Press, (1970), 263-297.
• [B) P. Lescanne: Two Implementations of Recursive Path Ordering on Monadic Terms, Centre de Recherche en lnformatique de Nancy, Nancy, France, CAIN 81-R-011.
• [9) A. Pettorossi : Comparing and putting together Recursive Path Orderings. Simplification Orderings and Non-Ascending Property for termination proofs of Term Rewriting Systems 8th Int. Coli. Automata Languages and Programming, Haifa Israel, 1981 .
• D. Plaisted: A Recursively Defined Ordering lor Proving Termination of Term Rewriting Systems, Dept of Computer Science Report 78·943, U. of Illinois at Urbana-Champaign, Sept. 1978.
• [11) F. Reinig: Decomposition Ordering: Theory and Application, Thesis in preparation, University of Nancy, France.