Term Orderings With Status

Abstract

The effective calculation with term rewriting systems presumes termination. Orderings on terms are able to guarantee termination. This report deals with some of those term orderings : Several path and decomposition orderings and the Knuth-Bendix ordering. We pursue three aims : Firstly, known orderings will get new definitions. In the second place, new ordering methods will be introduced : We will extend existing orderings by adding the principle of status ([KL80]). Thirdly, the comparison of the power as well as the time behaviour of all orderings will be presented. More precisely, after some preliminary remarks to termination of rewrite systems we present the ordering methods. All orderings are connected by an essential characteristic : Each operator has a status that determines the order according to which the subterms are compared. We will present the following well-known orderings : The recursive path ordering with status ([KL80])‚ the path of subterms ordering ([Ru87]) and another path ordering with status ([KNS 85]). A new recursive decomposition ordering with status will lead the catalogue of orderings introduced here. It is different from that of [Le84]. Moreover, we give a new definition based on decompositions of the path of subterms ordering (see [St88a]'). An extension by incorporating status to this ordering as well as to the improved recursive decomposition ordering (cf. [Ru87]) will be a part of the paper. All orderings based on decompositions will be presented in a new and simple style : The decomposition of a term consists of terms only. The original definitions take tuples composed of three (or even four) components. Additionally to path and decomposition orderings, we deal with the weight oriented ordering ([KB70]) and incorporate status. Finally, important properties (simplification ordering, stability w.r.t. substitutions, etc.) of the newly introduced orderings will be listed. Besides the introduction of new orderings, another main point of this report is the comparison of the power of these orderings, i.e. we will compare the sets of comparable terms for each combination of two orderings. It turned out that the new version with status of the improved recursive decomposition ordering (equivalent to the path ordering with status of [KNS85]) is the most powerful ordering of the class of path and decomposition orderings presented. This ordering and the Knuth-Bendix ordering with status overlap. The orderings are implemented in our algebraic specification laboratory TRSPEC and the completion system COMTES. A series of experiments has been conducted to study the time behaviour of the orderings. An evaluation of these chronometries concludes the paper.