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

Yoshihito Toyama

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

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationRewriting Techniques and Applications - 19th International Conference, RTA 2008, Proceedings
Pages381-391
Number of pages11
DOIs
Publication statusPublished - 2008 Aug 13
Event19th International Conference on Rewriting Techniques and Applications, RTA 2008 - Hagenberg, Austria
Duration: 2008 Jul 152008 Jul 17

Publication series

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

Other

Other19th International Conference on Rewriting Techniques and Applications, RTA 2008
CountryAustria
CityHagenberg
Period08/7/1508/7/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Termination proof of S-expression rewriting systems with recursive path relations'. Together they form a unique fingerprint.

Cite this