Confluence of Pattern-Based Calculi

Horatiu Cirstea 1 Germain Faure 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Different pattern calculi integrate the functional mechanisms from the lambda-calculus and the matching capabilities from rewriting. Several approaches are used to obtain the confluence but in practice the proof methods share the same structure and each variation on the way pattern-abstractions are applied needs another proof of confluence. We propose here a generic confluence proof where the way pattern-abstractions are applied is axiomatized. Intuitively, the conditions guarantee that the matching is stable by substitution and by reduction. We show that our approach directly applies to different pattern calculi, namely the lambda calculus with patterns, the pure pattern calculus and the rewriting calculus. We also characterize a class of matching algorithms and consequently of pattern-calculi that are not confluent.
Type de document :
Communication dans un congrès
Franz Baader. 18th International Conference on Term Rewriting and Applications - RTA 2007, Jun 2007, Paris, France. Springer Berlin / Heidelberg, 4533, pp.78-92, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-73449-9_8〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00185882
Contributeur : Horatiu Cirstea <>
Soumis le : mercredi 7 novembre 2007 - 14:23:22
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Lien texte intégral

Identifiants

Collections

Citation

Horatiu Cirstea, Germain Faure. Confluence of Pattern-Based Calculi. Franz Baader. 18th International Conference on Term Rewriting and Applications - RTA 2007, Jun 2007, Paris, France. Springer Berlin / Heidelberg, 4533, pp.78-92, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-73449-9_8〉. 〈inria-00185882〉

Partager

Métriques

Consultations de la notice

139