WEKO3
アイテム
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Technique
http://hdl.handle.net/2237/14975
http://hdl.handle.net/2237/14975886d8b94-f25c-440a-9978-69a15fd7836a
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
402.pdf (297.9 kB)
|
|
| アイテムタイプ | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2011-06-29 | |||||
| タイトル | ||||||
| タイトル | Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Technique | |||||
| 言語 | en | |||||
| 著者 |
KUSAKARI, Keiichirou
× KUSAKARI, Keiichirou× SAKAI, Masahiko |
|||||
| アクセス権 | ||||||
| アクセス権 | open access | |||||
| アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
| 権利 | ||||||
| 権利情報 | Copyright (C) 2009 IEICE | |||||
| 言語 | en | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | simply-typed term rewriting | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | termination | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | static dependency pair method | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | argument filtering | |||||
| キーワード | ||||||
| 主題Scheme | Other | |||||
| 主題 | usable rule | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | A static dependency pair method, proposed by us, can effectively prove termination of simply-typed term rewriting systems (STRSs). The theoretical basis is given by the notion of strong computability. This method analyzes a static recursive structure based on definition dependency. By solving suitable constraints generated by the analysis result, we can prove the termination. Since this method is not applicable to every system, we proposed a class, namely, plain function-passing, as a restriction. In this paper, we first propose the class of safe function-passing, which relaxes the restriction by plain function-passing. To solve constraints, we often use the notion of reduction pairs, which is designed from a reduction order by the argument filtering method. Next, we improve the argument filtering method for STRSs. Our argument filtering method does not destroy type structure unlike the existing method for STRSs. Hence, our method can effectively apply reduction orders which make use of type information. To reduce constraints, the notion of usable rules is proposed. Finally, we enhance the effectiveness of reducing constraints by incorporating argument filtering into usable rules for STRSs. | |||||
| 言語 | 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 巻 E92-D, 号 2, p. 235-247, 発行日 2009-02-01 |
|||||
| 著者版フラグ | ||||||
| 値 | publisher | |||||
| URI | ||||||
| 識別子 | http://www.ieice.org/jpn/trans_online/index.html | |||||
| 識別子タイプ | URI | |||||
| URI | ||||||
| 識別子 | http://hdl.handle.net/2237/14975 | |||||
| 識別子タイプ | HDL | |||||
