2024-03-29T11:26:43Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:00007859
2023-01-16T05:02:57Z
312:313:314
On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
SAKAI, Masahiko
22463
KUSAKARI, Keiichirou
22464
termination
dependency pair
higher-order rewite system
dependency forest
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.
journal article
IEICE
2005-03
application/pdf
IEICE Transactions on Information and Systems
3
E88-D
583
593
http://hdl.handle.net/2237/9579
0916-8532
https://nagoya.repo.nii.ac.jp/record/7859/files/E88-D_n3_583-593.pdf
eng
Copyright 2005 IEICE 許諾番号 08RB0027号