Bunched logic is a variety of substructural logic proposed by

Peter O'Hearn Peter William O'Hearn One or more of the preceding sentences incorporates text from the royalsociety.org website where: (born 13 July 1963 in Halifax, Nova Scotia), formerly a research scientist at Meta, is a Distinguished Engineer at Lacewor ...

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)

set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...

s as in most

proof calculi In mathematical logic, a proof calculus or a proof system is built to prove statements. Overview A proof system includes the components: * Language: The set ''L'' of formulas admitted by the system, for example, propositional logic or first-order ...

. Bunched logic has an associated

type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundat ...

, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in

program verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...

, where it is the basis of the assertion language of

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 Rod Burstall. The assertion l ...

, and in

systems modelling Systems modeling or system modeling is the interdisciplinary study of the use of models to conceptualize and construct systems in business and IT development.

Foundations

The deduction theorem of

classical logic Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy. Characteristics Each logical system in this class ...

relates conjunction and implication: ::

A \wedge B \vdash C \quad \mbox \quad A \vdash B \Rightarrow C

Bunched logic has two versions of the deduction theorem: ::

A * B \vdash C \quad \mbox \quad A \vdash B  C  \qquad  \mbox  \qquad A \wedge B \vdash C \quad \mbox \quad A \vdash B \Rightarrow C

A * B

and

B  C

are forms of conjunction and implication that take resources into account (explained below). In addition to these connectives bunched logic has a formula, sometimes written I or emp, which is the unit of *. In the original version of bunched logic

\wedge

and

\Rightarrow

were the connectives from intuitionistic logic, while a boolean variant takes

\wedge

and

\Rightarrow

(and

\neg

) as from traditional

boolean logic In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variable (mathematics), variables are the truth values ''true'' and ''false'', usually denote ...

. Thus, bunched logic is compatible with constructive principles, but is in no way dependent on them.

Truth-functional Semantics (resource semantics)

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

asserts that the resource at hand can be decomposed into resources that satisfy

A

and

B

B  C

says that if we compose the resource at hand with additional resource that satisfies

B

, then the combined resource satisfies

C

\wedge

and

\Rightarrow

have their familiar meanings. The foundation for this reading of formulae was provided by a forcing semantics

r \models A

advanced by Pym, where the forcing relation means ''A'' holds of resource ''r''. The semantics is analogous to Kripke's semantics of

intuitionistic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fu ...

modal logic Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...

, but where the elements of the model are regarded as resources that can be composed and decomposed, rather than as possible worlds that are accessible from one another. For example, the forcing semantics for the conjunction is of the form ::

r \models A * B \quad \mbox \quad \exists r_Ar_B.\,r_A \models A,\, r_B \models B,\,\mbox\,r_A \bullet r_B \leq r

where

r_A \bullet r_B

is a way of combining resources and

\leq

is a relation of approximation. 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 \bullet r  \leq r

and by accepting the semantics of standard intuitionistic or classical versions of

\wedge

and

\Rightarrow

. The property

r \bullet r  \leq r

is justified when thinking about relevance but denied by considerations of resource; having two copies of a resource is not the same as having one, and in some models (e.g.

heap Heap or HEAP may refer to: Computing and mathematics * Heap (data structure), a data structure commonly used to implement a priority queue * Heap (mathematics), a generalization of a group * Heap (programming) (or free store), an area of memory f ...

models)

r \bullet r

might not even be defined. The standard semantics of

\Rightarrow

