Paper Info
Title
Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms
Abstract
This paper expands the termination proof techniques based on the lexicographic path ordering to term rewriting systems over varyadic terms, in which each function symbol may have more than one arity. By removing the deletion property from the usual notion of the embedding relation, we adapt Kruskal's tree theorem to the lexicographic comparison over varyadic terms. The result presented is that finite term rewriting systems over varyadic terms are terminating whenever they are compatible with the lexicographic path order. The ordering is simple, but powerful enough to handle most of higher-order rewriting systems without A-abstraction, expressed as S-expression rewriting systems.
Year
DOI
Venue
2004
10.1007/978-3-540-25979-4_3
Lecture Notes in Computer Science
Keywords
Field
DocType
higher order
Path-ordering,Discrete mathematics,Arity,Embedding,Computer science,Algorithm,Confluence,Rewriting,Lexicographical order,Conservative extension,Kruskal's algorithm
Conference
Volume
ISSN
Citations 
3091
0302-9743
7
PageRank 
References 
Authors
0.52
9
1
Name
Order
Citations
PageRank
Yoshihito Toyama153349.60