Document Open Access Logo

Generalized Connectives for Multiplicative Linear Logic

Authors Matteo Acclavio , Roberto Maieli

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2020.6.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
Keywords
  • Linear Logic
  • Partitions Sets
  • Proof Nets
  • Sequent Calculus

Metrics

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

Abstract

In this paper we investigate the notion of generalized connective for multiplicative linear logic. We introduce a notion of orthogonality for partitions of a finite set and we study the family of connectives which can be described by two orthogonal sets of partitions.
We prove that there is a special class of connectives that can never be decomposed by means of the multiplicative conjunction ⊗ and disjunction ⅋, providing an infinite family of non-decomposable connectives, called Girard connectives. We show that each Girard connective can be naturally described by a type (a set of partitions equal to its double-orthogonal) and its orthogonal type. In addition, one of these two types is the union of the types associated to a family of MLL-formulas in disjunctive normal form, and these formulas only differ for the cyclic permutations of their atoms.

Cite As Get BibTex

Matteo Acclavio and Roberto Maieli. Generalized Connectives for Multiplicative Linear Logic. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.6

Author Details

Matteo Acclavio
  • Samovar, UMR 5157 Télécom SudParis and CNRS, 9 rue Charles Fourier, 91011 Évry, France
Roberto Maieli
  • Mathematics & Physics Department, Roma Tre University, L.go S. L. Murialdo 1, 00146 Rome, Italy

References

  1. V. Michele Abrusci and Roberto Maieli. Proof nets for multiplicative cyclic linear logic and Lambek calculus. Mathematical Structures in Computer Science, 29(6):733–762, 2019. URL: https://doi.org/10.1017/S0960129518000300.
  2. Jean-Marc Andreoli. Focussing and proof construction. Annals of Pure and Applied Logic, 107(1):131-163, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00032-4.
  3. Jean-Marc Andreoli and Laurent Mazaré. Concurrent construction of proof-nets. In International Workshop on Computer Science Logic, pages 29-42. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45220-1_3.
  4. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics in multiplicative-additive linear logic. Annals of Pure and Applied Logic, 102(3):247-282, 2000. URL: https://doi.org/10.1016/S0168-0072(00)00056-7.
  5. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical logic, 28(3):181-203, 1989. URL: https://doi.org/10.1007/BF01622878.
  6. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  7. Jean-Yves Girard. Multiplicatives. Rendiconti del Seminario Matematico, pages 11-34, 1987. Google Scholar
  8. Jean-Yves Girard. On Geometry of Interaction. In Helmut Schwichtenberg, editor, Proof and Computation, pages 145-191, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  9. Jean-Yves Girard. On the meaning of logical rules II: multiplicatives and additives. NATO ASI Series F Computer and Systems Sciences, 175:183-212, 2000. Google Scholar
  10. Roberto Maieli. Construction of Retractile Proof Structures. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi, pages 319-333. Springer International Publishing, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_22.
  11. Roberto Maieli. Non decomposable connectives of linear logic. Annals of Pure and Applied Logic, 170(11):102709, 2019. URL: https://doi.org/10.1016/j.apal.2019.05.006.
  12. Roberto Maieli and Quintijn Puite. Modularity of proof-nets. Archive for Mathematical Logic, 44(2):167-193, 2005. URL: https://doi.org/10.1007/s00153-004-0242-2.
  13. Dale Miller and Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science, 474:98-116, 2013. Google Scholar
  14. Robin Milner. Communicating and mobile systems: the Pi-calculus. Cambridge university press, 1999. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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