Possible worlds and resources: The semantics of BI

D J Pym, P W O'Hearn, H Yang

Research output: Contribution to journalArticle

81 Citations (Scopus)

Abstract

The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining operations, one which admits Weakening and Contraction and one which does not). BI may be seen to arise from two main perspectives. On the one hand, from proof-theoretic or categorical concerns and, on the other, from a possible-worlds semantics based on preordered (commutative) monoids. This semantics may be motivated from a basic model of the notion of resource. We explain BI's proof-theoretic, categorical and semantic origins. We discuss in detail the question of completeness, explaining the essential distinction between BI with and without perpendicular to (the unit of boolean OR). We give an extensive discussion of BI as a semantically based logic of resources, giving concrete models based on Petri nets, ambients, computer memory, logic programming, and money. (C) 2003 Published by Elsevier B.V.
Original languageEnglish
Pages (from-to)257-305
Number of pages49
JournalTheoretical Computer Science
Volume315
Issue number1
DOIs
Publication statusPublished - 2004

Fingerprint

Semantics
Categorical
Resources
Logic
Logic programming
Monoids
Logic Programming
Petri nets
Petri Nets
Perpendicular
Contraction
Completeness
Multiplicative
Model-based
Data storage equipment
Unit
Model
Context
Money

Cite this

Possible worlds and resources: The semantics of BI. / Pym, D J; O'Hearn, P W; Yang, H.

In: Theoretical Computer Science, Vol. 315, No. 1, 2004, p. 257-305.

Research output: Contribution to journalArticle

Pym, D J ; O'Hearn, P W ; Yang, H. / Possible worlds and resources: The semantics of BI. In: Theoretical Computer Science. 2004 ; Vol. 315, No. 1. pp. 257-305.
@article{7601eaf924434ae497db2269e9c1171b,
title = "Possible worlds and resources: The semantics of BI",
abstract = "The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining operations, one which admits Weakening and Contraction and one which does not). BI may be seen to arise from two main perspectives. On the one hand, from proof-theoretic or categorical concerns and, on the other, from a possible-worlds semantics based on preordered (commutative) monoids. This semantics may be motivated from a basic model of the notion of resource. We explain BI's proof-theoretic, categorical and semantic origins. We discuss in detail the question of completeness, explaining the essential distinction between BI with and without perpendicular to (the unit of boolean OR). We give an extensive discussion of BI as a semantically based logic of resources, giving concrete models based on Petri nets, ambients, computer memory, logic programming, and money. (C) 2003 Published by Elsevier B.V.",
author = "Pym, {D J} and O'Hearn, {P W} and H Yang",
note = "ID number: ISI:000221372000011",
year = "2004",
doi = "10.1016/j.ics.2003.11.020",
language = "English",
volume = "315",
pages = "257--305",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1",

}

TY - JOUR

T1 - Possible worlds and resources: The semantics of BI

AU - Pym, D J

AU - O'Hearn, P W

AU - Yang, H

N1 - ID number: ISI:000221372000011

PY - 2004

Y1 - 2004

N2 - The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining operations, one which admits Weakening and Contraction and one which does not). BI may be seen to arise from two main perspectives. On the one hand, from proof-theoretic or categorical concerns and, on the other, from a possible-worlds semantics based on preordered (commutative) monoids. This semantics may be motivated from a basic model of the notion of resource. We explain BI's proof-theoretic, categorical and semantic origins. We discuss in detail the question of completeness, explaining the essential distinction between BI with and without perpendicular to (the unit of boolean OR). We give an extensive discussion of BI as a semantically based logic of resources, giving concrete models based on Petri nets, ambients, computer memory, logic programming, and money. (C) 2003 Published by Elsevier B.V.

AB - The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining operations, one which admits Weakening and Contraction and one which does not). BI may be seen to arise from two main perspectives. On the one hand, from proof-theoretic or categorical concerns and, on the other, from a possible-worlds semantics based on preordered (commutative) monoids. This semantics may be motivated from a basic model of the notion of resource. We explain BI's proof-theoretic, categorical and semantic origins. We discuss in detail the question of completeness, explaining the essential distinction between BI with and without perpendicular to (the unit of boolean OR). We give an extensive discussion of BI as a semantically based logic of resources, giving concrete models based on Petri nets, ambients, computer memory, logic programming, and money. (C) 2003 Published by Elsevier B.V.

U2 - 10.1016/j.ics.2003.11.020

DO - 10.1016/j.ics.2003.11.020

M3 - Article

VL - 315

SP - 257

EP - 305

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1

ER -