An Algebraic Glimpse at Bunched Implications and Separation Logic

TL;DR

This paper explores the algebraic structures underlying Bunched Implications and Separation Logic, introducing generalized BI algebras and duality results, and applies these to various models and proof techniques in substructural logics.

Contribution

It introduces GBI-algebras as a unifying algebraic framework for BI and SL, and develops duality and decidability results, connecting algebraic and proof-theoretic perspectives.

Findings

Unified algebraic framework for BI and SL models

Duality theory for GBI-algebras established

Decidability results derived from algebraic approach

Abstract

We overview the logic of Bunched Implications (BI) and Separation Logic (SL) from a perspective inspired by Hiroakira Ono's algebraic approach to substructural logics. We propose generalized BI algebras (GBI-algebras) as a common framework for algebras arising via "declarative resource reading", intuitionistic generalizations of relation algebras and arrow logics and the distributive Lambek calculus with intuitionistic implication. Apart from existing models of BI (in particular, heap models and effect algebras), we also cover models arising from weakening relations, formal languages or more fine-grained treatment of labelled trees and semistructured data. After briefly discussing the lattice of subvarieties of GBI, we present a suitable duality for GBI along the lines of Esakia and Priestley and an algebraic proof of cut elimination in the setting of residuated frames of Galatos and Jipsen. We also show how the algebraic approach allows generic results on decidability, both positive and negative ones. In the final part of the paper, we gently introduce the substructural audience to some theory behind state-of-art tools, culminating with an algebraic and proof-theoretic presentation of (bi-)abduction.