Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The logic of bunched implications is undecidable

Nick Galatos, Peter Jipsen, Søren Brinck Knudstorp, Revantha Ramanayake

Abstract

The logic of bunched implications (BI), introduced by O'Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras. Our result is much more general, applying to the {and, or, not, --*}-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then --* splits into two divisions \, /). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable. This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.

The logic of bunched implications is undecidable

Abstract

The logic of bunched implications (BI), introduced by O'Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras. Our result is much more general, applying to the {and, or, not, --*}-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then --* splits into two divisions \, /). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable. This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.
Paper Structure (11 sections, 21 theorems, 73 equations, 5 figures)

This paper contains 11 sections, 21 theorems, 73 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries and Results
  3. Tiling proofs
  4. Refutation of decidability claims in the literature
  5. Proofs of Lemma \ref{['l: dual']} and Lemma \ref{['l: dualBI']}
  6. Reduction from acceptance in ACMs
  7. And-branching counter machines (ACM)
  8. Reduction from ACMs (soundness of the encoding)
  9. Soundness via (G)BI-algebras
  10. A brief review of residuated frames
  11. Completeness of the reduction

Key Result

theorem 2

The tiling problem is undecidable.

Figures (5)

  • Figure 1: The LBI sequent calculus GalmicheMP05:mscs. The $\equiv$ denotes commutative monoid equations for $,$ and $;$ applied to sub-bunches.
  • Figure 2: Examples of (a) tiles that tile $\mathbb{N}^2$, and of (b) tiles that do not.
  • Figure 3: Staircase of grid points.
  • Figure 4: New points: for $m \leq n$ (left) and $m>n$ (right).
  • Figure 5: Constructing the full grid of points.

Theorems & Definitions (43)

  • definition 1: Formulas, bunches, and sequents
  • definition 2: BI-algebras
  • Remark 1: The algebra $\mathcal{P}_{\omega}(\mathbb{N})^+$
  • definition 3: GBI-algebras
  • definition 4
  • definition 5: Wang tiling
  • theorem 2: Berger
  • lemma 1
  • lemma 2
  • theorem 3
  • ...and 33 more