{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T01:37:30Z","timestamp":1769909850750,"version":"3.49.0"},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T00:00:00Z","timestamp":1479686400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,5]]},"abstract":"<jats:p>Subexponential logic is a variant of linear logic with a family of exponential connectives \u2013 called <jats:italic>subexponentials<\/jats:italic> \u2013 that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that a classical propositional multiplicative subexponential logic (<jats:italic><jats:sc>MSEL<\/jats:sc><\/jats:italic>) with one unrestricted and two linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable. We then show how the additive connectives can be directly simulated by giving an encoding of propositional multiplicative additive linear logic (<jats:italic><jats:sc>MALL<\/jats:sc><\/jats:italic>) in an <jats:italic><jats:sc>MSEL<\/jats:sc><\/jats:italic> with one unrestricted and four linear subexponentials.<\/jats:p>","DOI":"10.1017\/s0960129516000293","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T05:39:33Z","timestamp":1479706773000},"page":"651-666","source":"Crossref","is-referenced-by-count":1,"title":["Expressing additives using multiplicatives and subexponentials"],"prefix":"10.1017","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2938-547X","authenticated-orcid":false,"given":"KAUSTUV","family":"CHAUDHURI","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,11,21]]},"reference":[{"key":"S0960129516000293_ref7","first-page":"35","volume-title":"Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP)","author":"L\u00f3pez","year":"2005"},{"key":"S0960129516000293_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90075-B"},{"key":"S0960129516000293_ref16","doi-asserted-by":"crossref","unstructured":"Watkins K. , Cervesato I. , Pfenning F. and Walker D. (2003). A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Carnegie Mellon University. Revised, May 2003.","DOI":"10.21236\/ADA418517"},{"key":"S0960129516000293_ref15","first-page":"21","article-title":"Structural focalization","volume":"15","author":"Simmons","year":"2014","journal-title":"ACM Transaction on Computational Logic"},{"key":"S0960129516000293_ref10","unstructured":"Nigam V. (2009). Exploiting Non-Canonicity in the Sequent Calculus, Ph.D. thesis, Ecole Polytechnique."},{"key":"S0960129516000293_ref8","first-page":"405","volume-title":"CSL 2007: Computer Science Logic","author":"Miller","year":"2007"},{"key":"S0960129516000293_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"S0960129516000293_ref2","first-page":"185","volume-title":"CSL 2010: Computer Science Logic","author":"Chaudhuri","year":"2010"},{"key":"S0960129516000293_ref9","doi-asserted-by":"publisher","DOI":"10.2307\/1970290"},{"key":"S0960129516000293_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9091-0"},{"key":"S0960129516000293_ref3","unstructured":"Chaudhuri K. (2014). Undecidability of multiplicative subexponential logic. In: Alves S. and Cervesato I. (eds.) Proceedings LINEARITY 2014. Electronic Proceedings in Theoretical Computer Science 176 1\u20136."},{"key":"S0960129516000293_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.03.009"},{"key":"S0960129516000293_ref13","volume-title":"Proceedings of the 24th International Conference on Concurrency Theory (CONCUR)","author":"Nigam","year":"2013"},{"key":"S0960129516000293_ref14","doi-asserted-by":"crossref","first-page":"539","DOI":"10.1093\/logcom\/exu029","article-title":"An extended framework for specifying and reasoning about proof systems","volume":"26","author":"Nigam","year":"2014","journal-title":"Journal of Logic and Computation"},{"key":"S0960129516000293_ref1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S0960129516000293_ref11","doi-asserted-by":"crossref","unstructured":"Nigam V. and Miller D. (2009). Algorithmic specifications in linear logic with subexponentials. In: ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP) 129\u2013140.","DOI":"10.1145\/1599410.1599427"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129516000293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,14]],"date-time":"2019-04-14T16:59:04Z","timestamp":1555261144000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129516000293\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,21]]},"references-count":16,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,5]]}},"alternative-id":["S0960129516000293"],"URL":"https:\/\/doi.org\/10.1017\/s0960129516000293","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11,21]]}}}