The Discriminating Power of Multiplicities in theλ-Calculus

AbstractTheλ-calculus with multiplicities is a refinement of the lazyλ-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λ-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λ-terms. This is a consequence of the characterization we give of the corresponding observational precongruence, as an intensional preorder involvingη-expansion, namely, Ong's lazy Plotkin–Scott–Engeler preorder