An improved recursive decomposition ordering for higher-order rewrite systems

Munehiro Iwami, Masahiko Sakai, Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


Simplification orderings, like the recursive path ordering and the improved recursive decomposition ordering, are widely used for proving the termination property of term rewriting systems. The improved recursive decomposition ordering is known as the most powerful simplification ordering. Recently Jouannaud and Rubio extended the recursive path ordering to higher-order rewrite systems by introducing an ordering on type structure. In this paper we extend the improved recursive decomposition ordering for proving termination of higher-order rewrite systems. The key idea of our ordering is a new concept of pseudoterminal occurrences.

Original languageEnglish
Pages (from-to)988-996
Number of pages9
JournalIEICE Transactions on Information and Systems
Issue number9
Publication statusPublished - 1998 Jan 1


  • Higher-order rewrite system
  • Pseudoterminal occurrence
  • Simplification ordering
  • Term rewriting system
  • Termination, improved recursive decomposition ordering
  • Type

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Vision and Pattern Recognition
  • Electrical and Electronic Engineering
  • Artificial Intelligence


Dive into the research topics of 'An improved recursive decomposition ordering for higher-order rewrite systems'. Together they form a unique fingerprint.

Cite this