Cyclic Multiplicative-Additive Proof Nets of Linear Logic with an Application to Language Parsing

Abstract

This paper concerns a logical approach to natural language parsing based on proof nets (PNs), i.e. de-sequentialized proofs, of linear logic (LL). It first provides a syntax for proof structures (PSs) of the cyclic multiplicative and additive fragment of linear logic (CyMALL). A PS is an oriented graph, weighted by boolean monomial weights, whose conclusions $\varGamma$ are endowed with a cyclic order $\sigma$. Roughly, a PS $\pi$ with conclusions $\sigma (\varGamma )$ is correct (so, it is a proof net), if any slice $\varphi (\pi )$, obtained by a boolean valuation $\varphi$ of $\pi$, is a multiplicative (CyMLL) PN with conclusions $\sigma (\varGamma _r)$, where $\varGamma _r$ is an additive resolution of $\varGamma$, i.e. a choice of an additive subformula for each formula of $\varGamma$. The correctness criterion for CyMLL PNs can be considered as the non-commutative counterpart of the famous Danos-Regnier (DR) criterion for PNs of the pure multiplicative fragment (MLL) of LL. The main intuition relies on the fact that any DR-switching (i.e. any correction or test graph for a given PN) can be naturally viewed as a seaweed, that is, a rootless planar tree inducing a cyclic order on the conclusions of the given PN. Unlike the most part of current syntaxes for non-commutative PNs, our syntax allows a sequentialization for the full class of CyMALL PNs, without requiring these latter to be cut-free.

One of the main contributions of this paper is to provide a characterization of CyMALL PNs for the additive Lambek Calculus and thus a geometrical (non inductive) way to parse sentences containing words with syntactical ambiguity (i.e., with polymorphic type).