| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2009-12-17 15:50 高階書換え系における引数切り落とし法と実効規則 ○鈴木 翔・草刈圭一朗・坂部俊樹・酒井正彦・西田直樹（名大）  SS2009-39 |
|
| 抄録 | （和） | 項書換え系（TRS）の拡張として高階関数を直接扱える単純型付き項書換え系（STRS）や さらに$\lambda$抽象も扱える高階書換え系（HRS）が提案されている． 静的依存対法はこれら高階の系における非常に強力な停止性証明法である． 静的依存対法で停止性を証明する際には引数切り落とし法や実効規則の概念が重要となる． これらはTRS上で提案されSTRS上に拡張されているが，HRS上では知られていない． 本論文ではHRS上の引数切り落とし法と実効規則の概念を与える． さらに我々の成果は単なる拡張ではなく， 引数切り落とし法で要求されていた適用条件を取り除き， 実効規則の定義から高階変数を介した依存性を取り除くという改良も伴っている． |
| （英） | Simply-typed term rewriting systems (STRSs) and higher-order rewrite systems (HRSs) have been proposed to extend term rewriting systems (TRSs). These systems can handle higher-order functions directly, and moreover HRSs are allowed to have a $\lambda$-abstraction syntax. Static dependency pair methods are very powerful methods for proving termination of these higher-order systems. Notions of argument filtering and usable rules play important roles in proving termination by the static dependency pair method. These notions are proposed on TRSs, and extended to STRSs. However, we have not known these notions on HRSs. In this paper, we extend notions of argument filtering and usable rules onto HRSs. In addition, these extensions include some enhancements: removing an applicable condition demanded by existing argument fitering methods on STRSs, and removing a dependency through higher-order variables from the definition of usable rule. |
|
| キーワード | （和） | 高階書換え系 / 停止性 / 静的依存対法 / 引数切り落とし法 / 実効規則 / / / |
| （英） | higher-order rewrite system / termination / static dependency pair method / argument filtering / usable rule / / / | |
| 文献情報 | 信学技報, vol. 109, no. 343, SS2009-39, pp. 25-30, 2009年12月. | |
| 資料番号 | SS2009-39 | |
| 発行日 | 2009-12-10 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2009-39 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2009-12-17 - 2009-12-18 |
| 開催地（和） | 香川大学幸町キャンパス |
| 開催地（英） | Kagawa Univ. |
| テーマ（和） | 一般 |
| テーマ（英） | general |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2009-12-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 高階書換え系における引数切り落とし法と実効規則 |
| サブタイトル（和） | |
| タイトル（英） | Argument Filtering and Usable Rules in Higher-Order Rewrite Systems |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 高階書換え系 / higher-order rewrite system |
| キーワード(2)（和/英） | 停止性 / termination |
| キーワード(3)（和/英） | 静的依存対法 / static dependency pair method |
| キーワード(4)（和/英） | 引数切り落とし法 / argument filtering |
| キーワード(5)（和/英） | 実効規則 / usable rule |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 鈴木 翔 / Sho Suzuki / スズキ ショウ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 草刈 圭一朗 / Keiichirou Kusakari / クサカリ ケイイチロウ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 坂部 俊樹 / Toshiki Sakabe / サカベ トシキ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ |
| 第4著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第5著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2009-12-17 15:50:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2009-39 |
| 巻番号（vol） | vol.109 |
| 号番号（no） | no.343 |
| ページ範囲 | pp.25-30 |
| ページ数 | 6 |
| 発行日 | 2009-12-10 (SS) |
[研究会発表申込システムのトップページに戻る]