The discriminating power of multiplicities in the lambda-calculus, with C. Laneve, in Information and Computation Vol. 126, No. 1 (1996), 83-102.

Abstract: (see also RR-2441)
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 extensional preorder involving eta-expansion, namely Ong's lazy Plotkin-Scott-Engeler preorder.