Abstract:
(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.