Static Dependency Pair Method in Functional Programs

Keiichirou KUSAKARI  

IEICE TRANSACTIONS on Information and Systems   Vol.E101-D   No.6   pp.1491-1502
Publication Date: 2018/06/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2017FOP0004
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.