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 be really important in some matching theories and the substitution application usually involves a term traversal. Following the works on explicit substitutions in the λ-calculus, we propose, study and exemplify a rho-calculus with explicit constraint handling, up to the level of substitution applications. The approach is general, allowing the extension to various matching theories. We show that the calculus is powerful enough to deal with errors. We establish the confluence of the calculus and the termination of the explicit constraint handling and application sub-calculus.
Type de document :
Communication dans un congrès
Workshop on Rewriting Logic and Applications, Mar 2004, Barcelona (Spain), Spain. 117, 2004, ENTCS
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00095626
Contributeur : Germain Faure <>
Soumis le : lundi 18 septembre 2006 - 09:39:47
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : mardi 6 avril 2010 - 01:00:34

Identifiants

  • HAL Id : inria-00095626, version 1

Collections

Citation

Horatiu Cirstea, Germain Faure, Claude Kirchner. A rho-calculus of explicit constraint application.. Workshop on Rewriting Logic and Applications, Mar 2004, Barcelona (Spain), Spain. 117, 2004, ENTCS. 〈inria-00095626〉

Partager

Métriques

Consultations de la notice

125

Téléchargements de fichiers

63