Document

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

## File

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

## Cite As

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

## 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.
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.
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.
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.
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.
11. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. CoRR, abs/1606.01642, 2016.
12. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003.
13. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Electr. Notes Theor. Comput. Sci., 123:35-74, 2005.
14. Thomas Ehrhard and Laurent Regnier. Uniformity and the taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008.
15. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987.
16. Jean-Yves Girard. Normal functors, power series and lambda-calculus. Annals of Pure and Applied Logic, 37(2):129, 1988.
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.
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.
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.
21. Laurent Regnier. Lambda-calcul et réseaux. PhD thesis, Université Paris 7, Paris, France, 1992.
22. Christine Tasson. Sémantiques et syntaxes vectorielles de la logique linéaire. PhD thesis, Université Paris Diderot, Paris, France, Dec 2009.
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.