Generalized sufficient conditions for modular termination of rewriting
type: Item
instance of: scholarly article
title: Generalized sufficient conditions for modular termination of rewriting
zbMATH Open document ID: 0810.68085
DOI: 10.1007/BF01190827
author: Bernhard Gramlich
published in: Applicable Algebra in Engineering, Communication and Computing
publication date: 1994-07-04T00:00:00Z
review text: Since rewrite systems can be seen as programs of a functional programming language, there is some interest in the following question: Given two rewrite systems \(R_ 1\) and \(R_ 2\), both having property \(P\), under which conditions does the union \(R_ 1 \cup R_ 2\) have property \(P\)? In the paper, this problem is studied for \(P\) meaning ``terminating''. This problem is nontrivial since an example of Toyama shows that \(R_ 1 \cup R_ 2\) need not be terminating even if \(R_ 1\) and \(R_ 2\) are terminating and disjoint (i.e. are defined over disjoint signatures). The property \(P\) is called modular, if \(R_ 1 \cup R_ 2\) has property \(P\) whenever \(R_ 1\) and \(R_ 2\) are disjoint and have property \(P\). It is known that termination is modular on some restricted classes of rewrite systems, e.g. on the classes of (a) non-duplicating, (b) non-collapsing, (c) left-linear and confluent, and (d) confluent overlay systems. The paper generalizes these results by classifying exactly those cases where \(R_ 1 \cup R_ 2\) is non-terminating: \(R\) is called ``termination preserving under non-deterministic collapses'' if termination of \(R\) implies termination of \(R \cup \{G(x,y) \to x\), \(G(x,y) \to y\}\), where \(G\) is a new function symbol. Now the main result of the paper is: ``If \(R_ 1\) and \(R_ 2\) are disjoint terminating rewrite systems and \(R_ 1 \cup R_ 2\) is non-terminating, then one of the systems is not termination preserving under non-deterministic collapses and the other one is collapsing''. Unfortunately, it is undecidable whether \(R\) is termination preserving under non-deterministic collapses. The main result is generalized in several directions. For example, the assumption that \(R_ 1\) and \(R_ 2\) are disjoint can be weakend to the assumption that \(R_ 1\) and \(R_ 2\) share only constructor symbols.
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 599667
zbMATH Keywords: disjoint union
zbMATH Keywords: rewrite systems
zbMATH Keywords: functional programming language
reviewed by: Jürgen Avenhaus
MaRDI profile type: Publication
cites work: A note on simplification orderings
cites work: Orderings for term-rewriting systems
cites work: Termination of rewriting
cites work: Q4385532
cites work: Q4430317
cites work: Q4246729
cites work: Q4255514
cites work: Modular term rewriting systems and the termination
cites work: Modularity of simple termination of term rewriting systems with shared constructors
cites work: Q3204048
cites work: Modular properties of conditional term rewriting systems
cites work: Completeness of combinations of constructor systems
cites work: On termination of the direct sum of term-rewriting systems
cites work: Counterexamples to termination for the direct sum of term rewriting systems
cites work: On the Church-Rosser property for the direct sum of term rewriting systems
description: scientific article; zbMATH DE number 599667