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. © 2008 Springer-Verlag.
CITATION STYLE
Toyama, Y. (2008). Termination proof of S-expression rewriting systems with recursive path relations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5117 LNCS, pp. 381–391). https://doi.org/10.1007/978-3-540-70590-1_26
Mendeley helps you to discover research relevant for your work.