THE DISCRIMINATING POWER OF MULTIPLICITIES IN THE LAMBDA-CALCULUS

The lambda-calculus with multiplicities is a refinement of the lazy la mbda-calculus where the argument in an application comes with a multip licity, which is an upper bound to the number of its uses. This introd uces potential deadlocks in the evaluation. We study the discriminatin g power of this calculus over the usual lambda-terms. We prove in part icular that the observational equivalence induced by contexts with mul tiplicities coincides with the equality of Levy-Longo trees associated with lambda-terms. This is a consequence of the characterization we g ive of the corresponding observational precongruence, as an intensiona l preorder involving eta-expansion, namely, Ong's lazy Plotkin-Scott-E ngeler preorder. (C) 1996 Academic Press, Inc.