Cyclic multiplicative-additive proof nets of linear logic with an application to language parsing

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 Γ are endowed with a cyclic order σ. Roughly, a PS π with conclusions σ(Γ) is correct (so, it is a proof net), if any slice φ(π), obtained by a boolean valuation φ of π, is a multiplicative (CyMLL) PN with conclusions σ(Γr), where Γr is an additive resolution of Γ, i.e. a choice of an additive subformula for each formula of Γ. 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).