Higher-Order Path Orders Based on Computability(<Special Section>Foundations of Computer Science)
スポンサーリンク
概要
- 論文の詳細を見る
Simply-typed term rewriting systems (STRSs) are an extension of term rewriting systems. STRSs can be naturally handle higher order functions, which are widely used in existing functional programming languages. In this paper we design recursive and lexicographic path orders, which can efficiently prove the termination of STRSs. Moreover we discuss an application to the dependency pair and the argument filtering methods, which are very effective and efficient support methods for proving termination.
- 社団法人電子情報通信学会の論文
- 2004-02-01
著者
-
KUSAKARI Keiichirou
Graduate School of Information Science, Nagoya Univ.
-
Kusakari Keiichirou
Graduate School Of Information Science Nagoya Univ.
-
Kusakari Keiichirou
School Of Information Science Jaist
関連論文
- Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems
- 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
- 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
- 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