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.
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.
See also
References