First-Order Intuitionistic Linear Logic and Hypergraph Languages

There is a strong connection between substructural logics, especially non-commutative ones, and the theory of formal languages and grammars [Buszkowski03, MootR12]. This connection is two-way. On the one hand, a logic can be used as a derivational mechanism for generating formal languages, which is the essence of categorial grammars. One prominent example is Lambek categorial grammars based on the Lambek calculus $\mathrm{L}$ [Lambek58]; formulae of the latter are built using multiplicative conjunction ‘$\cdot$’ and two directed implications ‘$\backslash$’, ‘$/$’. In a Lambek categorial grammar, one assigns a finite number of formulae of $\mathrm{L}$ to each symbol of an alphabet and chooses a distinguished formula $S$; then, the grammar accepts a string $a_{1}\ldots a_{n}$ if the sequent $A_{1},\ldots,A_{n}\vdash S$ is derivable in $\mathrm{L}$ where, for $i=1,\ldots,n$, $A_{i}$ is one of the formulae assigned to $a_{i}$. A famous result by Pentus [Pentus93] says that Lambek categorial grammars generate exactly context-free languages (without the empty word, to be precise).

On the other hand, algebras of formal languages can serve as models for substructural logics. For example, one can define language semantics for the Lambek calculus as follows: a language model is a function $u$ mapping formulas of $\mathrm{L}$ to formal languages such that $u(A\cdot B)=\{vw\mid v\in u(A),w\in u(B)\}$, $u(B\backslash A)=\{w\mid\forall v\in u(B)\;vw\in u(A)\}$, and $u(A/B)=\{v\mid\forall w\in u(B)\;vw\in u(A)\}$; a sequent $A\vdash B$ is interpreted as inclusion $u(A)\subseteq u(B)$. Another famous result by Pentus with a very complicated proof [Pentus95] is that $\mathrm{L}$ is sound and complete w.r.t. language semantics; completeness for the fragment of $\mathrm{L}$ without ‘$\cdot$’ had been proved earlier by Buszkowski in [Buszkowski82].

Numerous variants and extensions of the Lambek calculus have been studied, including its nonassociative version [MootR12], commutative version [vanBenthem95] (i.e. multiplicative intuitionistic linear logic), the multimodal Lambek calculus [Moortgat96], the displacement calculus [MorrillVF10] etc. These logics have many common properties, which motivates searching for a unifying logic. One such “umbrella” logic is the first-order multiplicative intuitionistic linear logic $\mathrm{MILL}1$ [Moot14, MootP01], which is the multiplicative fragment of first-order intuitionistic linear logic $\mathrm{ILL}1$. The Lambek calculus can be embedded in $\mathrm{MILL}1$ [MootP01]: for example, the $\mathrm{L}$ sequent $p\cdot p\backslash q\vdash q$ is translated into the $\mathrm{MILL}1$ sequent $p(x_{0},x_{1})\otimes\forall y(p(y,x_{1})\multimap q(y,x_{2}))\vdash q(x_{0},x_{2})$. Although $\mathrm{MILL}1$ is a first-order generalisation of $\mathrm{L}$, derivability problems in these logics have the same complexity, namely, they are NP-complete.

One can define $\mathrm{MILL}1$ categorial grammars in the same manner as Lambek categorial grammars [Moot14, Slavnov23]. The former generalise of the latter, hence generate all context-free languages. Moot proved in [Moot14] that $\mathrm{MILL}1$ grammars generate all multiple context-free languages, hence some non-context-free ones, e.g. $\{ww\mid w\in\Sigma^{\ast}\}$. However, it has remained an open question whether the upper bound is the same:

“Do $\mathrm{MILL}1$ grammars without complex terms <…> generate exactly the multiple context-free languages or strictly more?” [Moot14]

It turns out that the interplay between propositional substructural logics and formal grammars can be elevated fruitfully to that between first-order substructural logics and hypergraph grammars, which is the subject of this article. Hypergraph grammar approaches generate sets of hypergraphs; usually they are designed as generalisations of grammar formalisms generating strings. For example, hyperedge replacement grammar [DrewesKH97] is a formalism that extends context-free grammar. A rule of a hyperedge replacement grammar allows one to replace a hyperedge in a hypergraph by another hypergraph; see an example below.