Skip to Main content Skip to Navigation
Reports

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
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00107538
Contributor : Publications Loria <>
Submitted on : Thursday, October 19, 2006 - 9:00:28 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Friday, November 25, 2016 - 12:52:53 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

167

Files downloads

75