2024-03-28T10:23:35Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:00007856
2023-01-16T05:02:57Z
312:313:314
An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems
IWAMI, Munehiro
22456
SAKAI, Masahiko
22457
TOYAMA, Yoshihito
22458
higher-order rewrite system
term rewriting system
termination
improved recursive decomposition ordering
pseudoterminal occurrence
type
simplification ordering
Simplification orderings, like the recursive path ordering and the improved recursive decomposition ordering, are widely used for proving the termination property of term rewriting systems. The improved recursive decomposition ordering is known as the most powerful simplification ordering. Recently Jouannaud and Rubio extended the recursive path ordering to higher-order rewrite systems by introducing an ordering on type structure. In this paper we extend the improved recursive decomposition ordering for proving termination of higher-order rewrite systems. The key idea of our ordering is a new concept of pseudoterminal occurrences.
journal article
IEICE
1998-09
application/pdf
IEICE Transactions on Information and Systems
9
E81-D
988
996
http://hdl.handle.net/2237/9576
0916-8532
https://nagoya.repo.nii.ac.jp/record/7856/files/E-81-D_9_988-996.pdf
eng
Copyright 1998 IEICE 許諾番号 08RB0027号