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.

翻译：逼近语义捕捉了λ项的可观测行为，其中Böhm树和泰勒展开是两个核心范式。尽管概念上不同，这些概念通过交换定理相互关联，该定理将项的泰勒展开与其Böhm树的泰勒展开联系起来。这些概念在按名调用λ演算中已得到充分理解，最近也被引入按值调用场景。由于这两种求值策略传统上需要各自独立的理论，自然的下一步是寻求逼近语义的统一框架。Bang演算恰好提供了这样的框架，通过线性逻辑翻译同时涵盖按名调用和按值调用，并具备稳健的重写性质。然而，其逼近语义尚未得到充分发展。本文针对dBang（具有显式替换和远距离归约的Bang演算）发展了逼近语义。我们在dBang中定义了Böhm树和泰勒展开，并建立了它们的基本性质。通过将按名调用和按值调用翻译到Bang演算，我们的结果统一涵盖并推广了这两种策略，提供了一个能跨求值策略一致捕获无穷语义和资源敏感语义的单一框架。