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

Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingChapter

7 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 languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsVincent van Oostrom
PublisherSpringer Verlag
Pages40-54
Number of pages15
ISBN (Print)3540221530
DOIs
Publication statusPublished - 2004 Jan 1

Publication series

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Termination of s-expression rewriting systems: Lexicographic path ordering for higher-order terms'. Together they form a unique fingerprint.

Cite this