Paper Info
Title
Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations
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.
Year
DOI
Venue
2008
10.1007/978-3-540-70590-1_26
RTA
Keywords
Field
DocType
simpler proof,tree theorem,well-founded order,finite s-expression,direct proof,termination proof,s-expression rewriting systems,recursive path relation,termination analysis,well-founded binary relation,recursive path relations,higher-order functional program,binary relation,higher order functions
S-expression,Discrete mathematics,Binary relation,Computer science,Algorithm,Termination analysis,Confluence,Rewriting,Kruskal's algorithm,Recursion,Direct proof
Conference
Volume
ISSN
Citations 
5117
0302-9743
2
PageRank 
References 
Authors
0.36
13
1
Name
Order
Citations
PageRank
Yoshihito Toyama153349.60