Termination of rewrite relations on λ-terms based on Girard's notion of reducibility

Abstract : In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of β-reduction in the polymorphic λ-calculus, to prove the termination of various kinds of rewrite relations on λ-terms, including rewriting modulo some equational theory and rewriting with matching modulo βη, by using the notion of computability closure. This provides a powerful termination criterion for various higher-order rewriting frameworks, including Klop's Combinatory Reductions Systems with simple types and Nipkow's Higher-order Rewrite Systems.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2015, 611 (50-86), pp.37. 〈10.1016/j.tcs.2015.07.045〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01191693
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 2 septembre 2015 - 13:04:57
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mercredi 26 avril 2017 - 14:10:32

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Frédéric Blanqui. Termination of rewrite relations on λ-terms based on Girard's notion of reducibility. Theoretical Computer Science, Elsevier, 2015, 611 (50-86), pp.37. 〈10.1016/j.tcs.2015.07.045〉. 〈hal-01191693〉

Partager

Métriques

Consultations de la notice

368

Téléchargements de fichiers

59