Size-based termination of higher-order rewrite systems

Frédéric Blanqui (1)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique

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.

Keywords: termination; rewriting; lambda-calculus; size; max-plus algebra; typing; subtyping

Domains: Logic in Computer Science [cs.LO]

Frédéric Blanqui. Size-based termination of higher-order rewrite systems. 2017. ⟨hal-01424921v1⟩