2026-07-22T01:32:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20358 2024-07-05T06:20:34Z ddc:004 open_access

Böhm and Taylor for All! Dufour, Aloÿs Mazza, Damiano Linear logic Differential linear logic Taylor expansion of lambda-terms Böhm trees Process calculi Böhm approximations, used in the definition of Böhm trees, are a staple of the semantics of the lambda-calculus. Introduced more recently by Ehrhard and Regnier, Taylor approximations provide a quantitative account of the behavior of programs and are well-known to be connected to intersection types. The key relation between these two notions of approximations is a commutation theorem, roughly stating that Taylor approximations of Böhm trees are the same as Böhm trees of Taylor approximations. Böhm and Taylor approximations are available for several variants or extensions of the lambda-calculus and, in some cases, commutation theorems are known. In this paper, we define Böhm and Taylor approximations and prove the commutation theorem in a very general setting. We also introduce (non-idempotent) intersection types at this level of generality. From this, we show how the commutation theorem and intersection types may be applied to any calculus embedding in a sufficiently nice way into our general calculus. All known Böhm-Taylor commutation theorems, as well as new ones, follow by this uniform construction. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Aloÿs Dufour and Damiano Mazza 2024 Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2024.29 urn:nbn:de:0030-drops-203582 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.29 eng https://creativecommons.org/licenses/by/4.0/legalcode