Bunched Implications

Origin. O'Hearn and Pym introduced bunched implications (BI, 1999). Combines intuitionistic logic with linear/resource logic. Two conjunctions: additive (∧) and multiplicative (*). Foundation for separation logic. Substructural logic with resource sensitivity.

Models. Resources that split and combine. Intuitionistic logic: truth persists, premises can be reused. Linear logic: use each premise exactly once. BI: have both — some resources are reusable, some are consumable. Models heap memory: disjoint combination (*) and sharing (∧).

Formalism.

BI syntax: φ ::= p | ⊤ | ⊥ | I | φ ∧ ψ | φ ∨ ψ | φ → ψ | φ * ψ | φ —* ψ

Two conjunctions:

φ ∧ ψ: additive (intuitionistic) — shared resources
φ * ψ: multiplicative — disjoint resources

Two implications:

φ → ψ: intuitionistic implication — reusable
φ —* ψ: multiplicative implication (magic wand) — resource-consuming

Units:

⊤: additive truth (always available)
I: multiplicative unit (empty resource)

Kripke resource semantics: Frame: (W, ≤, ∘, e) where:

W: resource worlds
≤: resource extension (intuitionistic)
∘: W × W → W resource combination (monoidal)
e: unit element

w ⊨ φ * ψ iff ∃w₁, w₂. w = w₁ ∘ w₂ and w₁ ⊨ φ and w₂ ⊨ ψ w ⊨ φ —* ψ iff ∀w'. w ∘ w' defined and w' ⊨ φ implies w ∘ w' ⊨ ψ

Boolean BI (BBI): Classical version: adds excluded middle for additive connectives. Used in separation logic.

Symbols.

Symbol	Unicode	Name	Meaning
*	—	Separating conjunction	Disjoint combination
—*	—	Magic wand	Separating implication
∧	U+2227	Additive conjunction	Shared resources
→	U+2192	Implication	Intuitionistic
I	—	Emp	Empty resource
⊤	U+22A4	Top	Always true
∘	U+2218	Composition	Resource combination

Metatheory. BI is decidable (PSPACE-complete for propositional). Boolean BI undecidable. Cut-elimination holds. Display calculus provides proof theory. Semantics: partial commutative monoids. Categorical: Day convolution on presheaves. Separation logic = BBI + memory model.

Applies to. Separation logic foundation. Memory and resource verification. Concurrent resource reasoning. File system verification. Linear/affine type systems. Access control (RBAC). Information flow.

Limitations. More complex than pure intuitionistic logic. Frame problem for —*. Tool support less than separation logic. Boolean BI undecidability limits some applications. Choosing between * and ∧ requires care. Metatheory still being developed for extensions.