| 講演名 | 1997/1/24 高階項書換え系における改良再帰分解順序について 岩見 宗弘, 酒井 正彦, 外山 芳人, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 項書換え系の停止性を証明する方法としては, 単純化順序による方法が広く用いられている。再帰経路順序, 改良再帰分解順序などの現在知られている単純化順序のうちで, 改良再帰分解順序は, 最も比較力が強い順序の一つである。一方, 高階項書換え系への拡張に関しては, 近年J.-P. Jouannaud と A. Rubio により再帰経路順序に型の情報を取り入れた方法が提案された. 本論文では, 高階項書換え系の停止性の証明に用いるために, 改良再帰分解順序を拡張する。本方法では擬終端の概念を新しく導入することにより、代入に関する安定性を保証している。 |
| 抄録(英) | Simplification orderings, like the recursive path ordering and the improved recursive decomposition ordering, are widely used for proving the termination property of term rewriting systems. The improved recursive decomposition ordering is among the most powerful simplification orderings. Recently J.-P. Jouannaud and A. Rubio extended the recursive path ordering to higher-order rewrite systems by introducing an ordering on type structure. In this paper we extend the improved recursive decomposition ordering for proving termination of higher-order rewrite systems. The key idea of our ordering is a new concept of pseudo-terminal occurrences. |
| キーワード(和) | 高階項書換え系 / 停止性 / 改良再帰分解順序 / 擬終端 / 型 / 単純化順序 |
| キーワード(英) | higher-order rewrite system / termination / improved recursive decomposition ordering / Pseudo-terminal occurrence / type / simplification ordering |
| 資料番号 | COMP96-73 |
| 発行日 |
| 研究会情報 | |
| 研究会 | COMP |
|---|---|
| 開催期間 | 1997/1/24(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Theoretical Foundations of Computing (COMP) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | 高階項書換え系における改良再帰分解順序について |
| サブタイトル（和） | |
| タイトル（英） | An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 高階項書換え系 / higher-order rewrite system |
| キーワード(2)（和/英） | 停止性 / termination |
| キーワード(3)（和/英） | 改良再帰分解順序 / improved recursive decomposition ordering |
| キーワード(4)（和/英） | 擬終端 / Pseudo-terminal occurrence |
| キーワード(5)（和/英） | 型 / type |
| キーワード(6)（和/英） | 単純化順序 / simplification ordering |
| 第 1 著者 氏名（和/英） | 岩見 宗弘 / Munehiro Iwami |
| 第 1 著者 所属（和/英） | 北陸先端科学技術大学院大学 School of Information Science, JAIST |
| 第 2 著者 氏名（和/英） | 酒井 正彦 / Masahiko Sakai |
| 第 2 著者 所属（和/英） | 北陸先端科学技術大学院大学 School of Information Science, JAIST |
| 第 3 著者 氏名（和/英） | 外山 芳人 / Yoshihito Toyama |
| 第 3 著者 所属（和/英） | 北陸先端科学技術大学院大学 School of Information Science, JAIST |
| 発表年月日 | 1997/1/24 |
| 資料番号 | COMP96-73 |
| 巻番号（vol） | vol.96 |
| 号番号（no） | 488 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |