WEKO3
アイテム
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques
http://hdl.handle.net/2237/21156
http://hdl.handle.net/2237/2115697004e9e-96cc-41f4-86df-2751aeb227db
名前 / ファイル | ライセンス | アクション |
---|---|---|
110006782682.pdf (759.8 kB)
|
|
Item type | 学術雑誌論文 / Journal Article(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2015-01-29 | |||||
タイトル | ||||||
タイトル | Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques | |||||
言語 | en | |||||
その他のタイトル | ||||||
その他のタイトル | 単純型付き項書き換え系における静的依存対法とその周辺 | |||||
言語 | ja | |||||
著者 |
KUSAKARI, Keiichirou
× KUSAKARI, Keiichirou× SAKAI, Masahiko× 草刈, 圭一朗× 酒井, 正彦 |
|||||
アクセス権 | ||||||
アクセス権 | open access | |||||
アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
権利 | ||||||
言語 | ja | |||||
権利情報 | (c)一般社団法人電子情報通信学会。本文データは学協会の許諾に基づきCiNiiから複製したものである | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | 単純型付き項書き換え系 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | 停止性 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | 静的依存対 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | 引数切り落とし法 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | 実効規則 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Simply-Typed Term Rewriting | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Termination | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Static Dependency Pair | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Argument Filtering | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Usable Rule | |||||
抄録 | ||||||
内容記述 | 我々が提案した関数プログラムの強力な停止性証明法である静的依存対法は一般には適用できないため取り扱うプログラムに一定の制限を課す必要がある.このような制限として我々は直接関数渡しと呼ばれる性質を提案した.本論文ではより適用範囲の広い関数渡しの安全条件を提案し,このクラスで静的依存対法が健全であることを示す.また,依存対法で停止性を証明する際には,引数切り落とし法や実効規則が重要となる.本論文では,既存の引数切り落とし法と異なり型の構造を破壊しない引数切り落とし法も与える.さらに,実効規則の既存の成果を拡張して引数切り落とし法と組合せた実効規則の概念を与える. | |||||
言語 | ja | |||||
内容記述タイプ | Abstract | |||||
抄録 | ||||||
内容記述 | We proposed a static dependency pair method, which can effectively prove termination of functional programs. Since the method is not applicable in general, we proposed plain function-passing as a restriction. In this paper, we refine the method. Firstly we propose the notion of safely function-passing, which relax the restriction of plain function-passing. Next we improve the argument filtering method, which support dependency pair methods by generating a reduction pair from a given reduction order. Our argument filtering method does not destroy type structure unlike existing method. Hence our method can effectively apply reduction orders which make use of type information. Finally we combine argument filtering method and usable rules, which reduce the number of constraints. | |||||
言語 | en | |||||
内容記述タイプ | Abstract | |||||
出版者 | ||||||
言語 | ja | |||||
出版者 | 一般社団法人電子情報通信学会 | |||||
言語 | ||||||
言語 | eng | |||||
資源タイプ | ||||||
資源タイプresource | http://purl.org/coar/resource_type/c_6501 | |||||
タイプ | journal article | |||||
出版タイプ | ||||||
出版タイプ | VoR | |||||
出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
関連情報 | ||||||
関連タイプ | isVersionOf | |||||
識別子タイプ | URI | |||||
関連識別子 | http://ci.nii.ac.jp/naid/110006782682 | |||||
ISSN | ||||||
収録物識別子タイプ | PISSN | |||||
収録物識別子 | 0913-5685 | |||||
書誌情報 |
ja : 電子情報通信学会技術研究報告SS, ソフトウェアサイエンス 巻 107, 号 505, p. 19-24, 発行日 2008-02 |
|||||
著者版フラグ | ||||||
値 | publisher | |||||
URI | ||||||
識別子 | http://ci.nii.ac.jp/naid/110006782682 | |||||
識別子タイプ | URI | |||||
URI | ||||||
識別子 | http://hdl.handle.net/2237/21156 | |||||
識別子タイプ | HDL |