| 講演抄録／キーワード |
| 講演名 |
2005-03-18 10:25
修正AC単調意味論経路順序によるAC停止性
○落合秀幸・青戸等人・外山芳人（東北大） |
| 抄録 |
（和） |
AC項書き換え系はAC(結合律・交換律)を法とした簡約関係により項書き換え系を拡張した計算モデルである. AC項書き換え系の停止性(AC停止性)を示すために様々なAC簡約化順序が提案されている. 本論文では, 最近BorrallerasとRubio(2003)により示された, AC単調意味論経路順序がAC簡約化順序であるという結果に対して反例を与える. つまり, 彼らのAC単調意味論経路順序はAC停止性を保証できない. 我々は, この反例の解析をもとに, AC単調意味論経路順序を修正した新しい順序を提案し, その正当性を示す. この修正AC単調意味論経路順序は, 現在知られているAC簡約化順序のうち, 最も強力なAC簡約化順序の1つとなっている. |
| （英） |
AC term rewriting is a computational model that deals the rewrite relation modulo AC (associative-commutative law). Various AC reduction orderings are proposed to show the termination of AC term rewriting systems. In this paper, we give an example that shows the monotonic AC semantic path ordering recently proposed by Borralleras and Rubio (2003) is not an AC reduction ordering; hence their ordering can not be used to guarantee the AC termination. We obtain a new monotonic AC semantic path ordering by analyzing this counterexample and prove its correctness. Our modified monotonic AC semantic path ordering is one of the most powerful AC reduction orderings that have been proposed. |
| キーワード |
（和） |
AC項書き換え / AC停止性 / AC簡約化順序 / / / / / |
| （英） |
AC-term rewriting / AC-termination / AC-reduction order / / / / / |
| 文献情報 |
信学技報, vol. 104, no. 743, COMP2004-76, pp. 23-31, 2005年3月. |
| 資料番号 |
COMP2004-76 |
| 発行日 |
2005-03-11 (COMP) |
| ISSN |
Print edition: ISSN 0913-5685 |
| PDFダウンロード |
|