Approximation theory for distant Bang calculus
Kostia Chardonnet, Jules Chouquet, Axel Kerinec
TL;DR
This work develops a unified approximation framework for the distance Bang-calculus $dBang$, defining Böhm trees and Taylor expansions to capture infinitary and resource-sensitive semantics across Call-by-Name and Call-by-Value paradigms. It introduces a resource calculus $\delta Bang$ and an approximation relation $\triangleleft_\oc$, proves a Taylor–Böhm commutation theorem, and establishes a simulation between $dBang$ reductions and their Taylor approximants. The paper then transfers these notions to the distant translations of $dCBN$ and $dCBV$ into $dBang$, showing that their Taylor/Böhm approximations are preserved under translation and that meaningfulness corresponds to nonempty Taylor normal forms in these fragments. By providing sound embeddings and a robust semantic bridge, the work unifies infinitary, resource-sensitive semantics for diverse evaluation strategies and lays groundwork for extending meaningfulness to broader proof-structure settings. Overall, it yields a single, coherent framework for approximation semantics that subsumes both CbN and CbV within the Bang-calculus and offers a path toward further connections with proof-net formalisms and related distant calculi.
Abstract
Approximation semantics capture the observable behaviour of λ-terms, with Böhm Trees and Taylor Expansion standing as two central paradigms. Although conceptually different, these notions are related via the Commutation Theorem, which links the Taylor expansion of a term to that of its Böhm tree. These notions are well understood in Call-by-Name λ-calculus and have been more recently introduced in Call-by-Value settings. Since these two evaluation strategies traditionally require separate theories, a natural next step is to seek a unified setting for approximation semantics. The Bang-calculus offers exactly such a framework, subsuming both CbN and CbV through linear-logic translations while providing robust rewriting properties. However, its approximation semantics is yet to be fully developed. In this work, we develop the approximation semantics for dBang, the Bang-calculus with explicit substitutions and distant reductions. We define Böhm trees and Taylor expansion within dBang and establish their fundamental properties. Our results subsume and generalize Call-By-Name and Call-By-Value through their translations into Bang, offering a single framework that uniformly captures infinitary and resource-sensitive semantics across evaluation strategies.