On Proving AC-Termination by Argument Filtering Method
スポンサーリンク
概要
- 論文の詳細を見る
The notion of dependency pairs is widely used for proving termination of TRSs. Recently, this notion was extended to AC-TRSs. Using AC-dependency pairs, we can easily show the AC-termination property of AC-TRSs to which traditional techniques cannot be applied. On this notion, a weak AC-reduction pair plays an important role. In this paper, we introduce the argument filtering method, which designs a weak AC-reduction pair from an arbitary AC-reduction order. Moreover, we improve the method in two directions. One is the lexicographic argument filtering method, which lexicographically combines argument filtering functions to compare AC-dependency pairs. Another one is an extension by AC-multiset extension. These methods offer useful means to prove AC-termination of complicated AC-TRSs.
- 一般社団法人情報処理学会の論文
- 2000-06-15
著者
-
Kusakari Keiichirou
School Of Information Science Jaist
-
TOYAMA TOSHIHITO
School of Information Science, JAIST
-
Toyama Toshihito
School Of Information Science Jaist
-
Toyama Yoshihito
School Of Information Science Jaist
関連論文
- On proving AC-termination by argument filtering method
- On proving Ac-termination by AC-dependency pairs
- On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
- Higher-Order Path Orders Based on Computability(Foundations of Computer Science)
- Argument filtering transformation
- On Proving AC-Termination by Argument Filtering Method
- The hierarchy of dependency pairs
- Decidability for left-linear growing term rewriting systems
- Simplification ordering for higher-order rewrite systems
- Simplification Ordering for Higher-Order Rewrite Systems
- NVNF-sequentiality of Left-linear Term Rewriting Systems(Theory of Rewriting Systems and Its Applications)
- Church-Rosser Property and Unique Normal Form Property of Non-Duplicating Term Rewriting Systems(Theory of Rewriting Systems and Its Applications)