Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems
スポンサーリンク
概要
- 論文の詳細を見る
Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.
- （社）電子情報通信学会の論文
- 2009-10-01
著者
-
KUSAKARI Keiichirou
Graduate School of Information Science, Nagoya Univ.
-
ISOGAI Yasuo
Graduate School of Information Science, Nagoya Univ.
-
SAKAI Masahiko
Graduate School of Information Science, Nagoya Univ.
-
BLANQUI Frédéric
INRIA & LORIA
-
Isogai Yasuo
Graduate School Of Information Science Nagoya Univ.
-
Sakai Masahiko
Graduate School Of Information Science Nagoya Univ.
-
Kusakari Keiichirou
Graduate School Of Information Science Nagoya Univ.
-
Blanqui Frederic
Inria & Loria
-
Blanqui Frederic
Inria
関連論文
- 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
- Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques
- 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
- A Higher-Order Knuth-Bendix Procedure and Its Applications
- On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
- Higher-Order Path Orders Based on Computability(Foundations of Computer Science)
- 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