The Logic of Bunched Implications
We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication and can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers for all new and there exists new which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels.
Basic References
Erratum: In Proposition 4, `DCC' should be `bicartesian DCC'.
@book{PymMono,
title={The Semantics and Proof Theory of
the Logic of Bunched Implications},
author={D.J. Pym},
year={2002},
publisher={Kluwer Academic Publishers},
series={Applied Logic Series},
volume={26},
note={Errata and Remarks maintained at:
\url{http://www.cantab.net/users/david.pym/BI-monograph-errata.pdf}},
}
A list of Errata and Remarks (pdf), last updated 30 March, 2008, is available as pdf. Full citations of articles which extend the content of the monograph are provided.
@unpublishd{BI-Errata,
author="D.J. Pym",
title="{E}rrata and {R}emarks for \emph{The Semantics and Proof Theory of
the Logic of Bunched Implications} \cite{PymMono}",
note="Maintained at:
\url{http://www.springer.com/philosophy/logic/book/978-1-4020-0745-3}",
year="2008"
}
This monograph provides a thorough account of the model theory, proof theory and computational interpretations of BI, the logic of bunched implications, which freely combines intuitionistic logic and multiplicative intuitionistic linear logic. Starting, on the one hand, from elementary observations about modelling resources and, on the other, from a desire to develop a system of logic within which additive (or extensional) and multiplicative (or intensional) implications co-exist with equal logical status, we give natural deduction, lambda-calculi, sequent calculus, categorical semantics, Kripke models, topological models, logical relations and computational interpretations for both propositional and predicate BI, within which both additive and multiplicative quantifiers also co-exist. This monograph will be of interest to graduate students and researchers in mathematical logic, philosophical logic, computational logic and theoretical computer science.
Contents List of Figures. List of Tables. Preface. Acknowledgments. Foreword. Introduction; David J. Pym. Part I: Propositional BI. 1. Introduction to Part I. 2. Natural Deduction for Propositional BI. 3. Algebraic, Topological, Categorical. 4. Kripke Semantics. 5. Topological Kripke Semantics. 6. Propositional BI as a Sequent Calculus. 7. Towards Classical Propositional BI. 8. Bunched Logical Relations. 9. The Sharing Interpretation, I. Part II: Predicate BI. 10. Introduction to Part II. 11. The Syntax of Predicate BI. 12. Natural Deduction & Sequent Calculus For Predicate BI. 13. Kripke Semantics for Predicate BI. 14. Topological Kripke Semantics for Predicate BI. 15. Resource Semantics, Type Theory & Fibred Categories. 16. The Sharing Interpretation, II. Bibliography. Index.
The logic of bunched implications, BI , provides a logical analysis of a basic notion of resource which has proved rich enough to provide a pointer logic semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, thereby providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI's tableaux to solve the resource-distribution problem, the labels being the elements of resource models. In the case of BI with inconsistency, the challenge consists in dealing with BI's Grothendieck topological models within such a based-on labels proof-search method. In this paper, we prove soundness and completeness theorems for a resource tableaux method TBI with respect this semantics and provides a way to build countermodels from so-called dependency graphs. As consequences, we have two new results for BI: the decidability for propositional BI and the finite model property with respect to Grothendieck topological semantics. In addition, we propose a new resource semantics by considering a partially defined monoid, which generalizes the semantics of BI pointer logic and is complete for BI.
Errata and remarks applicable to this paper are available here.
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 bottom (the unit of 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.
Errata and remarks applicable to this paper are available here.
An implmentation of the bunched logic programming language, BLP, which requires OCAML, and Pablo Armelín's Ph.D. thesis are available from the BLP directory.
We consider the problem of searching for proofs in sequential presentations of logics with multiplicative (or intensional) connectives. Specifically, we start with the multiplicative fragment of linear logic and extend, on the one hand, to linear logic with its additives and, on the other, to the additives of the logic of bunched implications (BI). We give an algebraic method for calculating the distribution of the side-formulæ in multiplicative rules which allows the occurrence or non-occurrence of a formula on a branch of a proof to be determined once sufficient information is available. Each formula in the conclusion of such a rule is assigned a Boolean expression. As a search proceeds, a set of Boolean constraint equations is generated. We show that a solution to such a set of equations determines a proof corresponding to the given search. We explain a range of strategies, from the lazy to the eager, for solving sets of constraint equations. We indicate how to apply our methods systematically to large family of relevant systems.
A preprint is available.
Abstract. The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough, for example, to form the logical basis for ``pointer logic'' and ``separation logic'' semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI's tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, bottom, the challenge consists in dealing with BI's Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. Then, from these results, we can define a new resource semantics of BI, based on partially defined monoids, and prove that this semantics is complete. Such a semantics, based on partiality, is closely related to the semantics of BI's (intuitionistic) pointer and separation logics. Returning to the tableaux calculus, we propose a new version with liberalized rules for which the countermodels are closely related to the topological Kripke semantics of BI. As consequences of the relationships between semantics of BI and resource tableaux, we prove two strong new results for propositional BI: its decidability and the finite model property with respect to topological semantics.
The BILL Theorem Prover
A theorem prover, BILL (Bunched Implication Logic with Labels), for propositional BI, based on BI's labelled semantic tableaux, has been implemented by Frédéric Béal, Daniel Méry and Didier Galmiche at LORIA, Nancy.
BILL References