|
JAIST Repository >
b. 情報科学研究科・情報科学系 >
b10. 学術雑誌論文等 >
b10-1. 雑誌掲載論文 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/7831
|
| タイトル: | A Higher-Order Knuth-Bendix Procedure and Its Applications |
| 著者: | KUSAKARI, Keiichirou
CHIBA, Yuki |
| キーワード: | simply-typed term rewriting system
higher-order KB procedure
inductive theorem
inductionless induction
fusion transformation |
| 発行日: | 2007-04-01 |
| 出版者: | 電子情報通信学会 |
| 誌名: | IEICE TRANSACTIONS on Information and Systems |
| 巻: | E90-D |
| 号: | 4 |
| 開始ページ: | 707 |
| 終了ページ: | 715 |
| DOI: | 10.1093/ietisy/e90-d.4.707 |
| 抄録: | 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. |
| Rights: | Copyright (C)2007 IEICE. Keiichirou Kusakari and Yuki Chiba, IEICE TRANSACTIONS on Information and Systems, E90-D(4), 2007, 707-715. http://www.ieice.org/jpn/trans_online/ |
| URI: | http://hdl.handle.net/10119/7831 |
| 資料タイプ: | publisher |
| 出現コレクション: | b10-1. 雑誌掲載論文 (Journal Articles)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| A12054.pdf | | 194Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
