On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
スポンサーリンク
概要
- 論文の詳細を見る
This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. In the first order case, the termination of term rewriting systems are proved by showing the non-existence of an infinite R-chain of the dependency pairs. However, the termination and the non-existence of an infinite R-chain do not coincide in the higher-order case. We introduce a new notion of dependency forest that characterize infinite reductions and infinite R-chains, and show that the termination property of higher-order rewrite systems R can be checked by showing the non-existence of an infinite R-chain, if R is strongly linear or non-nested.
- 社団法人電子情報通信学会の論文
- 2005-03-01
著者
-
KUSAKARI Keiichirou
Graduate School of Information Science, Nagoya Univ.
-
SAKAI Masahiko
Graduate School of Information Science, Nagoya Univ.
-
Sakai M
Graduate School Of Information Science Nagoya University
-
Sakai Masahiko
Graduate School Of Information Science Nagoya Univ.
-
Kusakari Keiichirou
Graduate School Of Information Science Nagoya University
-
Kusakari Keiichirou
Graduate School Of Information Science Nagoya Univ.
-
Kusakari Keiichirou
School Of Information Science Jaist
-
Sakai Masahiko
Department Of Information Engineering Nagoya University
関連論文
- Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems
- Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes
- Recognizability of Redexes for Higher-Order Rewrite Systems
- Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs
- Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems
- An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
- Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques
- An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems
- Left-Incompatible Term Rewriting Systems and Functional Strategy
- Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes
- Argument Filterings and Usable Rules in Higher-order Rewrite Systems
- Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting
- Characterizing Inductive Theorems by Extensional Initial Models in a Higher-Order Equational Logic
- On proving AC-termination by argument filtering method
- A Higher-Order Knuth-Bendix Procedure and Its Applications
- 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
- 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)
- Confluence of Length Preserving String Rewriting Systems is Undecidable
- Static Dependecy Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types
- Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems
- Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems