Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074234
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:49:53 PM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM
Long-term archiving on: : Sunday, April 4, 2010 - 9:25:49 PM

Identifiers

  • HAL Id : inria-00074234, version 1

Collections

Citation

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

Share

Metrics

Record views

189

Files downloads

207