nLab bunched logic

Idea

In formal logic, and more specifically in sequent calculus/natural deduction/type theory, a bunched logic is a logical theory in which the formulas appearing in any context are not necessarily just a list but have some additional structure, usually that of tree whose nodes are then the eponymous “bunches”:

Where a classical context is traditionally presented as a comma-separated list of propositions and/or types, e.g.

$$\Gamma ,\; X ,\; Y \;\;\; ctxt \,,$$

which classically may always be thought of as a (dependent) classical product type

$$\Gamma \times X \times Y \;\;\; ctxt \,,$$

so a context in bunched logic is allowed, more generally, to be a nested list of structural connectives, iterating between this comma-denoted conjunction and another connective typically denoted by a semicolon, e.g.:

$$A,\; B,\; \big( C;\; (D,\,E); \; F \big),\; (G;\,H) \;\;\;\; ctxt \,.$$

The original and common motivation for such “bunched contexts” is the existence of further (function types and) product types in addition to the classical ones; such as in linear type theories with their additional (linear implication $(-)\multimap (-)$ and) linear conjunction $(-)\otimes (-)$, and more generally in the internal logic of a doubly closed monoidal category, whence bunched contexts as above may usefully be thought of as types formed consecutively from cartesian products and another tensor product:

$$A \times B \times \big( C \otimes (D \times E) \otimes F \big) \times (G \otimes H) \;\;\;\; ctxt \,.$$

(NB: In saying this we are reversing the role of commas and semicolons as compared to the original literature on bunched logic, so that the comma retains it original meaning as the classical connective.)

Accordingly, the bunched context indicates a variation of structural rules: The classical product $\times$ will admit the contraction rule and/or the weakening rule, while $\otimes$ may not.

Notice that the general phrase bunched logic is not entirely standard, and the word “bunches” has been used with more than one logic of this form.

