講演名 | 1998/11/20 切り落とし法に基づく項書換え系の停止性判定 草刈 圭一朗, 外山 芳人, |
---|---|
PDFダウンロードページ | PDFダウンロードページへ |
抄録(和) | ArtsとGieslは依存対の概念の導入により項書き換え系の停止性を証明するための効果的な手法を開発した.この手法においては, 弱書き換え順序が重要な役割をなす.本研究では, 従来より研究されている書き換え順序を用いて弱書き換え順序を容易に設計できる切り落とし法を提案する.また, この切り落とし法を用いて停止性証明のための変換手法の一つである置換消去法に簡単な証明を与えるとともに, より一般的な変換手法を提案する. |
抄録(英) | Arts and Giesl introduced the notion of dependency paris, which gives an effective method for proving termination of term rewriting systems. In this method a weak reduction order plays an important role. In this paper, we introduce a pruning method, which makes a weak reduction order of an arbitrary reduction order. Furthermore, this method gives a simplified proof of the dummy elimination, which is one of the transformation methods for proving termination, and proposes a more generalized transformation. |
キーワード(和) | 項書換え系 / 停止性 / 依存対 / 弱書き換え順序 / 切り落とし法 |
キーワード(英) | Term Rewriting System / Termination / Dependency Pair / Weak Reduction Order / Pruning Method |
資料番号 | COMP98-57 |
発行日 |
研究会情報 | |
研究会 | COMP |
---|---|
開催期間 | 1998/11/20(から1日開催) |
開催地(和) | |
開催地(英) | |
テーマ(和) | |
テーマ(英) | |
委員長氏名(和) | |
委員長氏名(英) | |
副委員長氏名(和) | |
副委員長氏名(英) | |
幹事氏名(和) | |
幹事氏名(英) | |
幹事補佐氏名(和) | |
幹事補佐氏名(英) |
講演論文情報詳細 | |
申込み研究会 | Theoretical Foundations of Computing (COMP) |
---|---|
本文の言語 | ENG |
タイトル(和) | 切り落とし法に基づく項書換え系の停止性判定 |
サブタイトル(和) | |
タイトル(英) | On Proving Termination of Term Rewriting Systems by Pruning Method |
サブタイトル(和) | |
キーワード(1)(和/英) | 項書換え系 / Term Rewriting System |
キーワード(2)(和/英) | 停止性 / Termination |
キーワード(3)(和/英) | 依存対 / Dependency Pair |
キーワード(4)(和/英) | 弱書き換え順序 / Weak Reduction Order |
キーワード(5)(和/英) | 切り落とし法 / Pruning Method |
第 1 著者 氏名(和/英) | 草刈 圭一朗 / Keiichirou Kusakari |
第 1 著者 所属(和/英) | 北陸先端科学技術大学院大学 情報科学研究科 School of Information Science, JAIST |
第 2 著者 氏名(和/英) | 外山 芳人 / Yoshihito Toyama |
第 2 著者 所属(和/英) | 北陸先端科学技術大学院大学 情報科学研究科 School of Information Science, JAIST |
発表年月日 | 1998/11/20 |
資料番号 | COMP98-57 |
巻番号(vol) | vol.98 |
号番号(no) | 432 |
ページ範囲 | pp.- |
ページ数 | 8 |
発行日 |