Traduction des Combinatory Reduction Systems en Rho-Calcul

Clara Bertolissi 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Les "Combinatory Reduction Systems" sont des systèmes de réécriture d'ordre supérieur étendant les systèmes de réécriture du premier ordre par un mécanisme de liaison de variables. D'un autre côté, la réécriture et le lambda-calcul ont été généralisés dans le calcul de réécriture et il est donc naturel de se demander quelle est la relation entre les deux formalismes : les systèmes de réécriture d'ordre supérieur et le rho-calcul. Nous avons analysé cette correspondance et nous présentons une fonction de traduction entre les termes CRS et les termes du rho-calcul. Nous montrons que cette traduction permet d'exprimer les réduction des termes CRS dans le rho-calcul. || The higher order rewrite systems known as Combinatory Reduction systems (CRS), introduced by J.W.Klop, are an extension of first order rewrite systems by a mechanism allowing the binding of variables. On the other side, first order rewriting and lambda c
Type de document :
Rapport
[Stage] A02-R-497 || bertolissi02a, 2002, 39 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00099419
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:02:52
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 11:50:34

Fichiers

Identifiants

  • HAL Id : inria-00099419, version 1

Collections

Citation

Clara Bertolissi. Traduction des Combinatory Reduction Systems en Rho-Calcul. [Stage] A02-R-497 || bertolissi02a, 2002, 39 p. 〈inria-00099419〉

Partager

Métriques

Consultations de la notice

61

Téléchargements de fichiers

28