Presentation 2017-07-20
Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Intergers
Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, Tomoya Ueyama,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) In dependency pair framework for proving termination of constrained term rewriting systems, polynomial interpretations that transform dependency chains representing sequences of relevant function calls into bounded decreasing sequences of integers play an important role for the success of proving termination. In this article, we propose polynomial interpretations that transform dependency chains into bounded decreasing sequences but transform rewrite sequences of the original system into increasing sequences.We also propose polynomial interpretations that transform dependency chains into bounded increasing sequences of integers. We report empirical comparison results between the proposed polynomial interpretations.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) constrained rewriting / dependency pair framework / termination / polynomial interpretation
Paper # SS2017-17,KBSE2017-17
Date of Issue 2017-07-12 (SS, KBSE)

Conference Information
Committee SS / KBSE / IPSJ-SE
Conference Date 2017/7/19(3days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair Kazuhiro Ogata(JAIST) / Shigeo Kaneda(Doshisha Univ.)
Vice Chair Akio Nakata(Hiroshima City Univ.) / Fumihiro Kumeno(Nippon Inst. of Tech.)
Secretary Akio Nakata(Tokyo Inst. of Tech.) / Fumihiro Kumeno(Osaka Univ.) / (Kanagawa Inst. of Tech.)
Assistant Kazuyuki Shima(Hiroshima City Univ.) / Takuya Saruwatari(NTT DATA) / Kosaku Kimura(Fujitsu labs.)

Paper Information
Registration To Technical Committee on Software Science / Technical Committee on Knowledge-Based Software Engineering / Special Interest Group on Software Engineering
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Intergers
Sub Title (in English)
Keyword(1) constrained rewriting
Keyword(2) dependency pair framework
Keyword(3) termination
Keyword(4) polynomial interpretation
1st Author's Name Tomohiro Sasano
1st Author's Affiliation Nagoya University(Nagoya Univ.)
2nd Author's Name Naoki Nishida
2nd Author's Affiliation Nagoya University(Nagoya Univ.)
3rd Author's Name Masahiko Sakai
3rd Author's Affiliation Nagoya University(Nagoya Univ.)
4th Author's Name Tomoya Ueyama
4th Author's Affiliation Nagoya University(Nagoya Univ.)
Date 2017-07-20
Paper # SS2017-17,KBSE2017-17
Volume (vol) vol.117
Number (no) SS-136,KBSE-137
Page pp.pp.139-144(SS), pp.139-144(KBSE),
#Pages 6
Date of Issue 2017-07-12 (SS, KBSE)