Term collection in lambda/rho-calculi

Germain Faure 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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).
Type de document :
Communication dans un congrès
Science Direct, Electronic Notes In Theoritical Computer Science. 2nd International Workshop on Developments in Computational Models - DCM 2006, Jul 2006, Venise, Italy. 117, pp.3-19, 2007, Proceedings of the Second International Workshop on Developments in Computational Models (DCM 2006)
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00102993
Contributeur : Germain Faure <>
Soumis le : jeudi 8 novembre 2007 - 10:45:16
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57
Document(s) archivé(s) le : mardi 6 avril 2010 - 17:26:05

Fichier

dcm06.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : inria-00102993, version 1

Collections

Citation

Germain Faure. Term collection in lambda/rho-calculi. Science Direct, Electronic Notes In Theoritical Computer Science. 2nd International Workshop on Developments in Computational Models - DCM 2006, Jul 2006, Venise, Italy. 117, pp.3-19, 2007, Proceedings of the Second International Workshop on Developments in Computational Models (DCM 2006). 〈inria-00102993〉

Partager

Métriques

Consultations de la notice

164

Téléchargements de fichiers

113