Proof Nets for Multiplicative Cyclic Linear Logic and Lambek Calculus

Autori: Maieli, Roberto; Abrusci, Vito Michele

Editore: Cambridge University Press

Tipologia Prodotto: Articolo in rivista

DOI: 10.1017/S0960129518000300

Titolo della Rivista: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

Numero;Volume: 6; 29

Numero prima e ultima pagina: 733 – 762

Codice ISSN/ISBN/ISMN: 0960-1295 (Stampa) , 1469-8072 (Online)

Anno di Pubblicazione: 2019

Link: https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/proof-nets-for-multiplicative-cyclic-linear-logic-and-lambek-calculus/93844613B0C334AA05AFC5C5192D21EF

Abstract:

This paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic linear logic. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non inductive) way to parse phrases or sentences by means of Lambek proof nets.