A Higher-Order Knuth-Bendix Procedure and Its Applications
スポンサーリンク
概要
- 論文の詳細を見る
The completeness (i.e. confluent and terminating) property is an important concept when using a term rewriting system (TRS) as a computational model of functional programming languages. Knuth and Bendix have proposed a procedure known as the KB procedure for generating a complete TRS. A TRS cannot, however, directly handle higher-order functions that are widely used in functional programming languages. In this paper, we propose a higher-order KB procedure that extends the KB procedure to the framework of a simply-typed term rewriting system (STRS) as an extended TRS that can handle higher-order functions. We discuss the application of this higher-order KB procedure to a certification technique called inductionless induction used in program verification, and its application to fusion transformation, a typical kind of program transformation.
- 社団法人電子情報通信学会の論文
- 2007-04-01
著者
-
KUSAKARI Keiichirou
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.
-
Chiba Yuki
Research Institute for Scientific Measurements, Tohoku University
-
Chiba Yuki
Research Institute Of Electrical Communication Tohoku University
-
Chiba Yuki
Research Institute For Scientific Measurements Tohoku University
関連論文
- 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
- Far-Infrared Reflectivity Spectra of the Hydrogen-Bonded Ferroelectric KH_2PO_4 Measured by Synchrotron Radiation
- 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)
- Automatic Construction of Program Transformation Templates
- Program Transformation by Templates : A Rewriting Framework
- 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
- Program Transformation by Templates: A Rewriting Framework
- Automatic Construction of Program Transformation Templates
- Automatic Construction of Program Transformation Templates
- Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems
- Program Transformation by Templates: A Rewriting Framework