A path ordering for term rewriting systems with polynomial size normal forms

Kouki Isobe, Takahito Aoto, Yoshihito Toyama

Research output: Contribution to journalArticle

Abstract

Numbers of methods have been proposed to guarantee polynomial time computability of programs represented by term rewriting systems. Marion (2003) proposes the light multiset path ordering to guarantee polynomial size normal forms and shows that in term rewriting systems which can be oriented by this ordering any term can be evaluated in polynomial time. It is also shown that any polynomial time computable function can be encoded by term rewriting systems that can be oriented by this ordering. In general, however, there are term rewriting systems whose normal forms can be evaluated in polynomial time but which can not be oriented by this ordering. Thus a more general path ordering which guarantees polynomial time normal form is preferred. In this paper, we give an extension of the light multiset path ordering so that polynomial size normal form is guaranteed for more general class of term rewriting systems.

Original languageEnglish
Pages (from-to)176-190
Number of pages15
JournalComputer Software
Volume29
Issue number1
Publication statusPublished - 2012 Mar 7

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'A path ordering for term rewriting systems with polynomial size normal forms'. Together they form a unique fingerprint.

  • Cite this

    Isobe, K., Aoto, T., & Toyama, Y. (2012). A path ordering for term rewriting systems with polynomial size normal forms. Computer Software, 29(1), 176-190.