The notion (together with its categorical semantics in doubly closed monoidal categories) originates with the logic of “bunched implication” (BI) and its “$\alpha \lambda$-calculus” (a bunched variation of the lambda-calculus) due to [O’Hearn & Pym (1999), Pym (2002), see also O’Hearn (2003).

But aspects of the proposal of O’Hearn & Pym (1999) and Pym (2002) have remained unsatisfactory, see Pym (2008), Errata to Pym (2002) and Riley(2022), pp. 19 and Rem. 1.4.1 (p. 64):

[Riley 2022, pp. 19]: [Since] context manipulations are not recorded in the terms, typechecking a term can be difficult. First, it is not always obvious when and how the contraction rule has to be applied, and secondly, it is not always obvious how the context has to be split into two pieces to apply $\multimap$-ELIM. Besides the challenge of typechecking, the combination of the weakening rule and the rules for the monoidal unit also breaks soundness for the intended semantics.

The various extensions of the αλ-calculus that have since appeared [BO06; CPR08; SS04; Atk04] do not resolve these issues. It is also not so clear how to add dependent types to this system and how dependency should behave between bunches.

Further developments had not resolved the fundamental issue:

[Riley 2022, p. 91:] Schöpp and Stark’s Bunched Dependent Type Theory [Schöpp & Stark (2004)] [admits] no dependency across bunches. The corresponding monoidal pair type therefore requires the input types to be closed. […] the monoidal unit is the terminal object. This is certainly not the case in [linear] models of interest.

In reaction to this, Riley (2022) proposes an enhanced form of bunched type theory which is claimed to fix all these problems at least in the case that the second structural connective $\otimes$ is a multiplicative conjunction in a linear type theory, hence for a form of dependent linear type theory. The key new ingredients in Riley (2022) to make this work are:

1. a classical modality $\natural$ which from any “parameterized linear type” projects out the underlying classical type;

2. a decoration of bunched contexts by “color palettes” which keep explicit track of the bunching/tree structure.

(On the other hand, this second point leads to a proliferation of inference rules, but maybe that’s what it takes.)

Examples

Bunched implications

In bunched implications logic (O’Hearn & Pym (1999)), the semicolon allows contraction and weakening while the comma does not. This allows defining both an additive conjunction and a multiplicative conjunction, internalizing the semicolon and the comma respectively, such that both distribute over the “” additive disjunction and moreover both come with a corresponding implication: the “additive” implication and the multiplicative implication.

Relevance logic

Some forms of relevance logic can be presented with a bunched sequent calculus that is similar to BI, but in which the comma also has contraction (though not weakening) and there is no additive implication. See for instance (Mints).

Classical bunched implication

A logic of classical bunched implication is like BI but with arbitrary bunches on the right as well as on the left. On the right, the semicolon represents the additive disjunction and the comma represents a multiplicative disjunction, and there are both an additive and a multiplicative negation that move formulas back and forth. Both negations are “classical” with respect to their corresponding connectives, e.g. we have $\sim\sim A \multimap A$ (where $\sim$ is the multiplicative negation and $\multimap$ the multiplicative implication) and also $\neg\neg A \to A$ (where $\neg$ is the additive negation and $\to$ the additive implication). See Pym 2002 and this discussion.

Dependent versions

Bunched logics are also used to combine linear type theories with dependent type theories. See some of the references at dependent linear type theory.

Categorical semantics

Bunched logics naturally have semantics in categories with more than one monoidal structure, so that a bunch such as $(A,(B;C),((D,E);F))$ can be interpreted as $A \otimes (B\boxtimes C) \otimes ((D\otimes E)\boxtimes F)$. Frequently (e.g. if one kind of bunch admits contraction and weakening) one of the two monoidal structures is a cartesian one. A typical and motivating example of a model for BI is the category of presheaves $[C^{op},Set]$ over a monoidal category $C$, which comes equipped both with the ordinary ccc structure on presheaves as well as the closed monoidal structure given by Day convolution.

Related pages

• linear logic

• doubly closed monoidal category

• relevance logic

• separation logic

• display logic

• substructural logic

• monoidal topos

References

Precursors:

• G. E. Mints. Cut-elimination theorem for relevant logics, Zap. Nauchn. Sem. LOMI, 1972, Volume 32, Pages 90–97. (math-net.ru). An English translation appears in the Journal of Soviet Mathematics 6 (1976) 422-8 [doi:10.1007/BF01084083]

The original articles:

• Peter O'Hearn, David J. Pym, The Logic of Bunched Implications, The Bulletin of Symbolic Logic 5 2 (1999) 215-244 [pdf, doi:10.2307/421090]

• David Pym, The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series 26, Springer (2002) [doi:10.1007/978-94-017-0091-7, GoogleBooks]

  Errata and Remarks for The Semantics and Proof Theory of the Logic of Bunched Implications (2008) [pdf, pdf]

  [p. 5] “Items 3, 4, and 5 in the errata for Chapter 12 and 4, 5 in Chapter 13, whilst necessary to fix a technical problem, leave us in a conceptually and computationally undesirable situation: we have no clean characterization of a useful notion of well-formedness, leading to obvious computational difficulties in, say, theorem proving. We conclude that such a highly multiplicative system is far too complex, at least in its current formulation, to be of much value. All of the applications of multiplicative quantifiers known to-date require much simpler systems. It is the author’s recommendation that readers should not devote very much of their resources to studying the system of predicate BI discussed in these chapters”

• Peter O'Hearn, On bunched typing, Journal of Functional Programming 13 4 (2003) 747-796 [doi:10.1017/S0956796802004495]

Review and further development:

• Bodil Biering, On the logic of bunched implications – and its relation to separation logic, MSc thesis, Copenhagen (2004) [pdf]

• Brotherston and Calcagno, Classical BI: Its Semantics and Proof Theory, arxiv

Discussion of bunched logic with the linear logic-part regarded as a quantum logic:

• Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, A Quantum Interpretation of Bunched Logic for Quantum Separation Logic, LICS ‘21: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science 75 (2021) 1–14 [arXiv:2102.00329, doi:10.1109/LICS52264.2021.9470673]

A bunched dependent type theory, to some extent:

• Ulrich Schöpp, Ian Stark, A Dependent Type Theory with Names and Binding, in Computer Science Logic. CSL 2004, Lecture Notes in Computer Science 3210 (2004) 235–249 [doi:10.1007/978-3-540-30124-0_20, web]

Further refinement to dependent bunches for a dependent linear homotopy types:

• Mitchell Riley, A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis (2022) [doi:10.14418/wes01.3.139, ir:3269, pdf]

• Mitchell Riley, Linear Homotopy Type Theory, talk at: HoTTEST Event for Junior Researchers 2022 (Jan 2022) [slides: pdf, video: YT]

• Mitchell Riley, Dependent Type Theories à la Carte, talk at CQTS Initial Researcher’s Meeting (Sep 2022) [pdf]