Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems

  • We investigate restricted termination and confluence properties of term rewritADing systems, in particular weak termination and innermost termination, and theirinterrelation. New criteria are provided which are sufficient for the equivalenceof innermost / weak termination and uniform termination of term rewriting sysADtems. These criteria provide interesting possibilities to infer completeness, i.e.termination plus confluence, from restricted termination and confluence properADties.Using these basic results we are also able to prove some new results aboutmodular termination of rewriting. In particular, we show that termination ismodular for some classes of innermost terminating and locally confluent termrewriting systems, namely for nonADoverlapping and even for overlay systems. Asan easy consequence this latter result also entails a simplified proof of the factthat completeness is a decomposable property of soADcalled constructor systems.Furthermore we show how to obtain similar results for even more general cases of(nonADdisjoint) combined systems with shared constructors and of certain hierarADchical combinations of systems with constructors. Interestingly, these modularityresults are obtained by means of a proof technique which itself constitutes a modADular approach.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Bernhard Gramlich
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3208
Serie (Series number):SEKI Report (93,9)
Document Type:Preprint
Language of publication:English
Year of Completion:1993
Year of Publication:1993
Publishing Institute:Technische Universität Kaiserslautern
Tag:Term rewriting systems ; combined systems with sha; confluence ; disjoint union ; innermost termination ; modularity ; termination ; weak termination
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $