DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2024.29

Böhm and Taylor for All!

Authors: Aloÿs Dufour and Damiano Mazza

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

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.

Cite as

Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for All!. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dufour_et_al:LIPIcs.FSCD.2024.29,
  author =	{Dufour, Alo\"{y}s and Mazza, Damiano},
  title =	{{B\"{o}hm and Taylor for All!}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.29},
  URN =		{urn:nbn:de:0030-drops-203582},
  doi =		{10.4230/LIPIcs.FSCD.2024.29},
  annote =	{Keywords: Linear logic, Differential linear logic, Taylor expansion of lambda-terms, B\"{o}hm trees, Process calculi}
}

Search Results

Documents authored by Dufour, Aloÿs

Böhm and Taylor for All!

Abstract

Cite as

Thanks for your feedback!

Could not send message