Approximation theory for distant Bang calculus

TL;DR

This paper develops a unified approximation semantics framework for the Bang-calculus, encompassing both Call-by-Name and Call-by-Value strategies through B"ohm trees and Taylor expansion.

Contribution

It introduces the approximation semantics for dBang, integrating and generalizing existing semantics for different evaluation strategies within a single framework.

Findings

Defined B"ohm trees and Taylor expansion in dBang.

Established fundamental properties of the approximation semantics.

Unified semantics subsuming Call-By-Name and Call-By-Value.

Abstract

Approximation semantics capture the observable behaviour of {\lambda}-terms, with B\"ohm 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\"ohm tree. These notions are well understood in Call-by-Name {\lambda}-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\"ohm 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.