REVIEW
Type-logical grammars and formal languages
Computational Complexity · Submitted 9 Nov 2026 · 3 references
Pith's verdict: Solid extension of Pshenitsyn's construction to a range of type-logical grammars, plus a nontrivial strengthening to NLIN for MILL1; the paper is clear, honest about limitations, and the central claims hold up.
Why Pith says this
Highlight any text to comment on it.
Referee report
The paper
The paper claims
This paper shows that type-logical grammars with product, associativity, extraction, and infixation have NP-complete fixed recognition, and that first-order linear logic grammars generate the quasi-linear languages NLIN.
The reading
What carries the argument
The central mechanism is a two-phase simulation of context-sensitive rewrites using extraction and infixation connectives. Lexical entries are assigned formulas of the form ((F\s)⇓s)•…•p, where each F is (s⇑(δ/γ))⇓s representing a rule instance. The proof uses focusing proof search to separate a prefixation phase (moving F to the front via ⇓L and \R) from an infixation phase (applying the rewrite via /L, ⇑R, ⇓L). For the NLIN simulation in first-order linear logic, the paper encodes a multitape online Turing machine using predicates for word, head, and stack positions, with quantifier rules generating fresh positions for pushed symbols; the composition of atomic state, scan, push, and pop formulas mirrors machine transitions.
Extended reading notes
Core claim
The paper establishes two main results. First, using a translation of linear-time context-sensitive (CS LIN) grammars into type-logical grammars, it proves that any such grammar with product, associativity, medial extraction, and non-deterministic infixation has an NP-complete fixed recognition problem (Corollary 3.2). Second, it shows that first-order linear logic grammars (MILL1) can encode any nondeterministic linear-time (NLIN) Turing machine with three stacks, thus generating all quasi-linear languages. This gives a new lower bound L(NLIN) ⊆ L(MILL1), demonstrating that MILL1 grammars are closed under intersection and produce non-semilinear languages like $a^{{2^n}}$.
Load-bearing premise
The construction relies on the presence of a non-deterministic infixation operation (e.g., the ⇓L rule, the ˇ operator, or the β rule) that can insert a formula arbitrarily into the string; while the paper argues this is available in all considered formalisms, some variants (e.g., original non-associative NL) may lack it, limiting the result’s generality.
Editorial extensions
If this is right
- Fixed recognition for all major type-logical grammars (Displacement calculus, associative logic of scope, hybrid type-logical, multimodal) is NP-complete, making them strictly more powerful than mildly context-sensitive formalisms unless P=NP.
- First-order linear logic grammars generate the quasi-linear languages NLIN, which include the exponential language a^{2^n} and all intersection closures of context-free languages, giving a concrete lower bound on their generative capacity.
- The results provide a unified logic for non-deterministic linear-time string languages, graph languages, and automata, suggesting that MILL1 captures the complexity class NLIN.
- Language classes known to be in NLIN, such as crossing dependencies, copy language ww, and the MIX language, can now be generated by first-order linear logic grammars, extending the known empirical coverage of such systems.
- The paper opens up the possibility that type-logical grammars can be restricted (e.g., by order or growth conditions) to regain polynomial recognition, but the construction shows that unrestricted systems are inherently hard.
Reading between the lines
- If the conjecture that L(MILL1) ⊊ CSL holds, then MILL1 grammars would occupy an intermediate complexity class between NLIN and CSL, providing a precise characterisation of linear-time computable languages that remains open.
- The exponential lexicon blowup (O(k^c) entries per word) in the NLIN simulation suggests that practical parsing of such grammars would be infeasible even for fixed grammars, aligning with the NP-completeness result.
- The paper's mild criticism of polynomial fixed recognition (e.g., O(n^6) vs NP) may reframe the debate on what counts as 'tractable' for natural language: if NLIN-completeness is unavoidable, empirical adequacy might be worth the complexity.
- The separation between type-logical grammars and mild context-sensitivity hinges on semilinearity and homomorphism closure; the paper suggests that intersection alone (without homomorphism) may lead to polynomial parsing, as in RCG, but type-logical grammars naturally have homomorphisms, making the trade-off acute.
Original abstract
We show that type-logical grammars with the standard rules for product, associativity, extraction and infixation have an NP-complete fixed recognition problem, adapting a construction for first-order linear logic from Pshenitsyn (2025), who already showed that grammars in first-order linear logic are closed under intersection and therefore not semilinear and not mildly context-sensitive. We strengthen these results and shown that grammars in first-order linear logic can simulate the quasi-linear grammars of Book \& Greibach (1970), the grammars recognised in non-deterministic linear time (NSPACE(n) or. NLIN). I argue that NLIN is an interesting class of formal languages as well, and a useful upper bound on the time complexity of formalisms used for natural language, just like LOGCFL is a useful upper bound on the space complexity. Taken together this means that first-order linear logic can be seen as the logic of non-deterministic linear-time string languages, graph languages and automata.
Figures
Figures reproduced from arXiv:2611.12618 by the authors.
References
Discussion
Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.