| 講演名 | 2010-08-05 高階書換え系における引数切り落とし法と実効規則 鈴木 翔, 草刈 圭一朗 /, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 静的依存対法は高階書換え系の停止性証明法である.この手法は一階の書換え系上で提案された依存対法と型付きλ計算の停止性証明で導入された強計算性を融合することによって設計されている.引数切り落とし法と実効規則は依存対法の枠組みにおける重要な二つの概念である.本論文では,これらの手法を高階書換え系上に拡張する. |
| 抄録(英) | The static dependency pair method is a method for proving the termination of higher-order rewrite systems a la Nipkow. It combines the dependency pair method introduced for first-order rewrite systems with the notion of strong computability introduced for typed λ-calculi. Argument filterings and usable rules are two important methods of the dependency pair framework used by current state-of-the-art first-order automated termination provers. In this paper, we extend the class of higher-order systems on which the static dependency pair method can be applied. Then, we extend argument filterings and usable rules to higher-order rewriting, hence providing the basis for a powerful automated termination prover for higher-order rewrite systems. |
| キーワード(和) | |
| キーワード(英) | |
| 資料番号 | SS2010-24 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2010/7/29(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | 高階書換え系における引数切り落とし法と実効規則 |
| サブタイトル（和） | |
| タイトル（英） | Argument Filterings and Usable Rules in Higher-Order Rewrite Systems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | |
| 第 1 著者 氏名（和/英） | 鈴木 翔 / Sho SUZUKI |
| 第 1 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Nagoya University, Graduate School of Information Science |
| 第 2 著者 氏名（和/英） | 草刈 圭一朗 / / Keiichirou KUSAKARI |
| 第 2 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 / Nagoya University, Graduate School of Information Science |
| 発表年月日 | 2010-08-05 |
| 資料番号 | SS2010-24 |
| 巻番号（vol） | vol.110 |
| 号番号（no） | 169 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |