|
|
Please login using the form on menu list.
It is required to login for Full-Text PDF.
|
On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
Masahiko SAKAI
Keiichirou KUSAKARI
Publication
IEICE TRANSACTIONS on Information and Systems Vol.E88-D No.3 pp.583-593
Publication Date: 2005/03/01
Online ISSN:
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Computation and Computational Models
Keyword:
termination,
dependency pair,
higher-order rewrite system,
dependency forest,
Full Text: PDF(642.8KB)
Summary:
This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. In the first order case, the termination of term rewriting systems are proved by showing the non-existence of an infinite R-chain of the dependency pairs. However, the termination and the non-existence of an infinite R-chain do not coincide in the higher-order case. We introduce a new notion of dependency forest that characterize infinite reductions and infinite R-chains, and show that the termination property of higher-order rewrite systems R can be checked by showing the non-existence of an infinite R-chain, if R is strongly linear or non-nested.
|
|
