2026-07-21T15:08:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26361 2026-07-15T06:01:56Z ddc:004 open_access

Approximation Theory for Distant Bang Calculus Chardonnet, Kostia Chouquet, Jules Kerinec, Axel Lambda-calculus Böhm Trees Taylor expansion of lambda-terms Approximation semantics capture the observable behaviour of λ-terms. Böhm Trees and Taylor Expansion are its two central paradigms, related by the Commutation Theorem. While these notions are well understood in Call-by-Name (CbN), they have only recently been developed for Call-by-Value (CbV), which motivate the search for a unified approximation framework. The Bang-calculus provides such a framework: it subsumes both CbN and CbV through linear-logic translations and enjoys robust rewriting properties. We develop the approximation semantics of dBang (the Bang-calculus with explicit substitutions and distant reductions) by introducing approximation trees in the Böhm tradition together with Taylor expansion. We establish their fundamental properties, including a commutation theorem. Via translations, our results recover the CbN and CbV cases within a single unifying framework capturing infinitary and resource-sensitive semantics. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kostia Chardonnet and Jules Chouquet and Axel Kerinec 2026 Is Part Of LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2026.11 urn:nbn:de:0030-drops-263612 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.11 eng https://creativecommons.org/licenses/by/4.0/legalcode