×

zbMATH — the first resource for mathematics

Subexponentials in non-commutative linear logic. (English) Zbl 07114855
Summary: Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organised as sets and multisets of formulae not being possible to organise formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.

MSC:
03F52 Proof-theoretic aspects of linear logic and other substructural logics
Software:
CatLog3; Grail
PDF BibTeX XML Cite
Full Text: DOI arXiv
References:
[1] Abrusci, V. M., A comparison between Lambek syntactic calculus and intuitionistic linear logic, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 36, 11-15, (1990) · Zbl 0719.03005
[2] Ajdukiewicz, K., Die syntaktische Konnexität, Studia Philosophica, 1, 1-27, (1935) · JFM 62.1050.03
[3] Andreoli, J.-M., Logic programming with focusing proofs in linear logic, Journal of Logic and Computation, 2, 3, 297-347, (1992) · Zbl 0764.03020
[4] Bar-Hillel, Y., A quasi-arithmetical notation for syntactic description, Language, 29, 47-58, (1953) · Zbl 0156.25402
[5] Benthem, J., Language in Action: Categories, Lambdas and Dynamic Logic, (1991), North Holland: North Holland, Amsterdam · Zbl 0717.03001
[6] Braüner, T. and De Paiva, V. (1998). A formulation of linear logic based on dependency relations. In: Proceedings of the International Workshop on Computer Science Logic (CSL ’97), Lecture Notes in Computer Science, vol. 1414, Springer, 129-148. · Zbl 0910.03034
[7] Buszkowski, W., Some decision problems in the theory of syntactic categories, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28, 539-548, (1982) · Zbl 0499.03010
[8] Buszkowski, W., Lambek calculus and substructural logics, Linguistic Analysis, 36, 1-4, 15-48, (2010)
[9] Chaudhuri, K. (2010). Classical and intuitionistic subexponential logics are equally expressive. In: Proceedings of the International Workshop on Computer Science Logic (CSL ’10), Lecture Notes in Computer Science, vol. 6247, Springer, 185-199.
[10] Danos, V., Joinet, J. and Schellinx, H. (1993). The structure of exponentials: Uncovering the dynamics of linear logic proofs. In: Proceedings of the Kurt Gödel Colloquium on Computational Logic and Proof Theory (KGC ’93), Lecture Notes in Computer Science, vol. 713, Springer, 159-171. · Zbl 0793.03061
[11] Gentzen, G., Untersuchungen über das logische Schließen I, Mathematische Zeitschrift, 39, 176-210, (1935) · JFM 60.0020.02
[12] Girard, J.-Y., Linear logic, Theoretical Computer Science, 50, 1, 1-102, (1987) · Zbl 0625.03037
[13] De Groote, P. (2005). On the expressive power of the Lambek calculus extended with a structural modality. In: Language and Grammar, CSLI Lecture Notes, vol. 168, CSLI, 95-111.
[14] Hodas, J. and Miller, D. (1991). Logic programming in a fragment of intuitionistic linear logic. Extended abstract. In: Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS ’91) 32-42. · Zbl 0807.68016
[15] Hodas, J. and Miller, D. (1994). Logic programming in a fragment of intuitionistic linear logic. Information and Computation110(2) 327-365. · Zbl 0807.68016
[16] Kanazawa, M., The Lambek calculus enriched with additional connectives, Journal of Logic, Language and Information, 1, 2, 141-171, (1992) · Zbl 0793.03028
[17] Kanazawa, M. (1999). Lambek calculus: Recognizing power and complexity. In: Johannes Franciscus Abraham Karel (JFAK). Essays dedicated to Johan van Benthem to the occasion of his 50th birthday. Vossiuspers, Amsterdam Univ. Press.
[18] Kanovich, M. (1994). Horn fragments of non-commutative logics with additives are PSPACE-complete. In: Extended abstract, presented at the 8th Annual Conference of the European Association for Computer Science Logic (CSL ’94), Kazimierz, Poland (unpublished manuscript).
[19] Kanovich, M.I. (1995). The complexity of neutrals in linear logic. In: Proceedings of the 10th Annual Symposium on Logic in Computer Science (LICS ’95), IEEE, 486-495.
[20] Kanovich, M., Kuznetsov, S. and Scedrov, A. (2016a). Reconciling Lambek’s restriction, cut-elimination, and substitution in the presence of exponential modalities. arXiv 1608.02254. · Zbl 06751236
[21] Kanovich, M., Kuznetsov, S. and Scedrov, A. (2016b). Undecidability of the Lambek calculus with a relevant modality. In: Proceedings of the International Conference on Formal Grammar (FG ’15 and ’16), Lecture Notes in Computer Science, vol. 9804, Springer, 240-256. · Zbl 06658641
[22] Kanovich, M., Kuznetsov, S. and Scedrov, A. (2016c). On Lambek’s restriction in the presence of exponential modalities. In: Artemov, S. and Nerode, A. (eds.) Proceedings of the International Symposium on Logical Foundations of Computer Science (LFCS ’16), Lecture Notes in Computer Science, vol. 9537, Springer, 146-158. · Zbl 06751236
[23] Kanovich, M., Kuznetsov, S. and Scedrov, A. (2017). Undecidability of the Lambek calculus with subexponential and bracket modalities. In: Fundamentals of Computation Theory, Lecture Notes in Computer Science, vol. 10472, Springer, 326-340. · Zbl 06810964
[24] Kuznetsov, S. and Okhotin, A. (2017). Conjunctive categorial grammars. In: Proceedings of the 15th Meeting on the Mathematics of Language (MoL ’17), ACL Anthology, vol. W17-3414, 140-151. · Zbl 1376.03034
[25] Kuznetsov, S. L., On the Lambek calculus with a unit and one division, Moscow University Mathematics Bulletin, 66, 4, 173-175, (2011) · Zbl 1304.03053
[26] Kuznetsov, S. L., On translating Lambek grammars with one division into context-free grammars, Proceedings of the Steklov Institute of Mathematics, 294, 129-138, (2016) · Zbl 1359.68153
[27] Lambek, J., The mathematics of sentence structure, The American Mathematical Monthly, 65, 154-170, (1958) · Zbl 0080.00702
[28] Lambek, J. (1961). On the calculus of syntactic types. In: Structure of Language and Its Mathematical Aspects, Proceedings of the Symposia Applied Mathematics, vol. 12, AMS, 166-178.
[29] Lambek, J. (1969). Deductive systems and categories II. Standard constructions and closed categories. In: Category Theory, Homology Theory and Their Applications I, Lecture Notes in Mathematics, vol. 86, Springer, 76-122.
[30] Lambek, J. (1993). From categorial grammar to bilinear logic. In: Substructural Logics, Studies in Logic and Computations, vol. 2, Clarendon Press, Oxford, 207-237. · Zbl 0941.03518
[31] Lincoln, P., Mitchell, J., Scedrov, A. and Shankar, N. (1992). Decision problems for propositional linear logic. Annals of Pure and Applied Logic56(1) 239-311. · Zbl 0768.03003
[32] Markov, A., On the impossibility of certain algorithms in the theory of associative systems, Doklady Academy of Sciences USSR (N. S.), 55, 583-586, (1947) · Zbl 0029.10101
[33] Miller, D. (1994). A multiple-conclusion meta-logic. In: Proceedings of the 9th Annual Symposium on Logic in Computer Science(LICS ’94), IEEE, 272-281.
[34] Miller, D., Forum: A multiple-conclusion specification logic, Theoretical Computer Science, 165, 1, 201-232, (1996) · Zbl 0872.68019
[35] Moortgat, M., Multimodal linguistic inference, Journal of Logic, Language and Information, 5, 349-385, (1996) · Zbl 0919.03023
[36] Moortgat, M. (1997). Categorial type logics. In: Van Benthem, J. and Ter Meulen, A. (eds.), Handbook of Logic and Language, Elsevier.
[37] Moot, R. (2017). The Grail theorem prover: Type theory for syntax and semantics. In: Modern Perspectives in Type-Theoretical Semantics, Studies in Linguistics and Philosophy, vol. 98, Springer, 247-277.
[38] Moot, R. and Retoré, C. (2012). The Logic of Categorial Grammars: A Deductive Account of Natural Language Syntax and Semantics, Lecture Notes in Computer Science, vol. 6850, Springer. · Zbl 1261.03001
[39] Morrill, G. (2017a). Parsing logical grammar: CatLog3. In: Proceedings of the Workshop on Logic and Algorithms in Computational Linguistics (LACompLing ’17), Stockholm University, 107-131.
[40] Morrill, G. (2017b). Grammar logicised: Relativisation. Linguistics and Philosophy40(2) 119-163.
[41] Morrill, G. and Valentín, O. (2015). Computation coverage of TLG: Nonlinearity. In: Proceedings of the Natural Language and Computer Science (NLCS ’15), EPiC Series, vol. 32, 51-63.
[42] Morrill, G. V., Categorial Grammar: Logical Syntax, Semantics, and Processing, (2011), Oxford Univ. Press
[43] Nigam, V. (2012). On the complexity of linear authorization logics. In: Proceedings of the 27th Annual Symposium on Logic in Computer Science (LICS ’12), IEEE, 511-520. · Zbl 1364.03044
[44] Nigam, V., A framework for linear authorization logics, Theoretical Computer Science, 536, 21-41, (2014) · Zbl 1323.03093
[45] Nigam, V. and Miller, D. (2009). Algorithmic specifications in linear logic with subexponentials. In: Proceedings of the Principles and Practice of Declarative Programming (PPDP ’09) 129-140.
[46] Nigam, V., Olarte, C. and Pimentel, E. (2013). A general proof system for modalities in concurrent constraint programming. In: Proceedings of the International Conference on Concurrency Theory (CONCUR ’13), Lecture Notes in Computer Science, vol. 8052, Springer, 410-424. · Zbl 1390.68485
[47] Nigam, V., Pimentel, E. and Reis, G. (2016). An extended framework for specifying and reasoning about proof systems. Journal of Logic and Computation26(2) 539-576. · Zbl 1403.03125
[48] Olarte, C., Pimentel, E. and Nigam, V. (2015). Subexponential concurrent constraint programming. Theoretical Computer Science60698-120. · Zbl 1332.68027
[49] Peirce, C. S., On the algebra of logic: A contribution to the philosophy of notation, American Journal of Mathematics, 7, 180-202, (1885) · JFM 17.0044.02
[50] Pentus, M. (1993). Lambek grammars are context-free. In: Proceedings of the 8th Annual Symposium on Logic in Computer Science (LICS ’93), IEEE, 429-433.
[51] Pentus, M. (1998). Free monoid completeness of the Lambek calculus allowing empty premises. In: Proceedings of the Logic Colloquium ’96, Lecture Notes Logic, vol. 12, Springer, 171-209. · Zbl 0920.03042
[52] Pentus, M., Lambek calculus is NP-complete, Theoretical Computer Science, 357, 1, 186-201, (2006) · Zbl 1104.03013
[53] Pfenning, F. and Simmons, R.J. (2009). Substructural operational semantics as ordered logic programming. In: Proceedings of the 24th Annual Symposium on Logic In Computer Science (LICS ’09), IEEE Computer Society, 101-110.
[54] Post, E. L., Recursive unsolvability of a problem of Thue, Journal of Symbolic Logic, 12, 1-11, (1947) · Zbl 1263.03030
[55] Savitch, W. J., Relationships between nondeterministic and deterministic tape complexities, Journal of Computer and System Sciences, 4, 2, 177-192, (1970) · Zbl 0188.33502
[56] Schellinx, H., Some syntactical observations on linear logic, Journal of Logic and Computation, 1, 4, 537-559, (1991) · Zbl 0745.03025
[57] Shieber, S. M., Evidence against the context-freeness of natural languages, Linguistics and Philosophy, 8, 333-343, (1985)
[58] Thue, A., Probleme über Veränderungen von Zeichenreihen nach gegebener Regeln, Christiana Videnskabs-Selskabets Skrifter, 10, 1-34, (1914) · JFM 45.0333.19
[59] Yetter, D. N., Quantales and (noncommutative) linear logic, Journal of Symbolic Logic, 55, 1, 41-64, (1990) · Zbl 0701.03026
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.