Term collection in lambda/rho-calculi - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2007

Term collection in lambda/rho-calculi

Résumé

The ρ-calculus generalises term rewriting and the λ-calculus by defining abstractions on arbitrary patterns and by using a pattern-matching algorithm which is a parameter of the calculus. In particular, equational theories that do not have unique principal solutions may be used. In the latter case, all the principal solutions of a matching problem are stored in a “structure” that can also be seen as a collection of terms. Motivated by the fact that there are various approaches to the definition of structures in the ρ-calculus, we study in this paper a version of the λ-calculus with term collections. The contributions of this work include a new syntax and operational semantics for a λ-calculus with term collections, which is related to the λ-calculi with strict parallel functions studied by Boudol and Dezani et al. and a proof of the confluence of the β-reduction relation defined for the calculus (which is a suitable extension of the standard rule of β-reduction in the λ-calculus).
Fichier principal
Vignette du fichier
dcm06.pdf (193.34 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

inria-00102993 , version 1 (08-11-2007)

Identifiants

  • HAL Id : inria-00102993 , version 1

Citer

Germain Faure. Term collection in lambda/rho-calculi. 2nd International Workshop on Developments in Computational Models - DCM 2006, Jul 2006, Venise, Italy. pp.3-19. ⟨inria-00102993⟩
159 Consultations
72 Téléchargements

Partager

Gmail Facebook X LinkedIn More