Size-based termination of higher-order rewriting
Logic in Computer Science
2018-02-21 v2
Abstract
We provide a general and modular criterion for the termination of simply-typed -calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern-matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.
Keywords
Cite
@article{arxiv.1802.06603,
title = {Size-based termination of higher-order rewriting},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:1802.06603},
year = {2018}
}