講演名 2017-07-20
制約付き項書換え系の依存鎖を上限付き整数増加列に変換する多項式解釈
笹野 智裕(名大), 西田 直樹(名大), 酒井 正彦(名大), 上山 智也(名大),
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 制約付き項書換え系の停止性証明の枠組みである依存対フレームワークでは,関数呼び出しの関係を表現した依存鎖を下限付き整数減少列に変換する多項式解釈が証明の成否を左右する重要な役割を果たす.本稿では,依存鎖を下限付き整数減少列に変換する一方で,書換え規則による書換え系列を整数増加列に変換する多項式解釈による停止性証明機能を依存対フレームワークに導入する.さらに,依存鎖を上限付き整数増加列に変換する多項式解釈による停止性証明機能を導入し,比較実験の結果を報告する.
抄録(英) 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.
キーワード(和) 制約付き書換え / 依存対フレームワーク / 停止性 / 多項式解釈
キーワード(英) constrained rewriting / dependency pair framework / termination / polynomial interpretation
資料番号 SS2017-17,KBSE2017-17
発行日 2017-07-12 (SS, KBSE)

研究会情報
研究会 SS / KBSE / IPSJ-SE
開催期間 2017/7/19(から3日開催)
開催地(和) 函館コミュニティプラザ
開催地(英)
テーマ(和) ソフトウェア工学全般/知能ソフトウェア工学全般/ソフトウェアサイエンス全般
テーマ(英)
委員長氏名(和) 緒方 和博(北陸先端大) / 金田 重郎(同志社大)
委員長氏名(英) Kazuhiro Ogata(JAIST) / Shigeo Kaneda(Doshisha Univ.)
副委員長氏名(和) 中田 明夫(広島市大) / 粂野 文洋(日本工大)
副委員長氏名(英) Akio Nakata(Hiroshima City Univ.) / Fumihiro Kumeno(Nippon Inst. of Tech.)
幹事氏名(和) 小林 隆志(東工大) / 肥後 芳樹(阪大) / 岩田 一(神奈川工科大) / 櫻井 孝平(金沢大)
幹事氏名(英) Takashi Kobayashi(Tokyo Inst. of Tech.) / Yoshiki Higo(Osaka Univ.) / Hajime Iwata(Kanagawa Inst. of Tech.) / Kohei Sakurai(Kanazawa Univ.)
幹事補佐氏名(和) 島 和之(広島市大) / 猿渡 卓也(NTTデータ) / 木村 功作(富士通研)
幹事補佐氏名(英) Kazuyuki Shima(Hiroshima City Univ.) / Takuya Saruwatari(NTT DATA) / Kosaku Kimura(Fujitsu labs.)

講演論文情報詳細
申込み研究会 Technical Committee on Software Science / Technical Committee on Knowledge-Based Software Engineering / Special Interest Group on Software Engineering
本文の言語 JPN
タイトル(和) 制約付き項書換え系の依存鎖を上限付き整数増加列に変換する多項式解釈
サブタイトル(和)
タイトル(英) Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Intergers
サブタイトル(和)
キーワード(1)(和/英) 制約付き書換え / constrained rewriting
キーワード(2)(和/英) 依存対フレームワーク / dependency pair framework
キーワード(3)(和/英) 停止性 / termination
キーワード(4)(和/英) 多項式解釈 / polynomial interpretation
第 1 著者 氏名(和/英) 笹野 智裕 / Tomohiro Sasano
第 1 著者 所属(和/英) 名古屋大学(略称:名大)
Nagoya University(略称:Nagoya Univ.)
第 2 著者 氏名(和/英) 西田 直樹 / Naoki Nishida
第 2 著者 所属(和/英) 名古屋大学(略称:名大)
Nagoya University(略称:Nagoya Univ.)
第 3 著者 氏名(和/英) 酒井 正彦 / Masahiko Sakai
第 3 著者 所属(和/英) 名古屋大学(略称:名大)
Nagoya University(略称:Nagoya Univ.)
第 4 著者 氏名(和/英) 上山 智也 / Tomoya Ueyama
第 4 著者 所属(和/英) 名古屋大学(略称:名大)
Nagoya University(略称:Nagoya Univ.)
発表年月日 2017-07-20
資料番号 SS2017-17,KBSE2017-17
巻番号(vol) vol.117
号番号(no) SS-136,KBSE-137
ページ範囲 pp.139-144(SS), pp.139-144(KBSE),
ページ数 6
発行日 2017-07-12 (SS, KBSE)