A size-based termination criterion for dependently-typed higher-order rule-based programs. Journal version of RTA'04 and CSL'05. F. Blanqui. Submitted.

Several authors devised size-based termination criteria for ML-like function definitions (lambda-calculi with inductive types and case analysis) that can handle non-structural recursive calls. These criteria use a notion of size related to the semantics of inductive types. Roughly speaking, for data types like lists or trees, the size of a normal term is the height of its tree representation. Typing judgments are then extended to derive informations about the size of terms. Hence, termination can be ensured by using a combination of type checking and constraint solving on size annotations. In the present paper, we extend these works to rewriting-based function definitions, dependent types and more general notions of size. We therefore provide a powerful termination criterion for the combination of rewriting and beta-reduction in the Calculus of Constructions.

This works detail and extend in important ways the conference papers of RTA'04 and CSL'05. In particular, we show how to use other notions of size and allow a much larger class of rule left-hand sides in successor-based systems.

Last updated on 9 November 2011. Come back to main page.