Undecidability of the Lambek calculus with a relevant modality
Morrill and Valentin in the paper "Computational coverage of TLG: Nonlinearity" considered an extension of the Lambek calculus enriched by a so-called "exponential" modality. This modality behaves in the "relevant" style, that is, it allows contraction and permutation, but not weakening. Morrill and Valentin stated an open problem whether this system is decidable. Here we show its undecidability. Our result remains valid if we consider the fragment where all division operations have one direction. We also show that the derivability problem in a restricted case, where the modality can be applied only to variables (primitive types), is decidable and belongs to the NP class.
Code (0)
등록된 구현이 없습니다.
Tasks
validSimilar Papers 제목 키워드 기반
Undecidability of the Lambek calculus with subexponential and bracket modalities
The Lambek calculus is a well-known logical formalism for modelling natural language syntax. The original calculus covered a substantial number of intricate natural language phenomena, but only those restricted to the co…
Vector Space Semantics for Lambek Calculus with Soft Subexponentials
We develop a vector space semantics for Lambek Calculus with Soft Subexponentials, apply the calculus to construct compositional vector interpretations for parasitic gap noun phrases and discourse units with anaphora and…
SentenceSentence SimilarityReconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called "Lambek's restriction," that is, the antecedent o…
Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality
We develop a categorical compositional distributional semantics for Lambek Calculus with a Relevant Modality !L*, which has a limited edition of the contraction and permutation rules. The categorical part of the semantic…
SentenceA polynomial time algorithm for the Lambek calculus with brackets of bounded order
Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. Pentus (2010) gave a polynomial-time algorithm for determ- ining provability of bounded d…