Size-based termination of higher-order rewriting

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.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

Littérature citée [175 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01424921
Contributeur : Frédéric Blanqui <>
Soumis le : mardi 12 décembre 2017 - 18:21:25
Dernière modification le : samedi 10 février 2018 - 01:16:36

Fichiers

Identifiants

  • HAL Id : hal-01424921, version 2

Collections

Citation

Frédéric Blanqui. Size-based termination of higher-order rewriting. 2017. 〈hal-01424921v2〉

Partager

Métriques

Consultations de la notice

54

Téléchargements de fichiers

26