A Rho-Calculus of explicit constraint application

Horatiu Cirstea 1 Germain Faure 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Theoretical presentations of the rho-calculus often treat the matching constraint computations as an atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a much more realistic view: computations needed in order to find the solutions of a matching equation can have an important impact on the (efficiency of the) calculus for some matching theories and the substitution application usually involves a term traversal. Following the works on explicit substitutions in the -calculus, we present two versions of the rho-calculus, one with explicit matching and one with explicit substitutions, together with a version that combines the two and considers efficiency issues and more precisely the composition of substitutions. The approach is general, allowing the extension to various matching theories. We establish the confluence of the calculus and the termination of the explicit constraint handling and application sub-calculus.
Type de document :
Article dans une revue
Higher-Order and Symbolic Computation, Springer Verlag, 2007, Special Issue on Rewriting Logic and its Applications, 20, pp.37-72. 〈10.1007/s10990-007-9004-2〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00000628
Contributeur : Germain Faure <>
Soumis le : jeudi 8 novembre 2007 - 10:49:00
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 16:08:39

Fichier

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

Identifiants

Collections

Citation

Horatiu Cirstea, Germain Faure, Claude Kirchner. A Rho-Calculus of explicit constraint application. Higher-Order and Symbolic Computation, Springer Verlag, 2007, Special Issue on Rewriting Logic and its Applications, 20, pp.37-72. 〈10.1007/s10990-007-9004-2〉. 〈inria-00000628v3〉

Partager

Métriques

Consultations de la notice

228

Téléchargements de fichiers

86