Interaction Improvement

TL;DR

This paper introduces a quantitative interpretation of relational semantics in linear logic, refining the contextual preorder by measuring the number of interactions between terms and contexts.

Contribution

It employs the checkers calculus to provide a new quantitative, contextual perspective on relational semantics in resource-aware models of the lambda calculus.

Findings

Relational semantics can be refined to account for interaction counts.

The checkers calculus enables a quantitative interpretation of preorders.

The approach constrains the number of interactions between terms and contexts.

Abstract

The relational semantics of linear logic is a powerful framework for defining resource-aware models of the $\lambda$-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\"ohm 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.