Bunched logic
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:
Corresponding 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.
Substructural logic
In logic, a substructural logic is a logic lacking one of the usual structural rules , such as weakening, contraction or associativity...
that, like linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
, has classes of multiplicative and additive operators, but differs from usual proof calculi in having a tree-like context of hypotheses
Hypothesis
A hypothesis is a proposed explanation for a phenomenon. The term derives from the Greek, ὑποτιθέναι – hypotithenai meaning "to put under" or "to suppose". For a hypothesis to be put forward as a scientific hypothesis, the scientific method requires that one can test it...
instead of a flat list-like structure; it is thus a calculus of deep inference
Deep inference
Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity...
. 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 ruleStructural ruleIn proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgements or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic...
s of weakening and contraction. - Additive composition admits weakening and contraction of entire bunches.
Corresponding 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
Preorder
In mathematics, especially in order theory, preorders are binary relations that are reflexive and transitive.For example, all partial orders and equivalence relations are preorders...
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
Tensor product
In mathematics, the tensor product, denoted by ⊗, may be applied in different contexts to vectors, matrices, tensors, vector spaces, algebras, topological vector spaces, and modules, among many other structures or objects. In each case the significance of the symbol is the same: the most general...
construction can be used to generate categorical models corresponding to the Kripke semantics
Kripke semantics
Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
.
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
Robin Milner
Arthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...
, the compositional structure of concurrent systems.
Bunched logic extended with a semantic model of locations and store is known as separation logic
Separation logic
In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs.It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Burstall...
. It has been used to define the logic of pointer-analysis in languages like ALGOL
ALGOL
ALGOL is a family of imperative computer programming languages originally developed in the mid 1950s which greatly influenced many other languages and became the de facto way algorithms were described in textbooks and academic works for almost the next 30 years...
or C
C (programming language)
C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
.
The implicational fragment of bunched logic has been given a games semantics.