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

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

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

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


  • HAL Id : inria-00074234, version 1



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



Record views


Files downloads