Encoding rewriting strategies in lambda-calculi with patterns

Germain Faure 1, 2
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We propose a patch to the pure pattern calculus: we claim that this is strictly more powerful to define the application of the match fail as the pure \lambda-term defining the boolean false instead of the identity function as it is done in the original version of the pure pattern calculus~\cite{JayK09}. We show that using non algebraic patterns we are able to encode in a natural way any rewriting strategies as well as the branching construct | used in functional programming languages. We close the open question (raised in~\cite{Cirstea00,CirsteaK01}) whether rewriting strategies can be directly encoded in lambda-calculi with patterns.
Type de document :
Rapport
[Research Report] RR-7025, INRIA. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00413178
Contributeur : Germain Faure <>
Soumis le : jeudi 3 septembre 2009 - 17:23:15
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : samedi 26 novembre 2016 - 12:09:28

Fichier

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

Identifiants

  • HAL Id : inria-00413178, version 2

Collections

Citation

Germain Faure. Encoding rewriting strategies in lambda-calculi with patterns. [Research Report] RR-7025, INRIA. 2009. 〈inria-00413178v2〉

Partager

Métriques

Consultations de la notice

229

Téléchargements de fichiers

82