TY - CHAP

T1 - Termination of s-expression rewriting systems

T2 - Lexicographic path ordering for higher-order terms

AU - Toyama, Yoshihito

PY - 2004/1/1

Y1 - 2004/1/1

N2 - 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 λ-abstraction, expressed as S-expression rewriting systems.

AB - 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 λ-abstraction, expressed as S-expression rewriting systems.

UR - http://www.scopus.com/inward/record.url?scp=35048901401&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35048901401&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-25979-4_3

DO - 10.1007/978-3-540-25979-4_3

M3 - Chapter

AN - SCOPUS:35048901401

SN - 3540221530

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 40

EP - 54

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - van Oostrom, Vincent

PB - Springer Verlag

ER -