Static dependency pair method based on strong computability for higher-order rewrite systems. K. Kusakari, Y. Isogai, M. Sakai and F. Blanqui. IEICE Transactions on Information and Systems E92-D(10), 9 pages, 2009.

Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. Recently, we proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, to prove termination of STRSs. In this paper, we extend the method to HRSs. Since HRSs include lambda-abstraction, but STRSs do not, we restructure the static dependency pair method to correspond to lambda-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.