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öhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on \(\lambda \) -terms, and demonstrate that it coincides with the preorder associated to the relational semantics.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Interaction Improvement

  • Adrienne Lancelot,
  • Giulio Manzonetto,
  • Guy McCusker,
  • Gabriele Vanoni

摘要

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öhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on \(\lambda \) -terms, and demonstrate that it coincides with the preorder associated to the relational semantics.