Residuated lattices provide the algebraic semantics of substructural logics, and Boolean algebras with operators (BAOs) give the algebraic semantics of polymodal logics. Bunched implication logic has found interesting applications in the past decade in the form of separation logic for reasoning about pointers, data structures and parallel resources. Generalized bunched implication algebras (GBI-algebras) are Heyting algebras expanded with a residuated monoid operation, and they provide the algebraic semantics of (noncommutative) bunched implication logic. As such, they fit neatly between residuated lattices and residuated BAOs. We survey this ordered algebraic landscape within the framework of lattices with operators, showing how the general theory of residuated lattices applies to the special cases of GBI-algebras and residuated Boolean monoids. In particular we will discuss the dual structures (topological contexts, Esakia spaces and Stone spaces, each with additional relations) and their non-topological versions (contexts, intuitionistic frames and Kripke frames), as well as their applications in algebraic proof theory. We will indicate why the Boolean varieties generally lack decision procedures for their equational theories, whereas GBI-algebras, residuated lattices and several of their subvarieties are equationally decidable. We also consider some algorithms for enumerating finite algebras in each of these varieties, and present computational tools that are useful for exploring ordered algebraic structures.
展开▼
