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 higherorder 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. Keyword. Simply-typed Term Rewriting System, Higher-order KB Procedure, Inductive Theorem, Inductionless Induction, Fusion Transformation.

• Type: Journal
• Year: 2007
• Where: IEICET
• Authors: Keiichirou Kusakari, Yuki Chiba
• Keywords: Functional Programming Languages, IEICET 2007, Kb Procedure, Term Rewriting System