标题： 远距离Bang微积分的逼近理论 显示英文标题

标题： Approximation theory for distant Bang calculus

摘要： 近似语义捕捉λ-terms的可观测行为，Böhm树和泰勒展开作为两个核心范式。 尽管概念不同，这些概念通过交换定理相关联，该定理将一个项的泰勒展开与其Böhm树的展开联系起来。 这些概念在按名调用λ-演算中已被很好地理解，并且最近被引入到按值调用的环境中。 由于这两种求值策略传统上需要单独的理论，下一步自然是要寻找一个统一的近似语义设置。 Bang-演算正好提供了这样的框架，通过线性逻辑翻译涵盖了CbN和CbV，同时提供了强大的重写性质。 然而，其近似语义尚未完全开发。 在本工作中，我们开发了dBang的近似语义，即具有显式替换和远距离归约的Bang-演算。 我们在dBang中定义了Böhm树和泰勒展开，并建立了它们的基本性质。 我们的结果通过将其翻译到Bang中，概括并推广了按名调用和按值调用，提供了一个统一的框架，能够统一地捕捉各种求值策略中的无限和资源敏感语义。 显示英文摘要

摘要： 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.