Static Dependency Pair Method in Functional Programs
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E101-D No.6 pp.1491-1502
- Publication Date
- 2018/06/01
- Publicized
- 2018/03/16
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2017FOP0004
- Type of Manuscript
- Special Section PAPER (Special Section on Formal Approaches)
- Category
- Formal Approaches
Authors
Keiichirou KUSAKARI
Gifu University
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Keiichirou KUSAKARI, "Static Dependency Pair Method in Functional Programs" in IEICE TRANSACTIONS on Information,
vol. E101-D, no. 6, pp. 1491-1502, June 2018, doi: 10.1587/transinf.2017FOP0004.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2017FOP0004/_p
Copy
@ARTICLE{e101-d_6_1491,
author={Keiichirou KUSAKARI, },
journal={IEICE TRANSACTIONS on Information},
title={Static Dependency Pair Method in Functional Programs},
year={2018},
volume={E101-D},
number={6},
pages={1491-1502},
abstract={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.},
keywords={},
doi={10.1587/transinf.2017FOP0004},
ISSN={1745-1361},
month={June},}
Copy
TY - JOUR
TI - Static Dependency Pair Method in Functional Programs
T2 - IEICE TRANSACTIONS on Information
SP - 1491
EP - 1502
AU - Keiichirou KUSAKARI
PY - 2018
DO - 10.1587/transinf.2017FOP0004
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E101-D
IS - 6
JA - IEICE TRANSACTIONS on Information
Y1 - June 2018
AB - 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.
ER -
English
