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演算，系统构建了逼近语义理论。我们在dBang中定义了Böhm树与泰勒展开式，并建立了它们的基本性质。通过将按名调用与按值调用策略翻译至Bang演算，我们的结果统一并推广了这两类策略，提供了一个能够跨求值策略一致刻画无穷语义与资源敏感语义的单一框架。