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 in Functional Programs
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2018/06/01
Online ISSN: 1745-1361
Type of Manuscript: Special Section PAPER (Special Section on Formal Approaches)
Category: Formal Approaches
functional program, term rewriting system, termination, recursive definition, static dependency pair method,
Full Text: PDF(281.4KB)
>>Buy this Article
We have previously introduced the static dependency pair method that proves termination by analyzing the static recursive structure of various extensions of term rewriting systems for handling higher-order functions. The key is to succeed with the formalization of recursive structures based on the notion of strong computability, which is introduced for the termination of typed λ-calculi. To bring the static dependency pair method close to existing functional programs, we also extend the method to term rewriting models in which functional abstractions with patterns are permitted. Since the static dependency pair method is not sound in general, we formulate a class; namely, accessibility, in which the method works well. The static dependency pair method is a very natural reasoning; therefore, our extension differs only slightly from previous results. On the other hand, a soundness proof is dramatically difficult.