Bunched logic[1] is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs.[2] The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic,[3] and in systems modelling, where it provides a way to decompose the resources used by components of a system.
The deduction theorem of classical logic relates conjunction and implication:
A\wedgeB\vdashC iff A\vdashB ⇒ C
A*B\vdashC iff A\vdashB{-*}C andalso A\wedgeB\vdashC iff A\vdashB ⇒ C
A*B
B{-*}C
\wedge
⇒
\wedge
⇒
\neg
The easiest way to understand these formulae is in terms of its truth-functional semantics. In this semantics a formula is true or false with respect to given resources.
A*B
A
B
B{-*}C
B
C
\wedge
⇒
The foundation for this reading of formulae was provided bya forcing semantics
r\modelsA
r\modelsA*B iff \existsrArB.rA\modelsA,rB\modelsB,andrA\bulletrB\leqr
rA\bulletrB
\leq
This semantics of bunched logic draws on prior work in relevance logic (especially the operational semantics of Routley–Meyer), but differs from it by not requiring
r\bulletr\leqr
\wedge
⇒
r\bulletr\leqr
r\bulletr
⇒
\wedge
⇒
The double version of the deduction theorem of bunched logic has a corresponding category-theoretic structure. Proofs in intuitionistic logic can be interpreted in cartesian closed categories, that is, categories with finite products satisfying the (natural in A and C) adjunction correspondence relating hom sets:
Hom(A\wedgeB,C) isisomorphicto Hom(A,B ⇒ C)
a categorical model of bunched logic is a single category possessing two closed structures, one symmetric monoidal closed the other cartesian closed.A host of categorial models can be given using Day's tensor product construction.[5] Additionally, the implicational fragment of bunched logic has been given a game semantics.[6]
The algebraic semantics of bunched logic is a special case of its categorical semantics, but is simple to state and can be more approachable.
An algebraic model of bunched logic is a poset that is a Heyting algebra and that carries an additional commutative residuated lattice structure (for the same lattice as the Heyting algebra): that is, an ordered commutative monoid with an associated implication satisfying
A*B\leqC iff A\leqB{-*}C
An algebraic model of boolean bunched logic is a poset that is a Boolean algebra and that carries an additional residuated commutative monoid structure.
The proof calculus of bunched logicdiffers from usual sequent calculi in having a tree-like context of hypotheses instead of a flat list-like structure. In its sequent-based proof theories, the context
\Delta
\Delta\vdashA
\Gamma,A\vdashB | |
\Gamma\vdashA{-* |
B}
\Gamma;A\vdashB | |
\Gamma\vdashA{ ⇒ |
B}
\Delta,\Gamma
\Delta;\Gamma
Corresponding to bunched logic is a type theory having two kinds of function type. Following the Curry–Howard correspondence, introduction rules for implications correspond to introduction rules for function types.
\Gamma,x:A\vdashM:B | |
\Gamma\vdashλx.M:A{-* |
B}
\Gamma;x:A\vdashM:B | |
\Gamma\vdash\alphax.M:A{ ⇒ |
B}
λ
\alpha
The proof theory of bunched logic has an historical debt to the use of bunches in relevance logic.[7] But the bunched structure can in a sense be derived from the categorical and algebraic semantics:to formulate an introduction rule for
{-*}
*
⇒
\wedge
James Brotherston has done further significant work on a unified proof theory for bunched logic and variants,[8] employing Belnap's notion of display logic.[9]
Galmiche, Méry, and Pym have provided a comprehensive treatment of bunched logic, including completeness and other meta-theory, based on labelled tableaux.[10]
In perhaps the first use of substructural type theory to control resources, John C. Reynolds showed how to use an affine type theory to control aliasing and other forms of interference in Algol-like programming languages.[11] O'Hearn used bunched type theory to extend Reynolds' system by allowing interference and non-interference to be more flexibly mixed. This resolved open problems concerning recursion and jumps in Reynolds' system.
Separation logic is an extension of Hoare logic that facilitates reasoning about mutable data structures that use pointers. Following Hoare logic the formulae of separation logic are of the form
\{Pre\}program\{Post\}
Heaps=L\rightharpoonupfV
h0\bulleth1=
Separation logic was used originally to prove properties of sequential programs, but then was extended to concurrency using a proof rule
\{P1\ | |
C |
1\{Q1\} \{P2\}C2\{Q2\}}{\{P1*P2\}C1\parallelC2\{Q1*Q2\}}
Later, the greater generality of the resource semantics was utilized: an abstract version of separation logic works for Hoare tripleswhere the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model.[13] By suitable choice of commutative monoid, it was surprisingly found that the proofs rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding rely-guarantee and trace-based reasoning.[14] [15]
Separation logic is the basis of a number of tools for automatic and semi-automatic reasoning about programs, and is used in the Infer program analyzer currently deployed at Facebook.[16]
Bunched logic has been used in connection with the (synchronous) resource-process calculus SCRP[17] [18] [19] in order to give a (modal) logic that characterizes, in the sense of Hennessy–Milner, the compositional structure of concurrent systems.
SCRP is notable for interpreting
A*B
A*B
R
E
R=S\bulletT
E
F x G
A
S
F
B
T
G
R,E\modelsA
S,F\modelsA
T,G\modelsB
The system SCRP is based directly on bunched logic's resource semantics; that is, on ordered monoids of resource elements. While direct and intuitively appealing, this choice leads to a specific technical problem: the Hennessy–Milner completeness theorem holds only for fragments of the modal logic that exclude the multiplicative implication and multiplicative modalities. This problem is solved by basing resource-process calculus on a resource semantics in which resource elements are combined using two combinators, one corresponding to concurrent composition and one corresponding to choice.[20]
Cardelli, Caires, Gordon and others have investigated a series of logics of process calculi, where a conjunction is interpreted in terms of parallel composition.Unlike the work of Pym et al. in SCRP, they do not distinguish between parallel composition of systems and composition of resources accessed by the systems.
Their logics are based on instances of the resource semantics that give rise to models of the boolean variant of bunched logic. Although these logics give rise to instances of boolean bunched logic, they appear to have been arrived at independently, and in any case have significant additional structure in the way of modalities and binders. Related logics have been proposed as well for modelling XML data.