-
Tensor term logic for categorial grammars: simple unification of commutative and noncommutative structure
Authors:
Sergey Slavnov
Abstract:
A prototypical example of categorial grammars are those based on Lambek calculus, i.e. noncommutative intuitionistic linear logic. However, it has been noted that purely noncommutative operations are often not sufficient for modeling even very simple natural language phenomena. Therefore a number of alternative formalisms are considered in the literature: those using purely ``commutative'' linear…
▽ More
A prototypical example of categorial grammars are those based on Lambek calculus, i.e. noncommutative intuitionistic linear logic. However, it has been noted that purely noncommutative operations are often not sufficient for modeling even very simple natural language phenomena. Therefore a number of alternative formalisms are considered in the literature: those using purely ``commutative'' linear logic as well as combining (to some level) commutative and non-commutative operations. The logic of tensor terms that we propose is a variant of such a combination. This logical calculus was designed specially for defining categorial grammars. It contains Lambek calculus and multiplicative linear logic as conservative fragments, yet the syntax is very simple, not departing much from that of multiplicative linear logic. The system is cut-free and decidable, it has both intuitionistic and classical versions, besides it is equipped with a simple intuitive semantics, which is sound and complete.
△ Less
Submitted 18 December, 2023;
originally announced December 2023.
-
Making first order linear logic a generating grammar
Authors:
Sergey Slavnov
Abstract:
It is known that different categorial grammars have surface representation in a fragment of first order multiplicative linear logic (MLL1). We show that the fragment of interest is equivalent to the recently introduced extended tensor type calculus (ETTC). ETTC is a calculus of specific typed terms, which represent tuples of strings, more precisely bipartite graphs decorated with strings. Types ar…
▽ More
It is known that different categorial grammars have surface representation in a fragment of first order multiplicative linear logic (MLL1). We show that the fragment of interest is equivalent to the recently introduced extended tensor type calculus (ETTC). ETTC is a calculus of specific typed terms, which represent tuples of strings, more precisely bipartite graphs decorated with strings. Types are derived from linear logic formulas, and rules correspond to concrete operations on these string-labeled graphs, so that they can be conveniently visualized. This provides the above mentioned fragment of MLL1 that is relevant for language modeling not only with some alternative syntax and intuitive geometric representation, but also with an intrinsic deductive system, which has been absent.
In this work we consider a non-trivial notationally enriched variation of the previously introduced ETTC, which allows more concise and transparent computations. We present both a cut-free sequent calculus and a natural deduction formalism.
△ Less
Submitted 16 November, 2023; v1 submitted 17 June, 2022;
originally announced June 2022.
-
On embedding Lambek calculus into commutative categorial grammars
Authors:
Sergey Slavnov
Abstract:
We consider tensor grammars, which are an example of \commutative" grammars, based on the classical (rather than intuitionistic) linear logic. They can be seen as a surface representation of abstract categorial grammars ACG in the sense that derivations of ACG translate to derivations of tensor grammars and this translation is isomorphic on the level of string languages. The basic ingredient are t…
▽ More
We consider tensor grammars, which are an example of \commutative" grammars, based on the classical (rather than intuitionistic) linear logic. They can be seen as a surface representation of abstract categorial grammars ACG in the sense that derivations of ACG translate to derivations of tensor grammars and this translation is isomorphic on the level of string languages. The basic ingredient are tensor terms, which can be seen as encoding and generalizing proof-nets. Using tensor terms makes the syntax extremely simple and a direct geometric meaning becomes transparent. Then we address the problem of encoding noncommutative operations in our setting. This turns out possible after enriching the system with new unary operators. The resulting system allows representing both ACG and Lambek grammars as conservative fragments, while the formalism remains, as it seems to us, rather simple and intuitive.
△ Less
Submitted 19 November, 2021; v1 submitted 20 May, 2020;
originally announced May 2020.
-
Classical linear logic, cobordisms and categorial grammars
Authors:
Sergey Slavnov
Abstract:
We propose a categorial grammar based on classical multiplicative linear logic.
This can be seen as an extension of abstract categorial grammars (ACG) and is at least as expressive. However, constituents of {\it linear logic grammars (LLG)} are not abstract $λ$-terms, but simply tuples of words with labeled endpoints and supplied with specific {\it plugging instructions}: the sets of endpoints a…
▽ More
We propose a categorial grammar based on classical multiplicative linear logic.
This can be seen as an extension of abstract categorial grammars (ACG) and is at least as expressive. However, constituents of {\it linear logic grammars (LLG)} are not abstract $λ$-terms, but simply tuples of words with labeled endpoints and supplied with specific {\it plugging instructions}: the sets of endpoints are subdivided into the {\it incoming} and the {\it outgoing} parts. We call such objects {\it word cobordisms}.
A key observation is that word cobordisms can be organized in a category, very similar to the familiar category of topological cobordisms. This category is symmetric monoidal closed and compact closed and thus is a model of linear $λ$-calculus and classical, as well as intuitionistic linear logic. This allows us using linear logic as a typing system for word cobordisms.
At least, this gives a concrete and intuitive representation of ACG.
We think, however, that the category of word cobordisms, which has a rich structure and is independent of any grammar, might be interesting on its own right.
△ Less
Submitted 31 July, 2020; v1 submitted 10 November, 2019;
originally announced November 2019.
-
Abstract categorial grammars with island constraints and effective decidability
Authors:
Sergey Slavnov
Abstract:
A well-known approach to treating syntactic island constraints in the setting of Lambek grammars consists in adding specific bracket modalities to the logic. We adapt this approach to abstract categorial grammars (ACG). Thus we define bracketed (implicational) linear logic, bracketed lambda-calculus, and, eventually, bracketed ACG based on bracketed $λ$-calculus. This allows us modeling at least s…
▽ More
A well-known approach to treating syntactic island constraints in the setting of Lambek grammars consists in adding specific bracket modalities to the logic. We adapt this approach to abstract categorial grammars (ACG). Thus we define bracketed (implicational) linear logic, bracketed lambda-calculus, and, eventually, bracketed ACG based on bracketed $λ$-calculus. This allows us modeling at least simplest island constraints, typically, in the context of relativization. Next we identify specific safely bracketed ACG which, just like ordinary (bracket-free) second order ACG generate effectively decidable languages, but are sufficiently flexible to model some higher order phenomena like relativization and correctly deal with syntactic islands, at least in simple toy examples.
△ Less
Submitted 20 May, 2020; v1 submitted 16 July, 2019;
originally announced July 2019.
-
Classical linear logic, cobordisms and categorical semantics of categorial grammars
Authors:
Sergey Slavnov
Abstract:
We propose a categorial grammar based on classical multiplicative linear logic.
This can be seen as an extension of abstract categorial grammars (ACG) and is at least as expressive. However, constituents of {\it linear logic grammars (LLG)} are not abstract $λ$-terms, but simply tuples of words with labeled endpoints, we call them {\it multiwords}. At least, this gives a concrete and intuitive r…
▽ More
We propose a categorial grammar based on classical multiplicative linear logic.
This can be seen as an extension of abstract categorial grammars (ACG) and is at least as expressive. However, constituents of {\it linear logic grammars (LLG)} are not abstract $λ$-terms, but simply tuples of words with labeled endpoints, we call them {\it multiwords}. At least, this gives a concrete and intuitive representation of ACG.
A key observation is that the class of multiwords has a fundamental algebraic structure. Namely, multiwords can be organized in a category, very similar to the category of topological cobordisms. This category is symmetric monoidal closed and compact closed and thus is a model of linear $λ$-calculus and classical linear logic. We think that this category is interesting on its own right. In particular, it might provide categorical representation for other formalisms.
On the other hand, many models of language semantics are based on commutative logic or, more generally, on symmetric monoidal closed categories. But the category of {\it word cobordisms} is a category of language elements, which is itself symmetric monoidal closed and independent of any grammar. Thus, it might prove useful in understanding language semantics as well.
△ Less
Submitted 9 February, 2019; v1 submitted 4 October, 2018;
originally announced October 2018.
-
On noncommutative extensions of linear logic
Authors:
Sergey Slavnov
Abstract:
Pomset logic introduced by Retoré is an extension of linear logic with a self-dual noncommutative connective. The logic is defined by means of proof-nets, rather than a sequent calculus. Later a deep inference system BV was developed with an eye to capturing Pomset logic, but equivalence of system has not been proven up to now. As for a sequent calculus formulation, it has not been known for eithe…
▽ More
Pomset logic introduced by Retoré is an extension of linear logic with a self-dual noncommutative connective. The logic is defined by means of proof-nets, rather than a sequent calculus. Later a deep inference system BV was developed with an eye to capturing Pomset logic, but equivalence of system has not been proven up to now. As for a sequent calculus formulation, it has not been known for either of these logics, and there are convincing arguments that such a sequent calculus in the usual sense simply does not exist for them. In an on-going work on semantics we discovered a system similar to Pomset logic, where a noncommutative connective is no longer self-dual. Pomset logic appears as a degeneration, when the class of models is restricted. Motivated by these semantic considerations, we define in the current work a semicommutative multiplicative linear logic}, which is multiplicative linear logic extended with two nonisomorphic noncommutative connectives (not to be confused with very different Abrusci-Ruet noncommutative logic). We develop a syntax of proof-nets and show how this logic degenerates to Pomset logic. However, a more interesting problem than just finding yet another noncommutative logic is to find a sequent calculus for this logic. We introduce decorated sequents, which are sequents equipped with an extra structure of a binary relation of reachability on formulas. We define a decorated sequent calculus for semicommutative logic and prove that it is cut-free, sound and complete. This is adapted to "degenerate" variations, including Pomset logic. Thus, in particular, we give a variant of sequent calculus formulation for Pomset logic, which is one of the key results of the paper.
△ Less
Submitted 19 September, 2019; v1 submitted 29 March, 2017;
originally announced March 2017.
-
On partial traces and compactification of $*$-autonomous Mix-categories
Authors:
Sergey Slavnov
Abstract:
We study the question when a $*$-autonomous Mix-category has a representation as a $*$-autonomous Mix-subcategory of a compact one. We define certain partial trace-like operation on morphisms of a Mix-category, which we call a mixed trace, and show that any structure preserving embedding of a Mix-category into a compact one induces a mixed trace on the former. We also show that, conversely, if a M…
▽ More
We study the question when a $*$-autonomous Mix-category has a representation as a $*$-autonomous Mix-subcategory of a compact one. We define certain partial trace-like operation on morphisms of a Mix-category, which we call a mixed trace, and show that any structure preserving embedding of a Mix-category into a compact one induces a mixed trace on the former. We also show that, conversely, if a Mix-category ${\bf K}$ has a mixed trace, then we can construct a compact category and structure preserving embedding of ${\bf K}$ into it, which induces the same mixed trace.
Finally, we find a specific condition expressed in terms of interaction of Mix- and coevaluation maps on a Mix-category ${\bf K}$, which is necessary and sufficient for a structure preserving embedding of ${\bf K}$ into a compact one to exist. When this condition is satisfied, we construct a "free" or "minimal" mixed trace on ${\bf K}$ directly from the Mix-category structure, which gives us also a "free" compactification of ${\bf K}$.
△ Less
Submitted 4 August, 2016;
originally announced August 2016.
-
Compactification of *-autonomous categories
Authors:
Sergey Slavnov
Abstract:
We study the question when a *-autonomous (Mix-)category has a representation as a $*$-autonomous category of a compact one. We prove that necessary and sufficient condition is that weak distributivity maps are monic (or, equivalently epic). For a Mix-category, this condition is, in turn, equivalent to the requirement that Mix-maps be monic (or epic). We call categories satisfying this property to…
▽ More
We study the question when a *-autonomous (Mix-)category has a representation as a $*$-autonomous category of a compact one. We prove that necessary and sufficient condition is that weak distributivity maps are monic (or, equivalently epic). For a Mix-category, this condition is, in turn, equivalent to the requirement that Mix-maps be monic (or epic). We call categories satisfying this property torsion-free. An important side result is that torsion-free categories have canonical partial traces.
△ Less
Submitted 20 July, 2016; v1 submitted 13 July, 2016;
originally announced July 2016.
-
On Banach spaces of sequences and free linear logic exponential modality
Authors:
Sergey Slavnov
Abstract:
We introduce a category of vector spaces modelling full propositional linear logic, similar to probabilistic coherence spaces and to Koethe sequences spaces. Its objects are {\it rigged sequences spaces}, Banach spaces of sequences, with norms defined from pairing with finite sequences, and morphisms are bounded linear maps, continuous in a suitable topology. The main interest of the work is that…
▽ More
We introduce a category of vector spaces modelling full propositional linear logic, similar to probabilistic coherence spaces and to Koethe sequences spaces. Its objects are {\it rigged sequences spaces}, Banach spaces of sequences, with norms defined from pairing with finite sequences, and morphisms are bounded linear maps, continuous in a suitable topology. The main interest of the work is that our model gives a realization of the free linear logic exponentials construction.
△ Less
Submitted 23 November, 2016; v1 submitted 13 September, 2015;
originally announced September 2015.
-
Linear logic with idempotent exponential modalities: a note
Authors:
Sergey Slavnov
Abstract:
In this note we discuss a variant of linear logic with idempotent exponential modalities. We propose a sequent calculus system and discuss its semantics. We also give a concrete relational model for this calculus.
In this note we discuss a variant of linear logic with idempotent exponential modalities. We propose a sequent calculus system and discuss its semantics. We also give a concrete relational model for this calculus.
△ Less
Submitted 22 July, 2014;
originally announced July 2014.
