Title:On the discriminating power of tests in ressource lambda-calculus

Abstract:Since the discovery of the differential linear logic (DLL), it inspired numerous domains. In denotational semantics, categorical models of DLL are now commune, and the simplest one is Rel, the category of sets and relations. In proof theory this naturally gave birth to differential proof nets that are full and complete for DLL. In turn, these tools can naturally be translated to intuitionistic counterpart. By taking the coKleisly category associated to the ! comonade, Rel becomes MRel, a model of the \lambda-calculus that contain a notion of differentiation. And proof nets can be used naturally to extend the \lambda-calculus into the lambda calculus with resources, a calculus that contains notions of linearity and differentiations. Of course MRel is a model of the \lambda-calculus with resources, and it has been proved adequate, but is it fully abstract? That was a strong conjecture of Bucciarelli, Carraro, Ehrhard and Manzonetto in [4]. However, in this paper we exhibit a counter-example. Moreover, to give more intuition on what it does and to look for more generality, we will use an extension of the resource \lambda-calculus also introduced by Bucciarelli et al in [4] for which M\infty is fully abstract, the tests.