Termination transformation by tree lifting ordering

Takahito Aoto, Yoshihito Toyama

研究成果: Conference contribution

1 被引用数 (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.

本文言語English
ホスト出版物のタイトルRewriting Techniques and Applications - 9th International Conference, RTA 1998, Proceedings
編集者Tobias Nipkow
出版社Springer-Verlag
ページ256-270
ページ数15
ISBN(印刷版)354064301X, 9783540643012
DOI
出版ステータスPublished - 1998 1 1
イベント9th International Conference on Rewriting Techniques and Applications, RTA 1998 - Tsukuba, Japan
継続期間: 1998 3 301998 4 1

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
1379
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

Other9th International Conference on Rewriting Techniques and Applications, RTA 1998
国/地域Japan
CityTsukuba
Period98/3/3098/4/1

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Termination transformation by tree lifting ordering」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル