講演抄録/キーワード |
講演名 |
2010-08-05 16:00
高階書換え系における引数切り落とし法と実効規則 ○鈴木 翔・草刈圭一朗(名大)・フレデリック ブランキ(INRIA) SS2010-24 |
抄録 |
(和) |
静的依存対法は高階書換え系の停止性証明法である.
この手法は一階の書換え系上で提案された依存対法と型付き$\lambda$計算の停止性証明で導入された強計算性を融合することによって設計されている.
引数切り落とし法と実効規則は依存対法の枠組みにおける重要な二つの概念である.
本論文では,これらの手法を高階書換え系上に拡張する. |
(英) |
The static dependency pair method is a method for proving the termination
of higher-order rewrite systems {\em \`a la} Nipkow.
It combines the dependency pair method introduced for first-order rewrite systems with the notion of strong computability introduced for typed $\lambda$-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. |
キーワード |
(和) |
高階書換え系 / 停止性 / 静的依存対法 / 引数切り落とし法 / 実効規則 / / / |
(英) |
higher-order rewrite system / termination / static dependency pair method / argument filtering / usable rule / / / |
文献情報 |
信学技報, vol. 110, no. 169, SS2010-24, pp. 47-52, 2010年8月. |
資料番号 |
SS2010-24 |
発行日 |
2010-07-29 (SS) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2010-24 |