Bunched logic

From Wikipedia, the free encyclopedia

Bunched logic is a variety of substructural logic that, like linear logic, has classes of multiplicative and additive operators, but differs from usual proof calculi in having a tree-like context of hypotheses instead of a flat list-like structure; it is thus a calculus of deep inference. Sub-trees of the context tree are referred to as bunches; hence the name. The internal nodes in the context tree are labelled with the mode of composition — multiplicative or additive, with the following characteristics:

Multiplicative composition denies the structural rules of weakening and contraction.
Additive composition admits weakening and contraction of entire bunches.

Correpsonding to each of these bunch combinators is conjunction, and each conjunction has an associated implication; hence the name, the logic of bunched implications.

The semantics of bunched logic can be given in terms of Kripke models in which the set of worlds carries not only a preorder but also a monoidal product. Categorical models of bunched logic are given by doubly-closed categories, which are both cartesian closed and symmetric monoidal closed. Day's tensor product construction can be used to generate categorical models corresponding to the Kripke semantics.

Bunched logic has been used in connection with the (synchronous) resource-process calculus SCRP in order to give a logic which characterizes, in the sense of Hennessey-Milner, the compositional structure of concurrent systems.

Bunched logic extended with a semantic model of locations and store is known as separation logic. It has been used to define the logic of pointer-analysis in languages like ALGOL or C.

The implicational fragment of bunched logic has been given a games semantics.

[edit] See also

Linear logic

[edit] References

(*)Matthew Collinson, David Pym, and Chris Tofts. Errata for Formal Aspects of Computing (2006) 18:495-517 and their consequences.
Peter O'Hearn and David Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic 5(2)(1999) 215-244.
O'Hearn P, On bunched typing, Journal of Functional Programming, 13(4), 747—796, 2003. (PDF)
Guy McCusker and David Pym. A Games Model of Bunched Implications. Proc. CSL 2007, LNCS.
Peter O'Hearn. Resources, Concurrency, and Local Reasoning. Theoretical Computer Science 357(1-3) 271-307, 2007.
David Pym, Peter O'Hearn, and Hongseok Yang. Possible Worlds and Resources: The Semantics of BI. Theoretical Computer Science 315 (2004) 257-305.
David Pym and Chris Tofts. A calculus and logic of resources and processes. Formal Aspects of Computing (2006) 18:495-517. Errata in (*).
David Pym and Chris Tofts. Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic. In: Cardelli, L. Fiore M, Winskel, G (eds) Electronic Notes in Theoretical Computer Science (Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin) 107, 545-587. Errata in (*).
David Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, 2002. Errata and Remarks at: www.cs.bath.ac.uk/~pym/BI-monograph-errata.pdf.