Summary
|
For Full-Text PDF, please login, if you are a member of IEICE, or go to Pay Per View on menu list, if you are a nonmember of IEICE. |
|
Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems Keiichirou KUSAKARI Yasuo ISOGAI Masahiko SAKAI Frederic BLANQUI Publication IEICE TRANSACTIONS on Information and Systems Vol.E92-D No.10 pp.2007-2015 Publication Date: 2009/10/01 Online ISSN: 1745-1361 DOI: 10.1587/transinf.E92.D.2007 Print ISSN: 0916-8532 Type of Manuscript: PAPER Category: Computation and Computational Models Keyword: higher-order rewrite system, termination, static dependency pair, plain function-passing, strong computability, subterm criterion, Full Text: PDF(274.3KB)>>
Summary: Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions. | ||||||||||
| ||||||||||