On the discriminating power of tests in resource lambda-calculus

Since its discovery, differential linear logic (DLL) 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 their intuitionistic counterpart. By taking the co-Kleisly category associated to the $!$ comonad, Rel becomes MRel, a model of the \Lcalcul that contains a notion of differentiation. Proof nets can be used naturally to extend the \Lcalcul into the lambda calculus with resources, a calculus that contains notions of linearity and differentiations. Of course MRel is a model of the \Lcalcul 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 \cite{BCEM11}. However, in this paper we exhibit a counter-example. Moreover, to give more intuition on the essence of the counter-example and to look for more generality, we will use an extension of the resource \Lcalcul also introduced by Bucciarelli {\em et al} in \cite{BCEM11} for which $\Minf$ is fully abstract, the tests.

Data and Resources

Additional Info

Field Value
Source https://hal.science/hal-00698609
Author Breuvart, Flavien
Maintainer CCSD
Last Updated May 17, 2026, 13:02 (UTC)
Created May 17, 2026, 13:02 (UTC)
Identifier hal-00698609
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Preuves, Programmes et Systèmes (PPS) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)
creator Breuvart, Flavien
date 2012-05-16T00:00:00
harvest_object_id 360760da-fd9d-4bbe-9474-054485d136ee
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2023-03-24T00:00:00
relation info:eu-repo/semantics/altIdentifier/arxiv/1205.4691
set_spec type:UNDEFINED