(see also RR-2581)
In this paper we study the semantics of the lambda-calculus induced by Milner's encoding into the pi-calculus. We show that the resulting may testing preorder on lambda-terms coincides with the inclusion of Lévy-Longo trees. To establish this result, we use a refinement of the lambda-calculus where the argument of a function may be of limited availability. In our lambda-calculus with multiplicities, evaluation is deterministic, but it may deadlock, due to the lack of resources. We show that this feature is enough to make the lambda-calculus as discriminating as the pi-calculus.