关于资源lambda演算中测试的区分能力

自发现以来，微分线性逻辑（DLL）启发了众多领域。在指称语义中，DLL的范畴模型现在很常见，最简单的是Rel，即集合与关系的范畴。在证明论中，这自然产生了对DLL完全且完备的微分证明网。反过来，这些工具可以自然地转化为其直觉主义对应物。通过取与!余单子相关的co-Kleisly范畴，Rel成为MRel，一个包含微分概念的\Lcalcul模型。证明网可以自然地用于将\Lcalcul扩展为带资源的lambda演算，这是一种包含线性和微分概念的演算。当然，MRel是带资源的\Lcalcul的一个模型，并且已被证明是充分的，但它是完全抽象的吗？这是Bucciarelli、Carraro、Ehrhard和Manzonetto的一个强猜想。然而，在本文中，我们给出了一个反例。此外，为了更直观地理解反例的本质并寻求更一般性，我们将使用Bucciarelli等人引入的带资源\Lcalcul的一个扩展，对于该扩展，$\Minf$是完全抽象的，即测试。