HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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).
Document type :
Conference papers
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/inria-00102993
Contributor : Germain Faure Connect in order to contact the contributor
Submitted on : Thursday, November 8, 2007 - 10:45:16 AM
Last modification on : Friday, February 4, 2022 - 3:31:51 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 5:26:05 PM

File

dcm06.pdf
Publisher files allowed on an open archive

Identifiers

  • HAL Id : inria-00102993, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

151

Files downloads

63