Termination proof of S-expression rewriting systems with recursive path relations

Yoshihito Toyama

研究成果: Conference contribution

2 被引用数 (Scopus)

抄録

S-expression rewriting systems were proposed by the author (RTA 2004) for termination analysis of Lisp-like untyped higher-order functional programs. This paper presents a short and direct proof for the fact that every finite S-expression rewriting system is terminating if it is compatible with a recursive path relation with status. By considering well-founded binary relations instead of well-founded orders, we give a much simpler proof than the one depending on Kruskal's tree theorem.

本文言語English
ホスト出版物のタイトルRewriting Techniques and Applications - 19th International Conference, RTA 2008, Proceedings
ページ381-391
ページ数11
DOI
出版ステータスPublished - 2008
外部発表はい
イベント19th International Conference on Rewriting Techniques and Applications, RTA 2008 - Hagenberg, Austria
継続期間: 2008 7 152008 7 17

出版物シリーズ

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

Other

Other19th International Conference on Rewriting Techniques and Applications, RTA 2008
国/地域Austria
CityHagenberg
Period08/7/1508/7/17

ASJC Scopus subject areas

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

フィンガープリント

「Termination proof of S-expression rewriting systems with recursive path relations」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル