[Zurück]

B. Gramlich:
"Modularity of Termination of Left-Linear Rewrite Systems Revisited";
Vortrag: 7th International Workshop on Termination (WST 2004), Aachen, Germany; 01.06.2004 - 02.06.2004; in: "Proc. 7th International Workshop on Termination - Extended Abstracts (WST 2004), part of RDP 2004 (2nd Federated Conference on Rewriting, Deduction, and Programming), Aachen, Germany, June 1-2, 2004", Technische Universität Aachen, (2004), ISSN: 0935-3232; S. 22 - 25.

We investigate modularity of termination of left-linear rewrite systems in the constructor sharing case. More precisely, we study cases where both involved system are left-linear, as well as other related cases where the conditions on the involved systems systems (like left-linearity) are not the same. Several tempting approaches to generalize the well-known deep modularity results of \cite{ToKlBa89,ToKlBa95}, \cite{Ma95b,SSMaPa95} are discussed and falsified by counterexamples. By a thorough analysis of the crucial notions of uniquely collapsing and consistency w.r.t. reduction and of the role of left-linearity in collapsing and, more generally, \emph{shared symbol lifting} reductions we finally show how to generalize certain modularity results for termination in the case of disjoint unions to combinations of constructor sharing systems. The problem in the symmetric case (where both systems are left-linear) remains open, whereas we are able to extend a couple of asymmetric modularity results from \cite{Gr98} to combinations of constructor sharing systems.

http://aleph.ub.tuwien.ac.at/F?base=tuw01&func=find-c&ccl_term=AC04968658