On the Lambek calculus with an exchange modality

Jiaming Jiang, Harley D Eades, Valeria de Paiva

Research output: Contribution to journalConference article

Abstract

In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton’s Linear/Non-Linear Logic [4] by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed commutative/non-commutative formalization of the Lambek calculus. Then both of these logics are connected via a pair of monoidal adjoint functors. An exchange modality is then derivable within the logic using the adjunction between both sides. Thus, the adjoint functors allow one to pull the exchange structural rule from the left side to the right side. We then give a categorical model in terms of a monoidal adjunction, and then a concrete model in terms of dialectica Lambek spaces.

Original languageEnglish (US)
Pages (from-to)43-89
Number of pages47
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume292
DOIs
StatePublished - Apr 15 2019
Event2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018 - Oxford, United Kingdom
Duration: Jul 7 2018Jul 8 2018

ASJC Scopus subject areas

  • Software

Cite this

On the Lambek calculus with an exchange modality. / Jiang, Jiaming; Eades, Harley D; de Paiva, Valeria.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 292, 15.04.2019, p. 43-89.

Research output: Contribution to journalConference article

@article{f84c73a0764e4e6fa40b314e89d0a0cc,
title = "On the Lambek calculus with an exchange modality",
abstract = "In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton’s Linear/Non-Linear Logic [4] by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed commutative/non-commutative formalization of the Lambek calculus. Then both of these logics are connected via a pair of monoidal adjoint functors. An exchange modality is then derivable within the logic using the adjunction between both sides. Thus, the adjoint functors allow one to pull the exchange structural rule from the left side to the right side. We then give a categorical model in terms of a monoidal adjunction, and then a concrete model in terms of dialectica Lambek spaces.",
author = "Jiaming Jiang and Eades, {Harley D} and {de Paiva}, Valeria",
year = "2019",
month = "4",
day = "15",
doi = "10.4204/EPTCS.292.4",
language = "English (US)",
volume = "292",
pages = "43--89",
journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

TY - JOUR

T1 - On the Lambek calculus with an exchange modality

AU - Jiang, Jiaming

AU - Eades, Harley D

AU - de Paiva, Valeria

PY - 2019/4/15

Y1 - 2019/4/15

N2 - In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton’s Linear/Non-Linear Logic [4] by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed commutative/non-commutative formalization of the Lambek calculus. Then both of these logics are connected via a pair of monoidal adjoint functors. An exchange modality is then derivable within the logic using the adjunction between both sides. Thus, the adjoint functors allow one to pull the exchange structural rule from the left side to the right side. We then give a categorical model in terms of a monoidal adjunction, and then a concrete model in terms of dialectica Lambek spaces.

AB - In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton’s Linear/Non-Linear Logic [4] by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed commutative/non-commutative formalization of the Lambek calculus. Then both of these logics are connected via a pair of monoidal adjoint functors. An exchange modality is then derivable within the logic using the adjunction between both sides. Thus, the adjoint functors allow one to pull the exchange structural rule from the left side to the right side. We then give a categorical model in terms of a monoidal adjunction, and then a concrete model in terms of dialectica Lambek spaces.

UR - http://www.scopus.com/inward/record.url?scp=85065757400&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85065757400&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.292.4

DO - 10.4204/EPTCS.292.4

M3 - Conference article

AN - SCOPUS:85065757400

VL - 292

SP - 43

EP - 89

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

SN - 2075-2180

ER -