WEKO3
アイテム
A Higher-Order Knuth-Bendix Procedure and Its Applications
http://hdl.handle.net/2237/14974
http://hdl.handle.net/2237/149746ec11bdd-b48f-428c-8564-93430b622629
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
401.pdf (198.9 kB)
|
|
| アイテムタイプ | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2011-06-29 | |||||
| タイトル | ||||||
| タイトル | A Higher-Order Knuth-Bendix Procedure and Its Applications | |||||
| 言語 | en | |||||
| 著者 |
KUSAKARI, Keiichirou
× KUSAKARI, Keiichirou× CHIBA, Yuki |
|||||
| アクセス権 | ||||||
| アクセス権 | open access | |||||
| アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
| 権利 | ||||||
| 権利情報 | Copyright (C) 2007 IEICE | |||||
| 言語 | en | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | simply-typed term rewriting system | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | higher-order KB procedure | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | inductive theorem | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | inductionless induction | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | fusion transformation | |||||
| 抄録 | ||||||
| 内容記述タイプ | 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. | |||||
| 言語 | en | |||||
| 出版者 | ||||||
| 出版者 | Institute of Electronics, Information and Communication Engineers | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | eng | |||||
| 資源タイプ | ||||||
| 資源タイプresource | http://purl.org/coar/resource_type/c_6501 | |||||
| タイプ | journal article | |||||
| 出版タイプ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| 関連情報 | ||||||
| 関連タイプ | isVersionOf | |||||
| 識別子タイプ | URI | |||||
| 関連識別子 | http://www.ieice.org/jpn/trans_online/index.html | |||||
| ISSN | ||||||
| 収録物識別子タイプ | PISSN | |||||
| 収録物識別子 | 0916-8532 | |||||
| 書誌情報 |
en : IEICE transactions on information and systems 巻 E90-D, 号 4, p. 707-715, 発行日 2007-04-01 |
|||||
| 著者版フラグ | ||||||
| 値 | publisher | |||||
| URI | ||||||
| 識別子 | http://www.ieice.org/jpn/trans_online/index.html | |||||
| 識別子タイプ | URI | |||||
| URI | ||||||
| 識別子 | http://hdl.handle.net/2237/14974 | |||||
| 識別子タイプ | HDL | |||||
