Generalized Connectives for Multiplicative Linear Logic

Acclavio, Matteo; Maieli, Roberto

doi:10.4230/LIPIcs.CSL.2020.6

File

LIPIcs.CSL.2020.6.pdf

Filesize: 0.57 MB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CSL.2020.6
URN: urn:nbn:de:0030-drops-116490

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

Cite AsGet 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

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.

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

References

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.
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.
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.
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.
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.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
Jean-Yves Girard. Multiplicatives. Rendiconti del Seminario Matematico, pages 11-34, 1987.
Jean-Yves Girard. On Geometry of Interaction. In Helmut Schwichtenberg, editor, Proof and Computation, pages 145-191, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg.
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.
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.
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.
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.
Dale Miller and Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science, 474:98-116, 2013.
Robin Milner. Communicating and mobile systems: the Pi-calculus. Cambridge university press, 1999.