Skip to Main content Skip to Navigation
Journal articles

Expressing Additives Using Multiplicatives and Subexponentials

Kaustuv Chaudhuri 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Subexponential logic is a variant of linear logic with a family of exponential connectives—called subex-ponentials—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 (MSEL) 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 con-nectives can be directly simulated by giving an encoding of propositional multiplicative additive linear logic (MALL) in an MSEL with one unrestricted and four linear subexponentials.
Document type :
Journal articles
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01222767
Contributor : Kaustuv Chaudhuri <>
Submitted on : Friday, October 30, 2015 - 3:01:14 PM
Last modification on : Friday, April 30, 2021 - 9:55:17 AM
Long-term archiving on: : Sunday, January 31, 2016 - 11:41:02 AM

Files

main.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License

Identifiers

  • HAL Id : hal-01222767, version 1

Collections

Citation

Kaustuv Chaudhuri. Expressing Additives Using Multiplicatives and Subexponentials. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (5), pp.651-666. ⟨hal-01222767⟩

Share

Metrics

Record views

448

Files downloads

325