Document Open Access Logo

Glueability of Resource Proof-Structures: Inverting the Taylor Expansion

Authors Giulio Guerrieri , Luc Pellissier , Lorenzo Tortora de Falco

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.24.pdf
  • Filesize: 0.87 MB
  • 18 pages

Document Identifiers

Author Details

Giulio Guerrieri
  • University of Bath, Department of Computer Science, Bath, UK
Luc Pellissier
  • Université de Paris, IRIF, CNRS, F-75013 Paris, France
Lorenzo Tortora de Falco
  • Università Roma Tre, Dipartimento di Matematica e Fisica, Rome, Italy

Funding

  • Guerrieri, Giulio: EPSRC grant EP/R029121/1 "Typed Lambda-Calculi with Sharing and Unsharing"
  • Pellissier, Luc: French ANR project Rapido (ANR-14-CE35-0007)

Cite As Get BibTex

Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Glueability of Resource Proof-Structures: Inverting the Taylor Expansion. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.24

Abstract

A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
Keywords
  • linear logic
  • Taylor expansion
  • proof-net
  • natural transformation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Denis Béchet. Minimality of the correctness criterion for multiplicative proof nets. Mathematical Structures in Computer Science, 8(6):543-558, 1998. URL: http://journals.cambridge.org/action/displayAbstract?aid=44779.
  2. Dennis V. Borisov and Yuri I. Manin. Generalized Operads and Their Inner Cohomomorphisms, volume 265 of Progress in Mathematics, pages 247-308. Birkhäuser Basel, Basel, 2007. URL: http://dx.doi.org/10.1007/978-3-7643-8608-5_4.
  3. Pierre Boudes. Thick Subtrees, Games and Experiments. In Typed Lambda Calculi and Applications, 9th International Conference (TLCA 2009), volume 5608 of Lecture Notes in Computer Science, pages 65-79. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02273-9_7.
  4. Pierre Boudes, Fanny He, and Michele Pagani. A characterization of the Taylor expansion of lambda-terms. In Computer Science Logic 2013 (CSL 2013), volume 23 of LIPIcs, pages 101-115. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.101.
  5. Gérard Boudol. The Lambda-Calculus with Multiplicities (Abstract). In 4th International Conference on Concurrency Theory (CONCUR '93), volume 715 of Lecture Notes in Computer Science, pages 1-6. Springer, 1993. URL: http://dx.doi.org/10.1007/3-540-57208-2_1.
  6. Daniel de Carvalho. The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In 25th Annual Conference on Computer Science Logic (CSL 2016), volume 62 of LIPIcs, pages 41:1-41:19. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.41.
  7. Daniel de Carvalho. Taylor expansion in linear logic is invertible. Logical Methods in Computer Science, 14(4), 2018. URL: http://dx.doi.org/10.23638/LMCS-14(4:21)2018.
  8. Daniel de Carvalho and Lorenzo Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakenings). Annals of Pure and Applied Logic, 163(9):1210-1236, 2012. URL: http://dx.doi.org/10.1016/j.apal.2012.01.004.
  9. Thomas Ehrhard. On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science, 12(5):579-623, 2002. URL: http://dx.doi.org/10.1017/S0960129502003729.
  10. Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 15(4):615-646, 2005. URL: http://dx.doi.org/10.1017/S0960129504004645.
  11. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003. URL: http://dx.doi.org/10.1016/S0304-3975(03)00392-X.
  12. Thomas Ehrhard and Laurent Regnier. Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms. In Second Conference on Computability in Europe (CiE 2006), volume 3988 of Lecture Notes in Computer Science, pages 186-197. Springer, 2006. URL: http://dx.doi.org/10.1007/11780342_20.
  13. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166-195, 2006. URL: http://dx.doi.org/10.1016/j.tcs.2006.08.003.
  14. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2-3):347-372, 2008. URL: http://dx.doi.org/10.1016/j.tcs.2008.06.001.
  15. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  16. Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), volume 52 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.20.
  17. Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Glueability of resource proof-structures: inverting the Taylor expansion (long version). CoRR, abs/1910.07936, 2019. URL: http://arxiv.org/abs/1910.07936.
  18. Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Proof-Net as Graph, Taylor Expansion as Pullback. In Logic, Language, Information, and Computation - 26th International Workshop (WoLLIC 2019), volume 11541 of Lecture Notes in Computer Science, pages 282-300. Springer, 2019. URL: http://dx.doi.org/10.1007/978-3-662-59533-6_18.
  19. Emma Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting call-by-value Böhm trees in light of their Taylor expansion. CoRR, abs/1809.02659, 2018. URL: http://arxiv.org/abs/1809.02659.
  20. Giulio Manzonetto and Domenico Ruoppolo. Relational Graph Models, Taylor Expansion and Extensionality. Electronic Notes in Theoretical Compututer Science, 308:245-272, 2014. URL: http://dx.doi.org/10.1016/j.entcs.2014.10.014.
  21. Damiano Mazza and Michele Pagani. The Separation Theorem for Differential Interaction Nets. In Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference (LPAR 2007), volume 4790 of Lecture Notes in Computer Science, pages 393-407. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-75560-9_29.
  22. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. PACMPL, 2(POPL):6:1-6:28, 2018. URL: http://dx.doi.org/10.1145/3158094.
  23. Michele Pagani and Christine Tasson. The Inverse Taylor Expansion Problem in Linear Logic. In 24th Annual Symposium on Logic in Computer Science (LICS 2009), pages 222-231. IEEE Computer Society, 2009. URL: http://dx.doi.org/10.1109/LICS.2009.35.
  24. Michele Pagani, Christine Tasson, and Lionel Vaux. Strong Normalizability as a Finiteness Structure via the Taylor Expansion of λ-terms. In Foundations of Software Science and Computation Structures - 19th International Conference (FOSSACS 2016), volume 9634 of Lecture Notes in Computer Science, pages 408-423. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49630-5_24.
  25. Christian Retoré. A Semantic Characterisation of the Correctness of a Proof Net. Mathematical Structures in Computer Science, 7(5):445-452, 1997. URL: http://dx.doi.org/10.1017/S096012959700234X.
  26. Christine Tasson. Sémantiques et Syntaxes Vectorielles de la Logique Linéaire. PhD thesis, Université Paris Diderot, France, December 2009. URL: https://tel.archives-ouvertes.fr/tel-00440752.
  27. Lionel Vaux. Taylor Expansion, lambda-Reduction and Normalization. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pages 39:1-39:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.39.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact