An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets

Authors Jules Chouquet, Lionel Vaux Auclair



PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.15.pdf
  • Filesize: 0.55 MB
  • 17 pages

Document Identifiers

Author Details

Jules Chouquet
  • IRIF UMR 8243, Université Paris Diderot, Sorbonne Paris Cité, CNRS, France
Lionel Vaux Auclair
  • Aix-Marseille Univ, CNRS, Centrale Marseille, I2M, Marseille, France

Cite AsGet BibTex

Jules Chouquet and Lionel Vaux Auclair. An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.15

Abstract

We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose some constraint on switching paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction. Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative exponential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfy our constraints. In the present work, we stick to the unit-free and weakening-free fragment of linear logic, which is rich enough to showcase our techniques, while allowing for a very simple kind of constraint: a bound on the number of cuts that are crossed by any switching path.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
Keywords
  • linear logic
  • proof nets
  • cut elimination
  • differential linear logic

Metrics

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

References

  1. Jules Chouquet, Giulio Guerrieri, Luc Pellissier, and Lionel Vaux. Normalization by evaluation in linear logic. In Stefano Guerrini, editor, Preproceedings of the International Workshop on Trends in Linear Logic and Applications, TLLA, 2017. Google Scholar
  2. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Inf. Comput., 209(6):966-991, 2011. URL: http://dx.doi.org/10.1016/j.ic.2011.02.001.
  3. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Arch. Math. Log., 28(3):181-203, 1989. Google Scholar
  4. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. PhD thesis, Université d'Aix-Marseille II, Marseille, France, 2007. Google Scholar
  5. Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251, 2009. URL: http://arxiv.org/abs/0905.4251.
  6. Daniel de Carvalho. The relational model is injective for multiplicative exponential linear logic. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, 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. 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.
  8. Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 15(4):615-646, 2005. URL: http://dx.doi.org/10.1017/S0960129504004645.
  9. Thomas Ehrhard. A finiteness structure on resource terms. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 402-410, 2010. Google Scholar
  10. Thomas Ehrhard. A new correctness criterion for MLL proof nets. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 38:1-38:10, 2014. Google Scholar
  11. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. CoRR, abs/1606.01642, 2016. Google Scholar
  12. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003. Google Scholar
  13. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Electr. Notes Theor. Comput. Sci., 123:35-74, 2005. Google Scholar
  14. Thomas Ehrhard and Laurent Regnier. Uniformity and the taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008. Google Scholar
  15. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  16. Jean-Yves Girard. Normal functors, power series and lambda-calculus. Annals of Pure and Applied Logic, 37(2):129, 1988. Google Scholar
  17. 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, June 22-26, 2016, Porto, Portugal, pages 20:1-20:18, 2016. Google Scholar
  18. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 301-310. IEEE Computer Society, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.36.
  19. Michele Pagani and Christine Tasson. The inverse taylor expansion problem in linear logic. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 222-231, 2009. Google Scholar
  20. Michele Pagani, Christine Tasson, and Lionel Vaux. Strong normalizability as a finiteness structure via the taylor expansion of lambda-terms. In Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 408-423, 2016. Google Scholar
  21. Laurent Regnier. Lambda-calcul et réseaux. PhD thesis, Université Paris 7, Paris, France, 1992. Google Scholar
  22. Christine Tasson. Sémantiques et syntaxes vectorielles de la logique linéaire. PhD thesis, Université Paris Diderot, Paris, France, Dec 2009. Google Scholar
  23. Lionel Vaux. Taylor expansion, β-reduction and normalization. In 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, pages 39:1-39:16, 2017. 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