A Higher-Order Knuth-Bendix Procedure and Its Applications

13 years 4 months ago

Download www.sakabe.nuie.nagoya-u.ac.jp

The completeness (i.e. conﬂuent 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 certiﬁcation technique called inductionless induction used in program veriﬁcation, 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.

Keiichirou Kusakari, Yuki Chiba

Real-time Traffic