Abstract:
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 various observation scenarios for this calculus, depending on the way we observe termination, deadlock and divergence. We relate these observational semantics with the intensional interpretation of lambda-terms, by means of Lévy-Longo trees. We show in particular that the inclusion of such trees coincides with the ``flat'' observational semantics, where deadlocks and convergence are distinguished.