Termination of simply typed term rewriting by translation and labelling

Takahito Aoto, Toshiyuki Yamada

Research output: Chapter in Book/Report/Conference proceedingConference contribution

13 Citations (Scopus)

Abstract

Simply typed term rewriting proposed by Yamada (RTA 2001) is a framework of term rewriting allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed term rewriting dispenses with bound variables. This paper presents a method for proving termination of simply typed term rewriting systems (STTRSs, for short). We first give a translation of STTRSs into many-sorted first-order TRSs and showthat termination problem of STTRSs is reduced to that of many-sorted first-order TRSs. Next, we introduce a labelling method which is applied to first-order TRSs obtained by the translation to facilitate termination proof of them; our labelling employs an extension of semantic labelling where terms are interpreted on a many-sorted algebra.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsRobert Nieuwenhuis
PublisherSpringer Verlag
Pages380-394
Number of pages15
ISBN (Print)3540402543, 9783540402541
DOIs
Publication statusPublished - 2003
Event14th International Conference on Rewriting Techniques and Applications, RTA 2003 - Valencia, Spain
Duration: 2003 Jun 92003 Jun 11

Publication series

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

Other

Other14th International Conference on Rewriting Techniques and Applications, RTA 2003
CountrySpain
CityValencia
Period03/6/903/6/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Termination of simply typed term rewriting by translation and labelling'. Together they form a unique fingerprint.

Cite this