Term Collections in λ and ρ-calculi
Germain Faure · Electronic Notes in Theoretical Computer Science · 2007
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).