| 講演名 | 2017-03-10 十分完全性を持たない階層的条件付き項書換え系の合流性証明 黒田 貴之(名大), 西田 直樹(名大), 関 浩之(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 条件付き項書換え系（CTRS）における合流性の検証手法として項書換え系への変換を経て証明する手法が知られているが，自然数リストの並び替えを行うCTRSの合流性は証明できていない．このCTRSは関数記号の振舞いが階層的に定義される階層的CTRSとなっており，十分完全性を持っていない．本稿では，十分完全性を持たない階層的CTRSの合流性を証明する手法を提案する．具体的には，条件付き等式に対する書換え帰納法を十分完全性を持たないTRSに拡張し，書換え帰納法を用いて条件付き危険対の条件から別の条件を導出することでその危険対が会同可能であることを示す．次に，書換え規則の条件部が成立することを考慮できる単純化順序を設計し，その単純化順序により階層的CTRSの停止性を証明する手法を提案する． |
| 抄録(英) | A transformational approach to confluence proofs for conditional term rewriting systems (CTRS) has been investigated, but confluence of a CTRS defining sorting over natural numbers has not been proved yet by any existing confluence prover. Such a CTRS defines behavior of function symbols hierarchically, called a hierarchical CTRS, and is not sufficiently complete. In this article, we propose a method to prove confluence of hierarchical CTRSs that are not sufficiently complete. More precisely, we first extend rewriting induction for conditional equations to TRSs that are not sufficiently complete, and then we prove joinability of a conditional critical pair by inducing other conditions from the original conditional part. Next, we design a simplification order that takes conditional parts of rewrite rules into account, and propose a method to prove termination of hierarchical CTRSs by means of the designed simplification order. |
| キーワード(和) | 条件付き項書換え系 / 合流性 / 書換え帰納法 / 十分完全性 |
| キーワード(英) | conditional term rewriting system / confluence / rewriting induction / sufficient completeness |
| 資料番号 | SS2016-77 |
| 発行日 | 2017-03-02 (SS) |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2017/3/9(から2日開催) |
| 開催地（和） | てんぶす那覇 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 委員長氏名（和） | 緒方 和博(北陸先端大) |
| 委員長氏名（英） | Kazuhiro Ogata(JAIST) |
| 副委員長氏名（和） | 中田 明夫(広島市大) |
| 副委員長氏名（英） | Akio Nakata(Hiroshima City Univ.) |
| 幹事氏名（和） | 小林 隆志(東工大) / 肥後 芳樹(阪大) |
| 幹事氏名（英） | Takashi Kobayashi(Tokyo Inst. of Tech.) / Yoshiki Higo(Osaka Univ.) |
| 幹事補佐氏名（和） | 島 和之(広島市大) |
| 幹事補佐氏名（英） | Kazuyuki Shima(Hiroshima City Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Software Science |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 十分完全性を持たない階層的条件付き項書換え系の合流性証明 |
| サブタイトル（和） | |
| タイトル（英） | Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 条件付き項書換え系 / conditional term rewriting system |
| キーワード(2)（和/英） | 合流性 / confluence |
| キーワード(3)（和/英） | 書換え帰納法 / rewriting induction |
| キーワード(4)（和/英） | 十分完全性 / sufficient completeness |
| 第 1 著者 氏名（和/英） | 黒田 貴之 / Takayuki Kuroda |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 2 著者 氏名（和/英） | 西田 直樹 / Naoki Nishida |
| 第 2 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 3 著者 氏名（和/英） | 関 浩之 / Hiroyuki Seki |
| 第 3 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 発表年月日 | 2017-03-10 |
| 資料番号 | SS2016-77 |
| 巻番号（vol） | vol.116 |
| 号番号（no） | SS-512 |
| ページ範囲 | pp.103-108(SS), |
| ページ数 | 6 |
| 発行日 | 2017-03-02 (SS) |