Dependency pairs for simply typed term rewriting

Takahito Aoto, Toshiyuki Yamada

Research output: Contribution to journalConference articlepeer-review

13 Citations (Scopus)


Simply typed term rewriting proposed by Yamada (RTA, 2001) is a framework of higher-order term rewriting without bound variables. In this paper, the dependency pair method of first-order term rewriting introduced by Arts and Giesl (TCS, 2000) is extended in order to show termination of simply typed term rewriting systems. Basic concepts such as dependency pairs and estimated dependency graph in the simply typed term rewriting framework are clarified. The subterm criterion introduced by Hirokawa and Middeldorp (RTA, 2004) is successfully extended to the case where terms of function type are allowed. Finally, an experimental result for a collection of simply typed term rewriting systems is presented. Our method is compared with the direct application of the first-order dependency pair method to a first-order encoding of simply typed term rewriting systems.

Original languageEnglish
Pages (from-to)120-134
Number of pages15
JournalLecture Notes in Computer Science
Publication statusPublished - 2005 Jan 1
Event16th International Conference on Term Rewriting and Applications, RTA 2005 - Nara, Japan
Duration: 2005 Apr 192005 Apr 21

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Dependency pairs for simply typed term rewriting'. Together they form a unique fingerprint.

Cite this