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) |