Document Open Access Logo

Computing Connected Proof(-Structure)s From Their Taylor Expansion

Authors Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.20.pdf
  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Author Details

Giulio Guerrieri
Luc Pellissier
Lorenzo Tortora de Falco

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.20

Abstract

We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational model is injective with respect to connected MELL proof-structures.
Keywords
  • proof-nets
  • (differential) linear logic
  • relational model
  • Taylor expansion

Metrics

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

References

  1. V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical logic, 28(3):181-203, 1989. Google Scholar
  2. V. Danos and L. Regnier. Proof-nets and the Hilbert space. In Advances in Linear Logic, pages 307-328. Cambridge University Press, 1995. Google Scholar
  3. D. de Carvalho. The relational model is injective for Multiplicative Exponential Linear Logic. Preprint available at http://arxiv.org/abs/1502.02404, April 2015.
  4. D. de Carvalho, M. Pagani, and L. Tortora de Falco. A semantic measure of the execution time in Linear Logic. Theoretical Computer Science, 412(20):1884-1902, 2011. Google Scholar
  5. D. de Carvalho and L. Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakening). Ann. Pure Appl. Logic, 163(9):1210-1236, 2012. Google Scholar
  6. T. Ehrhard. Finiteness spaces. Math. Struct. Comp. Science, 15(4):615-646, 2005. Google Scholar
  7. T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003. Google Scholar
  8. T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166-195, 2006. Google Scholar
  9. T. Ehrhard and L. Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2-3):347-372, 2008. Google Scholar
  10. H. Friedman. Equality between functionals. In Rohit Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 22-37. Springer Berlin, 1975. Google Scholar
  11. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. Google Scholar
  12. G. Guerrieri, L. Pellissier, and L. Tortora de Falco. Syntax, Taylor expansion and relational semantics of MELL proof-structures: an unusual approach. Technical report, 2016. Available at URL: http://logica.uniroma3.it/~tortora/mell.pdf.
  13. Y. Lafont. From Proof-Nets to Interaction Nets. In Advances in Linear Logic, pages 225-247. Cambridge University Press, 1995. Google Scholar
  14. O. Laurent. Polarized proof-nets and λμ-calculus. Theor. Comp. Sci., 290(1):161-188, 2003. Google Scholar
  15. D. Mazza and M. Pagani. The Separation Theorem for Differential Interaction Nets. In Proceedings of LPAR 2007, pages 393-407, 2007. Google Scholar
  16. M. Pagani. The Cut-Elimination Thereom for Differential Nets with Boxes. In Proceedings of TLCA 2009, pages 219-233, 2009. Google Scholar
  17. M. Pagani and C. Tasson. The Taylor Expansion Inverse Problem in Linear Logic. In Proceedings of LICS 2009, pages 222-231, 2009. Google Scholar
  18. R. Statman. Completeness, invariance and λ-definability. J. Symb. Logic, 47(1):17-26, 1982. Google Scholar
  19. L. Tortora de Falco. Obsessional Experiments For Linear Logic Proof-Nets. Mathematical Structures in Computer Science, 13(6):799-855, December 2003. Google Scholar
  20. P. Tranquilli. Intuitionistic differential nets and lambda-calculus. Theoretical Computer Science, 412(20):1979-1997, 2011. Google Scholar
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 Imprint Privacy Contact