An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems
スポンサーリンク
概要
- 論文の詳細を見る
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 known as the most powerful simplification ordering. Recently Jouannaud and 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.
- 社団法人電子情報通信学会の論文
- 1998-09-25
著者
-
Sakai M
Graduate School Of Information Science Nagoya University
-
IWAMI Munehiro
Faculty of Information Science, Japan Advanced Institute of Science and Technology
-
SAKAI Masahiko
Faculty of Information Science, Nagoya University
-
TOYAMA Yoshihito
Faculty of Information Science, Japan Advanced Institute of Science and Technology
-
Iwami M
School Of Information Science Japan Advanced Institute Of Science And Technology Hokuriku
-
Iwami Munehiro
Faculty Of Information Science Japan Advanced Institute Of Science And Technology
-
Toyama Yoshihito
School of Information Science, Japan Advanced Institute of Science and Technology, Hokuriku
-
Toyama Yoshihito
Faculty Of Information Science Japan Advanced Institute Of Science And Technology
-
Sakai Masahiko
Department Of Information Engineering Nagoya University
-
Sakai Masahiko
Faculty Of Information Science Nagoya University
関連論文
- An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
- An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems
- Left-Incompatible Term Rewriting Systems and Functional Strategy
- 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
- Argument filtering transformation
- The hierarchy of dependency pairs
- Decidability for left-linear growing term rewriting systems
- Simplification ordering for higher-order rewrite systems
- Persistence of Termination for Non-Overlapping Term Rewriting Systems
- Simplification Ordering for Higher-Order Rewrite Systems
- Effects of Chemical Modification of Arginine Residues Outside the Active Site Cleft of Ricin A-Chain on Its RNA N-Glycosidase Activity for Ribosomes
- Index Reduction of Overlapping Strongly Sequential Systems
- NVNF-sequentiality of Left-linear Term Rewriting Systems(Theory of Rewriting Systems and Its Applications)