The relational semantics of linear logic is a powerful framework for defining resource-aware models of the $λ$-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between Böhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to provide a quantitative and contextual interpretation of the preorder associated to the relational semantics. This way, we show that the relational semantics refines the contextual preorder constraining the number of interactions between the related terms and the context.

翻译：线性逻辑的关系语义是定义λ演算资源感知模型的强大框架。然而，其定量特性并未体现在这些模型所诱导的预序和等式理论中。事实上，这些理论可以通过外延性下的Böhm树（不）等式来刻画，而后者本质上是定性的。我们利用最近引入的检验器演算，为关系语义关联的预序提供了一种定量且上下文相关的解释。通过这种方式，我们证明了关系语义细化了上下文预序，从而约束了相关项与上下文之间的交互次数。