A Path Ordering for Term Rewriting Systems with Polynomial Size Normal Forms

• ISOBE Kouki

  Application Development Department, Software Development Operations, Hitachi INS Software, Ltd.

• AOTO Takahito

  RIEC, Tohoku University

• TOYAMA Yoshihito

  RIEC, Tohoku University

Bibliographic Information

Other Title

• 多項式サイズ正規形を保証する項書き換えシステムの経路順序

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.

Journal

• Computer Software

  Computer Software 29 (1), 176-190, 2012

  Japan Society for Software Science and Technology

Details

• CRID: 1390282679713893248
• NII Article ID: 130004549256
• DOI: 10.11309/jssst.29.1_176
• ISSN: 02896540
• Data Source:
  • JaLC
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed