Termination of s-expression rewriting systems: Lexicographic path ordering for higher-order terms

Yoshihito Toyama

doi:10.1007/978-3-540-25979-4_3

Termination of s-expression rewriting systems: Lexicographic path ordering for higher-order terms

Yoshihito Toyama

Systems & Software Division

Research output: Chapter in Book/Report/Conference proceeding › Chapter

11 Citations (Scopus)

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

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Vincent van Oostrom
Publisher	Springer Verlag
Pages	40-54
Number of pages	15
ISBN (Print)	3540221530
DOIs	https://doi.org/10.1007/978-3-540-25979-4_3
Publication status	Published - 2004 Jan 1

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3091
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

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

Cite this

Toyama, Y. (2004). Termination of s-expression rewriting systems: Lexicographic path ordering for higher-order terms. In V. van Oostrom (Ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 40-54). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3091). Springer Verlag. https://doi.org/10.1007/978-3-540-25979-4_3

Termination of s-expression rewriting systems: Lexicographic path ordering for higher-order terms. / Toyama, Yoshihito.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Vincent van Oostrom. Springer Verlag, 2004. p. 40-54 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3091).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Toyama, Y 2004, Termination of s-expression rewriting systems: Lexicographic path ordering for higher-order terms. in V van Oostrom (ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3091, Springer Verlag, pp. 40-54. https://doi.org/10.1007/978-3-540-25979-4_3

Toyama Y. Termination of s-expression rewriting systems: Lexicographic path ordering for higher-order terms. In van Oostrom V, editor, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2004. p. 40-54. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-25979-4_3

Toyama, Yoshihito. / Termination of s-expression rewriting systems : Lexicographic path ordering for higher-order terms. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Vincent van Oostrom. Springer Verlag, 2004. pp. 40-54 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{431599935f13460aa5496baf3a2d74d8,

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

author = "Yoshihito Toyama",

year = "2004",

month = jan,

day = "1",

doi = "10.1007/978-3-540-25979-4_3",

language = "English",

isbn = "3540221530",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "40--54",

editor = "{van Oostrom}, Vincent",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

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 -

Termination of s-expression rewriting systems: Lexicographic path ordering for higher-order terms

Abstract

Publication series

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this