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.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Bernhard Gramlich
URN:urn:nbn:de:hbz:386-kluedo-3208
Series (Serial Number):SEKI Report (93,9)
Document Type:Preprint
Language of publication:English
Year of Completion:1993
Year of first Publication:1993
Publishing Institution:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Tag:Term rewriting systems; combined systems with sha; confluence; disjoint union; innermost termination; modularity; termination; weak termination
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011