Discussing 'The Semantics and Proof Theory of the Logic of Bunched Implications'

(Link to reference; note not available online).

Author: David J. Pym (University of Bath)

Reference: Applied Logic Series Vol. 26, Kluwer Academic Publishers, 2002.

Why this paper? Cited by 4 (of a possible 31) of the papers in my Google Scholar Updates recommendations.

This week's most cited paper from among my Google Scholar Updates recommendations is a book, which I admittedly have not read through in its entirety for this discussion, but have enjoyed the excuse to flip through.

The logic of bunched implications, abbreviated BI, is similar to the linear logic I discussed last time, combining as it does 'normal logic' with a 'substructural' part that disallows the powerful inference rules of weakening and contraction. The technical difference between the two logics is that linear logic lacks a first-class normal implication (if... then...), usually considered to be the most important logical connective, but Girard showed that it can be reconstructed out of substructural implication and the '!' connective. As ingenious as that construction is, it demands a relationship between the normal and substructural connectives that it too tight for some applications. BI instead takes the conceptually rather simpler view that the normal and substructural logical connectives should be 'ships passing in the night' with no explicitly required interaction - which is not to say that they cannot be freely mixed together to create interesting theorems, but rather that one set of connectives does not depend on the other in any fundamental way.

I mentioned applications in the previous paragraph, and it is the breadth of concrete mathematical and computational constructions that can be understood via the logic BI that make it interesting. Nominal sets, the model of names in computing applications, provide such an example. In this setting propositions depend on finite set of names. The normal 'and' is defined in the usual way - 'p and q' is true if p is true and q is true. But the substructural conjunction, usually written with a star *, can be defined as follows: p * q is true if p is true and q is true and they do not share any names. The substructual implication is a bit trickier to define, and in fact I wrote a paper mostly about this very topic. Note that with this definition of * nominal sets do not define a model of linear logic (in the sense that we cannot define a ! connective with the required properties), showing that BI really is the 'better logic' for this application. A more famous application of BI is separation logic, a prominent formal methods technique for reasoning about programs, in which the * connective permits reasoning about the content of memory.

There is a lot of material in this book which I am not mentioning, of course. I will merely briefly note the proof theoretic notion of bunches that give the logic its name. These are essentially a richer notion of 'structure' than the lists (or sets) of propositions used by traditional proof systems; the idea of using more complicated structures in proof theory is reminiscent of the display calculi which I discussed recently.