| 講演抄録／キーワード |
| 講演名 |
2005-06-24 11:45
ナローイング計算の停止性証明のための依存グラフ法
○三浦浩一・西田直樹・酒井正彦・草刈圭一朗・坂部俊樹（名大） |
| 抄録 |
（和） |
項書換え系（TRS）を右辺のみに現れる変数を持つ書換え規則を含むように拡張した余剰変数付き項書換え系（EV-TRS）は逆計算プログラムなどを表現でき，その書換え計算は基礎項からのナローイングによって模倣できる．本稿では，項書換え系の停止性証明手法である依存グラフ法が，構成子EV-TRSなどのクラスを対象とした基礎項からのナローイング計算の停止性証明に%の手法として利用できることを示す．本手法では，切り落とし関数が全ての余剰変数を削除しているという条件が追加される．さらに，ナローイング計算の停止性を保証するための追加条件も示す． |
| （英） |
Term rewriting systems with extra variables (called EV-TRSs) has an ability to represent inverse-computation programs, and the rewrite sequences of EV-TRSs are simulated as narrowing sequences starting from ground terms. In this paper, we show that the ordinary dependency graph method for proving termination of TRSs works also for constructor EV-TRSs and so on, to prove termination of narrowing which starts from ground terms, by imposing argument filterings to eliminate all extra variables in every dependency pairs. We also give an additional condition to prove termination of the ordinary narrowing. |
| キーワード |
（和） |
項書換え系 / 余剰変数 / 依存対 / 切り落とし関数 / / / / |
| （英） |
term rewriting system / extra variable / dependency pair / argument filtering / / / / |
| 文献情報 |
信学技報, vol. 105, no. 129, SS2005-23, pp. 31-36, 2005年6月. |
| 資料番号 |
SS2005-23 |
| 発行日 |
2005-06-17 (SS) |
| ISSN |
Print edition: ISSN 0913-5685 |
| PDFダウンロード |
|