Please use this identifier to cite or link to this item: doi:10.22028/D291-40186
Title: Term Orderings With Status
Author(s): Steinbach, Joachim
Language: English
Year of Publication: 1988
Place of publication: Kaiserslautern
Free key words: Homeomorphic embedding
Knuth-Bendix ordering
Lexicographical ordering
Multiset ordering
Path of subterms ordering
Recursive decomposition ordering
Recursive path ordering
Simplification ordering
Term rewriting system
Well-founded ordering
DDC notations: 004 Computer science, internet
Publikation type: Report
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.
Link to this record: urn:nbn:de:bsz:291--ds-401860
Series name: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Series volume: 88,12
Date of registration: 11-Aug-2023
Faculty: SE - Sonstige Einrichtungen
Department: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professorship: SE - Sonstige
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
SEKI-Report-SR-88-12_Steinbach_Term-Orderings-With-Status.pdf3,29 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.