HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information

# The discriminating power of multiplicities in the $\lambda$-calculus

1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : The $\lambda$-calculus with multiplicities is a refinement of the lazy $\lambda$-calculus where the argument in an application comes with a multiplicity, which is an upper bound to the number of its uses. This introduces potential deadlocks in the evaluation. We study the discriminating power of this calculus over the usual $\lambda$-terms. We prove in particular that the observational equivalence induced by contexts with multiplicities coincides with the equality of Lévy-Longo trees associated with $\lambda$-terms. This is a consequence of the characterization we give of the corresponding observational precongruence, as an intensional preorder involving $\eta$-expansion, namely Ong's lazy Plotkin-Scott-Engeler preorder.
keyword :
Document type :
Reports
Domain :
Complete list of metadata

https://hal.inria.fr/inria-00074234
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:49:53 PM
Last modification on : Friday, February 4, 2022 - 3:23:28 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:25:49 PM

### Identifiers

• HAL Id : inria-00074234, version 1

### Citation

Gérard Boudol, Laneve Cosimo. The discriminating power of multiplicities in the $\lambda$-calculus. [Research Report] RR-2441, INRIA. 1994. ⟨inria-00074234⟩

Record views