Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40427
Titel: | A Structural Analysis of Modular Termination of Term Rewriting Systems |
VerfasserIn: | Gramlich, Bernhard |
Sprache: | Englisch |
Erscheinungsjahr: | 1991 |
Erscheinungsort: | Kaiserslautern |
Freie Schlagwörter: | Term Rewriting Systems Termination Modularity |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | Modular properties of term rewriting systems, i.e. properties which are preserved under disjoint unions, have attracted an increasing attention within the last few years. Whereas confluence is modular this does not hold true in general for termination. By means of a careful analysis of potential counterexamples we prove the following abstract result. Whenever the disjoint union R1 Ꚛ R2 of two (finite) terminating term rewriting systems R1, R2 is non-terminating, then one of the systems, say R1, enjoys an interesting (undecidable) property, namely it is not termination preserving under non-deterministic collapses, i.e. R1 Ꚛ {G(x‚ y) —> x, G(x‚ y) —> y} is non-terminating, and the other system R2 is collapsing, i.e. contains a rule with a variable right hand side. This result generalizes known sufficient syntactical criteria for modular termination of rewriting. Then we develop a specialized version of the ‘increasing interpretation method’ for proving termination of combinations of term rewriting systems. This method is applied to establish modularity of termination for certain classes of term rewriting systems. In particular, termination turns out to be modular for the class of systems, for which termination can be shown by simplification orderings (this result has recently been obtained by Kurihara & Ohuchi by a similar, but less general proof technique). Moreover, we show that the weaker property of being non-self-embedding which also implies termination is not modular. We prove that the finiteness restrictions in our main results concerning the term rewriting systems involved can be considerably weakened. Furthermore, we prove that the minimal rank of potential counterexamples in disjoint unions may be arbitrarily high. Hence, a general analysis of arbitrarily complicated ‘mixed’ term seems to be necessary when modularity of termination is investigated. Finally, we show that generalizations of our main results are possible for the cases of conditional term rewriting systems as well as for some restricted form of non-disjoint combinations of term rewriting systems involving common constructors. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-404271 hdl:20.500.11880/37685 http://dx.doi.org/10.22028/D291-40427 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 91,15 |
Datum des Eintrags: | 22-Mai-2024 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Professur: | SE - Sonstige |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
SEKI-Report-SR-91-15_Gramlich_A-Structural-Analysis-of-Modular-Termination-of-Term-Rewriting-Systems.pdf | 2,68 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.