Computational Coverage of TLG: Nonlinearity

TL;DR

This paper explores nonlinear connectives in Type Logical Grammar, introducing four conservative extensions of the displacement calculus with brackets that incorporate exponential modalities from linear logic, tailored for linguistic applications.

Contribution

It introduces four new calculi extending displacement calculus with exponential modalities, providing a Curry-Howard labelling, and proves cut-elimination and decidability results for these systems.

Findings

Controlled contraction accounts for parasitic gaps.

Controlled Mingle allows iterated coordination.

Calculi are proven to be cut-free and decidable in certain cases.

Abstract

We study nonlinear connectives (exponentials) in the context of Type Logical Grammar (TLG). We devise four conservative extensions of the displacement calculus with brackets, DbC, DbCM, DbCb and DbCbMr which contain the universal and existential exponential modalities of linear logic (LL). These modalities do not exhibit the same structural properties as in LL, which in TLG are especially adapted for linguistic purposes. The universal modality ! for TLG allows only the commutative and contraction rules, but not weakening, whereas the existential modality ? allows the so-called (intuitionistic) Mingle rule, which derives a restricted version of weakening. We provide a Curry-Howard labelling for both exponential connectives. As it turns out, controlled contraction by ! gives a way to account for the so-called parasitic gaps, and controlled Mingle ? iteration, in particular iterated coordination. Finally, the four calculi are proved to be Cut-Free, and decidability is proved for a linguistically sufficient special case of DbCbMr (and hence DbCb).