The search functionality is under construction.
The search functionality is under construction.

Keyword Search Result

[Keyword] recursive definition(1hit)

1-1hit
  • Static Dependency Pair Method in Functional Programs

    Keiichirou KUSAKARI  

     
    PAPER-Formal Approaches

      Pubricized:
    2018/03/16
      Vol:
    E101-D No:6
      Page(s):
    1491-1502

    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.