A Higher-Order Knuth-Bendix Procedure and Its Applications

Keiichirou KUSAKARI; Yuki CHIBA

doi:10.1093/ietisy/e90-d.4.707

A Higher-Order Knuth-Bendix Procedure and Its Applications

Keiichirou KUSAKARI, Yuki CHIBA

Full Text Views

0

Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Information Vol.E90-D No.4 pp.707-715

Publication Date: 2007/04/01

Publicized

Online ISSN: 1745-1361

DOI: 10.1093/ietisy/e90-d.4.707

Type of Manuscript: PAPER

Category: Computation and Computational Models

Cite this

Copy

Keiichirou KUSAKARI, Yuki CHIBA, "A Higher-Order Knuth-Bendix Procedure and Its Applications" in IEICE TRANSACTIONS on Information, vol. E90-D, no. 4, pp. 707-715, April 2007, doi: 10.1093/ietisy/e90-d.4.707.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1093/ietisy/e90-d.4.707/_p

Copy

@ARTICLE{e90-d_4_707,
author={Keiichirou KUSAKARI, Yuki CHIBA, },
journal={IEICE TRANSACTIONS on Information},
title={A Higher-Order Knuth-Bendix Procedure and Its Applications},
year={2007},
volume={E90-D},
number={4},
pages={707-715},
abstract={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.},
keywords={},
doi={10.1093/ietisy/e90-d.4.707},
ISSN={1745-1361},
month={April},}

Copy

TY - JOUR
TI - A Higher-Order Knuth-Bendix Procedure and Its Applications
T2 - IEICE TRANSACTIONS on Information
SP - 707
EP - 715
AU - Keiichirou KUSAKARI
AU - Yuki CHIBA
PY - 2007
DO - 10.1093/ietisy/e90-d.4.707
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E90-D
IS - 4
JA - IEICE TRANSACTIONS on Information
Y1 - April 2007
AB - 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.
ER -