Size-based termination of higher-order rewriting

TL;DR

This paper introduces a modular criterion for ensuring termination in simply-typed lambda calculus extended with user-defined rewrite rules, utilizing size-based bounds on function arguments.

Contribution

It extends previous size-based termination criteria to rewriting-based function definitions and more general notions of size, enhancing modularity and applicability.

Findings

Provides a general criterion for termination

Extends size-based approaches to rewriting systems

Applicable to user-defined functions and sizes

Abstract

We provide a general and modular criterion for the termination of simply-typed $\lambda$ -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.