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.
Type de document :
Rapport
[Research Report] RR-2441, INRIA. 1994
Liste complète des métadonnées

https://hal.inria.fr/inria-00074234
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:49:53
Dernière modification le : samedi 27 janvier 2018 - 01:31:00
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:25:49

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

89