?
Soft subexponentials and multiplexing
P. 500–517.
Publication based on the results of:
In book
Vol. 12166. , Cham: Springer, 2020.
Sergey Slavnov, Logical Methods in Computer Science 2023 Vol. 19 No. 4
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 ...
Added: December 20, 2023
Blaisdell E., Kanovich M., Stepan L. Kuznetsov et al., , in: Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, ProceedingsVol. 13385.: Cham: Springer, 2022. P. 449–467.
Added: August 7, 2022
Kanovich M., Kuznetsov S., Scedrov A., Information and Computation 2022 Vol. 287 Article 104760
We investigate language interpretations of two extensions of the Lambek calculus: with additive conjunction and disjunction and with additive conjunction and the unit constant. For extensions with additive connectives, we show that conjunction and disjunction behave differently. Adding both of them leads to incompleteness due to the distributivity law. We show that with conjunction only ...
Added: December 4, 2021
Sergey Slavnov, Mathematical Structures in Computer Science 2021 Vol. 31 No. 5 P. 495–534
Ehrhard et al. (2018. Proceedings of the ACM on Programming Languages, POPL 2, Article 59.) proposed a model of probabilistic functional programming in a category of normed positive cones and stable measurable cone maps, which can be seen as a coordinate-free generalization of probabilistic coherence spaces (PCSs). However, unlike the case of PCSs, it remained unclear ...
Added: November 16, 2021
Slavnov S. A., Journal of Logic and Computation 2022 Vol. 32 No. 3 P. 479–517
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 ...
Added: October 21, 2021
Sergey Slavnov, Journal of Cognitive Science 2021 Vol. 22 No. 2 P. 68–91
We propose a concrete surface representation of abstract categorial grammars in the category of word cobordisms or cowordisms
for short, which are certain bipartite graphs decorated withwords in a given alphabet, generalizing linear logic proof-nets.
We also introduce and study linear logic grammars, directly based on cobordisms and using classical multiplicative linear logic
as a typing system. ...
Added: October 2, 2021
Kanovich M., Kuznetsov S., Scedrov A., Journal of Logic and Computation 2020 Vol. 30 No. 1 P. 239–256
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’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality ...
Added: July 1, 2020
Sergey Slavnov, Logical Methods in Computer Science 2019 Vol. 15 No. 3 P. 1–25
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. ...
Added: October 23, 2019
Sergey Slavnov, Mathematical Structures in Computer Science 2019 Vol. 29 No. 2 P. 215–242
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 rigged sequence 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 ...
Added: December 24, 2017
Sergey Slavnov, / Series arXiv "math". 2016.
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 ...
Added: November 23, 2016
Max I. Kanovich, Mathematical Structures in Computer Science 2016 Vol. 26 No. 5 P. 719–744
In their seminal paper:
Lincoln, P., Mitchell, J., Scedrov, A. and Shankar, N. (1992). Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56 (1–3) 239–311,
LMSS have established an extremely surprising result that propositional linear logic is undecidable. Their proof is very complex and involves numerous nested inductions of different kinds.
Later an alternative ...
Added: September 1, 2016
Kanovich M., Kuznetsov S., Scedrov A., , in: Symposium on Logical Foundations of Computer Science (LFCS 2016)Vol. 9537: Logical Foundations of Computer Science.: Springer, 2016. P. 146–158.
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 of any provable sequent should be non-empty. In this paper we discuss ways of extending the Lambek calculus with the linear logic exponential ...
Added: June 28, 2016
Sergey Slavnov, Annals of Pure and Applied Logic 2014 Vol. 165 No. 1 P. 357–370
Just as intuitionistic proofs can be modeled by functions, linear logic proofs, being symmetric in the inputs and outputs, can be modeled by relations (for example, cliques in coherence spaces). However generic relations do not establish any functional dependence between the arguments, and therefore it is questionable whether they can be thought as reasonable generalizations ...
Added: October 7, 2013