Rewrite orderings for higher-order terms in eta-long beta-normal form and the recursive path ordering

摘要

This paper extends the termination proof techniques based on rewrite orderings to a higher-order setting, by defining a recursive path ordering for simply typed higher-order terms in long beta-normal form. This ordering is powerful enough to show termination of several complex examples. (C) 1998-Elsevier Science B.V. All rights reserved. [References: 19]