Size-based termination of higher-order rewrite systems. F. Blanqui. 70 pages, submitted on Dec. 2015, revised in Jan. 2017.
This paper is concerned with the termination, in Church’ simply-typed λ-calculus, of the combination of β-reduction and arbitrary user-defined rewrite rules fired using matching modulo α-congruence only.
Several authors have devised termination criteria for fixpoint-based function definitions using deduction rules for bounding the size of terms inhabiting inductively defined types, where the size of a term is (roughly speaking) the set-theoretical height of the tree representation of its normal form.
In the present paper, we extend this approach to rewriting-based function definitions and more general notions of size.