Termination and Confluence of Higher-Order Rewrite Systems

Abstract : In the last twenty years, several approaches to higher-order rewriting have been proposed, among which Klop's Combinatory Rewrite Systems (CRSs), Nipkow's Higher-order Rewrite Systems (HRSs) and Jouannaud and Okada's higher-order algebraic specification languages, of which only the last one considers typed terms. The later approach has been extended by Jouannaud, Okada and the present author into Inductive Data Type Systems (IDTSs). In this paper, we extend IDTSs with the CRS higher-order pattern-matching mechanism, resulting in simply-typed CRSs. Then, we show how the termination criterion developed for IDTSs with first-order pattern-matching, called the General Schema, can be extended so as to prove the strong normalization of IDTSs with higher-order pattern-matching. Next, we compare the unified approach with HRSs. We first prove that the extended General Schema can also be applied to HRSs. Second, we show how Nipkow's higher-order critical pair analysis technique for proving local confluence can be applied to IDTSs.
Type de document :
Communication dans un congrès
Rewriting Techniques and Applications, 11th International Conference, RTA 2000, Jul 2000, Norwich, United Kingdom. 1833, 2000, LNCS
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00105556
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 11 octobre 2006 - 15:30:05
Dernière modification le : mardi 24 avril 2018 - 13:38:54
Document(s) archivé(s) le : mardi 6 avril 2010 - 19:22:42

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. Termination and Confluence of Higher-Order Rewrite Systems. Rewriting Techniques and Applications, 11th International Conference, RTA 2000, Jul 2000, Norwich, United Kingdom. 1833, 2000, LNCS. 〈inria-00105556〉

Partager

Métriques

Consultations de la notice

121

Téléchargements de fichiers

96