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.

翻译：线性逻辑的关系语义学是定义$\lambda$-演算资源感知模型的强大框架。然而，其定量方面并未反映在这些模型所诱导的预序和等式理论中。实际上，这些模型可以通过基于外延性的Böhm树之间的（不）等式来刻画，而这种刻画本质上是定性的。我们采用最近引入的检查器演算，为关系语义学关联的预序提供定量且语境化的解释。通过这种方式，我们证明关系语义学通过约束相关项与语境之间的交互次数，细化了语境化预序。