nLab bunched logic

Redirected from "bunched type theory".
Bunched logic

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

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.

Γ,X,Yctxt, \Gamma ,\; X ,\; Y \;\;\; ctxt \,,

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

Γ×X×Yctxt, \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,(C;(D,E);F),(G;H)ctxt. 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×B×(C(D×E)F)×(GH)ctxt. 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 AA\sim\sim A \multimap A (where \sim is the multiplicative negation and \multimap the multiplicative implication) and also ¬¬AA\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))(A,(B;C),((D,E);F)) can be interpreted as A(BC)((DE)F)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][C^{op},Set] over a monoidal category CC, which comes equipped both with the ordinary ccc structure on presheaves as well as the closed monoidal structure given by Day convolution.

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:

A bunched dependent type theory, to some extent:

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

Last revised on February 7, 2024 at 16:59:41. See the history of this page for a list of all contributions to it.