A higher-order Knuth-Bendix procedure and its applications

被引：2
|
作者：
Kusakari, Keiichirou [1 ]
Chiba, Yuki
机构：
[1] Nagoya Univ, Grad Sch Informat Sci, Nagoya, Aichi 4648603, Japan
[2] Tohoku Univ, Elect Commun Res Inst, Sendai, Miyagi 9808577, Japan
来源：
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS | 2007年 / E90D卷 / 04期
关键词：
simply-typed term rewriting system; higher-order KB procedure; inductive theorem; inductionless induction; fusion transformation;
D O I：
10.1093/ietisy/e90-d.4.707
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
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.
引用
收藏
页码：707 / 715
页数：9
相关论文
共 50 条
  • [1] A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms
    Becker, Heiko
    Blanchette, Jasmin Christian
    Waldmann, Uwe
    Wand, Daniel
    [J]. AUTOMATED DEDUCTION - CADE 26, 2017, 10395 : 432 - 453
  • [2] Orienting equalities with the Knuth-Bendix order
    Korovin, K
    Voronkov, A
    [J]. 18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, : 75 - 84
  • [3] THE KNUTH-BENDIX COMPLETION PROCEDURE AND THUE SYSTEMS
    KAPUR, D
    NARENDRAN, P
    [J]. SIAM JOURNAL ON COMPUTING, 1985, 14 (04) : 1052 - 1072
  • [4] Orienting rewrite rules with the Knuth-Bendix order
    Korovin, K
    Voronkov, A
    [J]. INFORMATION AND COMPUTATION, 2003, 183 (02) : 165 - 186
  • [5] Categorification, term rewriting and the Knuth-Bendix procedure
    Beke, Tibor
    [J]. JOURNAL OF PURE AND APPLIED ALGEBRA, 2011, 215 (05) : 728 - 740
  • [6] An AC-compatible Knuth-Bendix order
    Korovin, K
    Voronkov, A
    [J]. AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 47 - 59
  • [7] AN INTRODUCTION TO KNUTH-BENDIX COMPLETION
    DICK, AJJ
    [J]. COMPUTER JOURNAL, 1991, 34 (01): : 2 - 15
  • [8] THE KNUTH-BENDIX PROCEDURE FOR STRINGS AS A SUBSTITUTE FOR COSET ENUMERATION
    SIMS, CC
    [J]. JOURNAL OF SYMBOLIC COMPUTATION, 1991, 12 (4-5) : 439 - 442
  • [9] The decidability of the first-order theory of Knuth-Bendix order
    Zhang, T
    Sipma, HB
    Manna, Z
    [J]. AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 131 - 148
  • [10] On Transfinite Knuth-Bendix Orders
    Kovacs, Laura
    Moser, Georg
    Voronkov, Andrei
    [J]. AUTOMATED DEDUCTION - CADA-23, 2011, 6803 : 384 - +
12345