Higher-Order Path Orders Based on Computability
Summary :
Simply-typed term rewriting systems (STRSs) are an extension of term rewriting systems. STRSs can be naturally handle higher order functions, which are widely used in existing functional programming languages. In this paper we design recursive and lexicographic path orders, which can efficiently prove the termination of STRSs. Moreover we discuss an application to the dependency pair and the argument filtering methods, which are very effective and efficient support methods for proving termination.
- Publication
- IEICE TRANSACTIONS on Information Vol.E87-D No.2 pp.352-359
- Publication Date
- 2004/02/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Section on Foundations of Computer Science)
- Category
Authors
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, "Higher-Order Path Orders Based on Computability" in IEICE TRANSACTIONS on Information,
vol. E87-D, no. 2, pp. 352-359, February 2004, doi: .
Abstract: Simply-typed term rewriting systems (STRSs) are an extension of term rewriting systems. STRSs can be naturally handle higher order functions, which are widely used in existing functional programming languages. In this paper we design recursive and lexicographic path orders, which can efficiently prove the termination of STRSs. Moreover we discuss an application to the dependency pair and the argument filtering methods, which are very effective and efficient support methods for proving termination.
URL: https://global.ieice.org/en_transactions/information/10.1587/e87-d_2_352/_p
Copy
@ARTICLE{e87-d_2_352,
author={Keiichirou KUSAKARI, },
journal={IEICE TRANSACTIONS on Information},
title={Higher-Order Path Orders Based on Computability},
year={2004},
volume={E87-D},
number={2},
pages={352-359},
abstract={Simply-typed term rewriting systems (STRSs) are an extension of term rewriting systems. STRSs can be naturally handle higher order functions, which are widely used in existing functional programming languages. In this paper we design recursive and lexicographic path orders, which can efficiently prove the termination of STRSs. Moreover we discuss an application to the dependency pair and the argument filtering methods, which are very effective and efficient support methods for proving termination.},
keywords={},
doi={},
ISSN={},
month={February},}
Copy
TY - JOUR
TI - Higher-Order Path Orders Based on Computability
T2 - IEICE TRANSACTIONS on Information
SP - 352
EP - 359
AU - Keiichirou KUSAKARI
PY - 2004
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E87-D
IS - 2
JA - IEICE TRANSACTIONS on Information
Y1 - February 2004
AB - Simply-typed term rewriting systems (STRSs) are an extension of term rewriting systems. STRSs can be naturally handle higher order functions, which are widely used in existing functional programming languages. In this paper we design recursive and lexicographic path orders, which can efficiently prove the termination of STRSs. Moreover we discuss an application to the dependency pair and the argument filtering methods, which are very effective and efficient support methods for proving termination.
ER -
English
