Termination transformation by tree lifting ordering

Takahito Aoto, Yoshihito Toyama

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

1 Citation (Scopus)


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
Number of pages15
ISBN (Print)354064301X, 9783540643012
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)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other9th International Conference on Rewriting Techniques and Applications, RTA 1998

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this