Termination transformation by tree lifting ordering

Takahito Aoto, Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

An extension of a modular termination result for term rewriting systems (TRSs, for short) by A. Middeldorp (1989) is presented. We intended to obtain this by adapting the dummy elimination transformation by M. C. F. Ferreira and H. Zantema (1995) under the presence of a non-collapsing non-duplicating terminating TRS whose function symbols are all to be eliminated. We propose a tree lifting ordering induced from a reduction order and a set G of function symbols, and use this ordering to transform a TRS R into R′; termination of R′ implies that of RUS for any non-collapsing non-duplicating terminating TRS S whose function symbols are contained in G, provided that for any l → r in R (1) the root symbol of r is in G whenever that of l is in G; and (2) no variable appears directly below a symbol from G in l when G contains a constant. Because of conditions (1) and (2), our technique covers only a part of the dummy elimination technique; however, even when S is empty, there are cases that our technique has an advantage over the dummy elimination technique.

Original languageEnglish
Title of host publicationRewriting Techniques and Applications - 9th International Conference, RTA 1998, Proceedings
EditorsTobias Nipkow
PublisherSpringer-Verlag
Pages256-270
Number of pages15
ISBN (Print)354064301X, 9783540643012
DOIs
Publication statusPublished - 1998 Jan 1
Event9th International Conference on Rewriting Techniques and Applications, RTA 1998 - Tsukuba, Japan
Duration: 1998 Mar 301998 Apr 1

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1379
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Conference on Rewriting Techniques and Applications, RTA 1998
CountryJapan
CityTsukuba
Period98/3/3098/4/1

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Termination transformation by tree lifting ordering'. Together they form a unique fingerprint.

  • Cite this

    Aoto, T., & Toyama, Y. (1998). Termination transformation by tree lifting ordering. In T. Nipkow (Ed.), Rewriting Techniques and Applications - 9th International Conference, RTA 1998, Proceedings (pp. 256-270). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1379). Springer-Verlag. https://doi.org/10.1007/BFb0052375