(or of negation) is often rejected by relevantists in their bid to escape the `paradoxes of material implication', which are not a problem from the perspective of modelling resources and so not rejected by bunched logic. The semantics is also related to the 'phase semantics' of

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. Although the logic has also be ...

, but again is differentiated by accepting the standard (even boolean) semantics of

\wedge

and

\Rightarrow

, which in linear logic is rejected in a bid to be constructive. These considerations are discussed in detail in an article on resource semantics by Pym, O'Hearn and Yang.

Categorical semantics (doubly closed categories)

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 In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in math ...

categories, that is, categories with finite products satisfying the (

natural Nature, in the broadest sense, is the physical world or universe. "Nature" can refer to the phenomena of the physical world, and also to life in general. The study of nature is a large, if not the only, part of science. Although humans are p ...

in ''A'' and ''C'') adjunction correspondence relating hom sets: ::

Hom(A \wedge B, C) \quad \mbox \quad Hom(A, B \Rightarrow C)

Bunched logic can be interpreted in categories possessing two such structures ::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 In mathematics, the tensor product V \otimes W of two vector spaces and (over the same field) is a vector space to which is associated a bilinear map V\times W \to V\otimes W that maps a pair (v,w),\ v\in V, w\in W to an element of V \otimes W ...

construction. Additionally, the implicational fragment of bunched logic has been given a

game semantics Game semantics (german: dialogische Logik, translated as ''dialogical logic'') is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, ...

Algebraic semantics

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 \leq C \quad \mbox \quad A \leq B  C

. The boolean version of bunched logic has models as follows. ::An algebraic model of boolean bunched logic is a poset that is a

Boolean algebra In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, whereas in e ...

and that carries an additional residuated commutative monoid structure.

Proof theory and type theory (bunches)

The

proof calculus In mathematical logic, a proof calculus or a proof system is built to prove statements. Overview A proof system includes the components: * Language: The set ''L'' of formulas admitted by the system, for example, propositional logic or first-order ...

of bunched logic differs from usual sequent calculi in having a tree-like context of

hypotheses A hypothesis (plural hypotheses) is a proposed explanation for a phenomenon. For a hypothesis to be a scientific hypothesis, the scientific method requires that one can test it. Scientists generally base scientific hypotheses on previous obser ...

instead of a flat list-like structure. In its sequent-based proof theories, the context

\Delta

in an entailment judgement

\Delta \vdash A

is a finite rooted tree whose leaves are propositions and whose internal nodes are labelled with modes of composition corresponding to the two conjunctions. The two combining operators, comma and semicolon, are used (for instance) in the introduction rules for the two implications. :

\frac  \qquad \qquad \frac

The difference between the two composition rules comes from additional rules that apply to them. * Multiplicative composition

\Delta , \Gamma

denies the

structural rule In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgment or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic. Logics ...

s of weakening and contraction. * Additive composition

\Delta ; \Gamma

admits weakening and contraction of entire bunches. The structural rules and other operations on bunches are often applied deep within a tree-context, and not only at the top level: it is thus in a sense a calculus of deep inference. Corresponding to bunched logic is a type theory having two kinds of function type. Following the

Curry–Howard correspondence In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relati ...

, introduction rules for implications correspond to introduction rules for function types. :

\frac  \qquad \qquad \frac

Here, there are two distinct binders,

\lambda

and

\alpha

, one for each kind of function type. The proof theory of bunched logic has an historical debt to the use of bunches in relevance logic. But the bunched structure can in a sense be derived from the categorical and algebraic semantics: to formulate an introduction rule for

we should mimick

*

on the left in sequents, and to introduce

\Rightarrow

we should mimick

\wedge

. This consideration leads to the use of two combining operators. James Brotherston has done further significant work on a unified proof theory for bunched logic and variants, employing Belnap's notion of

display logic In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof, a kind of proof whose semantic properties are exposed. When all the theorems of a logic formalise ...

. Galmiche, Méry, and Pym have provided a comprehensive treatment of bunched logic, including completeness and other meta-theory, based on labelled

tableaux The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) is an annual international academic conference that deals with all aspects of automated reasoning with analytic tableaux. Periodically, it joi ...

Applications

Interference control

In perhaps the first use of substructural type theory to control resources,

John C. Reynolds John Charles Reynolds (June 1, 1935 – April 28, 2013) was an American computer scientist. Education and affiliations John Reynolds studied at Purdue University and then earned a Doctor of Philosophy (Ph.D.) in theoretical physics from Harvard U ...

showed how to use an affine type theory to control aliasing and other forms of interference in Algol-like programming languages. 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

Separation logic is an extension of

Hoare logic Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and log ...

that facilitates reasoning about mutable data structures that use pointers. Following Hoare logic the formulae of separation logic are of the form

\ program \

, but the preconditions and postconditions are formulae interpreted in a model of bunched logic. The original version of the logic was based on models as follows: *

Heaps = L \rightharpoonup_f V \qquad

(finite partial functions from locations to values) *

h_0 \bullet h_1 =

union of heaps with disjoint domains, undefined when domains overlap. It is the undefinedness of the composition on overlapping heaps that models the separation idea. This is a model of the boolean variant of bunched logic. Separation logic was used originally to prove properties of sequential programs, but then was extended to concurrency using a proof rule :

\frac

that divides the storage accessed by parallel threads. Later, the greater generality of the resource semantics was utilized: an abstract version of separation logic works for Hoare triples where the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model. 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. 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.

Resources and processes

Bunched logic has been used in connection with the (synchronous) resource-process calculus SCRP 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

in terms of ''both'' parallel composition of systems and composition of their associated resources. The semantic clause of SCRP's process logic that corresponds to separation logic's rule for concurrency asserts that a formula

A * B

is true in resource-process state

R

E

just in case there are decompositions of the resource

R = S \bullet T

and process

E

F \times G

, where ~ denotes

bisimulation In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa. Intuitively two systems are bisimilar if ...

, such that

A

is true in the resource-process state

S

F

and

B

is true in the resource-process state

T

G

; that is

R, E \models A

iff

S, F \models A

and

T, G \models B

. 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.

Spatial logics

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 Extensible Markup Language (XML) is a markup language and file format for storing, transmitting, and reconstructing arbitrary data. It defines a set of rules for encoding documents in a format that is both human-readable and machine-readable. T ...

data.

References

{{reflist Mathematical logic Logic in computer science Substructural logic