| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2017-03-10 10:45 十分完全性を持たない階層的条件付き項書換え系の合流性証明 ○黒田貴之・西田直樹・関 浩之（名大）  SS2016-77 |
|
| 抄録 | （和） | 条件付き項書換え系（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 / / / / | |
| 文献情報 | 信学技報, vol. 116, no. 512, SS2016-77, pp. 103-108, 2017年3月. | |
| 資料番号 | SS2016-77 | |
| 発行日 | 2017-03-02 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2016-77 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2017-03-09 - 2017-03-10 |
| 開催地（和） | てんぶす那覇 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2017-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 十分完全性を持たない階層的条件付き項書換え系の合流性証明 |
| サブタイトル（和） | |
| タイトル（英） | Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 条件付き項書換え系 / conditional term rewriting system |
| キーワード(2)（和/英） | 合流性 / confluence |
| キーワード(3)（和/英） | 書換え帰納法 / rewriting induction |
| キーワード(4)（和/英） | 十分完全性 / sufficient completeness |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 黒田 貴之 / Takayuki Kuroda / クロダ タカユキ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 関 浩之 / Hiroyuki Seki / セキ ヒロユキ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2017-03-10 10:45:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | SS2016-77 |
| 巻番号（vol） | vol.116 |
| 号番号（no） | no.512 |
| ページ範囲 | pp.103-108 |
| ページ数 | 6 |
| 発行日 | 2017-03-02 (SS) |
[研究会発表申込システムのトップページに戻る]