Etude des propriétés du calcul de réécriture: du rho calcul au rhoEpsilon calcul

Germain Faure 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Le \roCal\ intégre dans un cadre uniforme et simple la réécriture du premier ordre et le lambda-calcul tout en permettant d'exprimer le non-déterminisme. Nous introduisons ici un nouveau calcul dans lequel l'échec est distingué de l'ensemble vide et dans lequel le test de l'échec est possible. Si nous munissons ce calcul de l'appel par valeur, nous obtenons un calcul confluent et dans lequel le first est exprimable (et par conséquent les stratégies d'évaluation le sont aussi). Nous concluons sur un bref aperçu des perspectives et des questions restant ouvertes. || The rho-calculus integrates in a uniform and simple setting first-order rewriting, lambda-calculus and non-deterministic computations. In the calculus here introduced, the empty set is not an overloading term i.e. failure is distinguished from the emptys
Type de document :
Rapport
[Stage] A01-R-389 || faure01a, 2001, 65 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00107538
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 09:00:28
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 12:52:53

Identifiants

  • HAL Id : inria-00107538, version 1

Collections

Citation

Germain Faure. Etude des propriétés du calcul de réécriture: du rho calcul au rhoEpsilon calcul. [Stage] A01-R-389 || faure01a, 2001, 65 p. 〈inria-00107538〉

Partager

Métriques

Consultations de la notice

143

Téléchargements de fichiers

40