Document Open Access Logo

Parallelism in Soft Linear Logic

Author Paulin Jacobé de Naurois

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2022.26.pdf
  • Filesize: 0.65 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Complexity theory and logic
Keywords
  • Implicit Complexity
  • Typing
  • Linear Logic
  • Functional Programming

Metrics

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

Abstract

We extend the Soft Linear Logic of Lafont with a new kind of modality, called parallel. Contractions on parallel modalities are only allowed in the cut and the left ⊸ rules, in a controlled, uniformly distributive way. We show that SLL, extended with this parallel modality, is sound and complete for PSPACE. We propose a corresponding typing discipline for the λ-calculus, extending the STA typing system of Gaboardi and Ronchi, and establish its PSPACE soundness and completeness. The use of the parallel modality in the cut-rule drives a polynomial-time, parallel call-by-value evaluation strategy of the terms.

Cite As Get BibTex

Paulin Jacobé de Naurois. Parallelism in Soft Linear Logic. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.26

Author Details

Paulin Jacobé de Naurois
  • CNRS, Université Paris 13, Sorbonne Paris Cité, LIPN, UMR 7030, F-93430 Villetaneuse, France

Funding

  • Jacobé de Naurois, Paulin: ANR project ELICA - ANR-14-CE25-0005.

References

  1. Patrick Baillot and Virgile Mogbil. Soft lambda-calculus: A language for polynomial time computation. In Igor Walukiewicz, editor, FoSSaCS, volume 2987 of Lecture Notes in Computer Science, pages 27-41. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24727-2_4.
  2. Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda calculus. Information and Computation, 207(1):41-62, January 2009. URL: https://doi.org/10.1016/j.ic.2008.08.005.
  3. Stephen Bellantoni and Stephen A. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97-110, 1992. Google Scholar
  4. Guillaume Bonfante, Reinhard Kahle, Jean-Yves Marion, and Isabel Oitavem. Two function algebras defining functions in NC^k boolean circuits. Inf. Comput., 248:82-103, 2016. URL: https://doi.org/10.1016/j.ic.2015.12.009.
  5. Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca. A logical account of pspace. In George C. Necula and Philip Wadler, editors, POPL, pages 121-131. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328456.
  6. Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca. An implicit characterization of PSPACE. ACM Transactions on Computational Logic, 13(2):1-36, April 2012. URL: https://doi.org/10.1145/2159531.2159540.
  7. Marco Gaboardi and Simona Ronchi Della Rocca. A soft type assignment system for ambda -calculus. In Jacques Duparc and Thomas A. Henzinger, editors, CSL, volume 4646 of Lecture Notes in Computer Science, pages 253-267. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_21.
  8. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  9. Jean-Yves Girard. Light linear logic. Inf. Comput., 143(2):175-204, 1998. Google Scholar
  10. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1):1-66, 1992. Google Scholar
  11. Paulin Jacobé De Naurois. Pointers in recursion: Exploring the tropics. In FSCD, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2019. URL: https://doi.org/10.4230/LIPICS.FSCD.2019.29.
  12. Satoru Kuroda. Recursion schemata for slowly growing depth circuit classes. Computational Complexity, 13(1-2):69-89, 2004. URL: https://doi.org/10.1007/s00037-004-0184-4.
  13. Yves Lafont. Soft linear logic and polynomial time. Theor. Comput. Sci., 318(1-2):163-180, 2004. URL: https://doi.org/10.1016/j.tcs.2003.10.018.
  14. Ugo Dal Lago and Martin Hofmann. Bounded linear logic, revisited. Logical Methods in Computer Science, 6(4), December 2010. URL: https://doi.org/10.2168/lmcs-6(4:7)2010.
  15. Ugo Dal Lago and Ulrich Schöpp. Functional programming in sublinear space. In Programming Languages and Systems, pages 205-225. Springer Berlin Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-11957-6_12.
  16. Daniel Leivant and Jean-Yves Marion. Ramified recurrence and computational complexity ii: Substitution and poly-space. In Leszek Pacholski and Jerzy Tiuryn, editors, CSL, volume 933 of Lecture Notes in Computer Science, pages 486-500. Springer, 1994. URL: https://doi.org/10.1007/BFb0022242.
  17. Ulrich Schöpp. Stratified bounded affine logic for logarithmic space. In LICS, pages 411-420. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.45.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact