Discussing "Sketches of an Elephant: A Topos Theory Compendium"

Links: Volume 1 and Volume 2

Author: Peter T. Johnstone (University of Cambridge)

Reference: Johnstone, Peter T., Sketches of an Elephant: A Topos Theory Compendium: Volume 1 and 2. Oxford University Press, 2002

Why this book? Cited by Groupoid-Valued Presheaf Models of Univalent Type Theory, KZ-monads and Kan Injectivity, and Classifying Topoi in Synthetic Guarded Domain Theory

The algorithm I follow to choose topics for this blog, where I take the most highly cited paper from my recent Google Scholar recommendations, can send me off to anything from a short conference paper to a full book. I like the variety, but of course a short blog post can only say so much about a book based on a week of reading pushed in around my other commitments; this was never more true than this week, given the monumental scale and density of these two volumes. The introduction even warns one off reading the book from start to finish; it is intended to be a tome one can dip into to find all manner of important facts in topos theory, including full proof details.

The title of the book refers to the ancient parable of the blind men and the elephant, where men touching different parts of the elephant come to different conclusions about its nature. The book is structured around sections describing the category theoretical notion of topos in different ways - as a category, as a 2-category, as a space, and as a logical theory (the latter being my main focus). The contents for a third volume are also included, covering homotopy / cohomology and mathematical universes, but more than twenty years later this is perhaps as likely to appear as the final Game of Thrones novels – but who knows?

The central definition of a topos in category theory is quite simple for something that can inspire so many pages of work, but this is in keeping with the usual nature of category theory – simple abstract definitions with many examples, which help to organise the structure of mathematical thought and provide connections between apparently unconnected areas. The distinctive concept here is that of subobject classifier, which can be seen as an object of ‘truth values’.  Classically, one can use the two element set of the Booleans True and False, but, to take a contrasting example, in the topos of trees the subobject classifier provides for an infinite-valued logic, as I discussed a few weeks ago. In any topos, the logic provided for by the subobject classifier is at least intuitionistic, but need not be classical (admitting the law of excluded middle, double negation elimination, and so on).

What do I mean by the ‘logic provided for’? To skip ahead to the logic section in the second half of the second book, a lot can be achieved without going all the way to toposes. For example, (sorted) first-order logic of the kind one might be taught in an introductory logic course can be interpreted in any Heyting category, which is a weaker definition than topos. The full power of toposes are not needed to interpret logical theories until one reaches for higher-order logic; in particular the ability to have variables ranging over subsets of a sort (more generally, type), and to sensibly use the set membership symbol ∈, requires the subobject classifier. Having said that, toposes do have their uses as an analytic tool before we get to such powerful logics, as each theory (collection of axioms) expressed with the weaker logics can be aligned to a ‘classifying topos’ which contains a universal model of the theory – a model that satisfies all and only the theorems entailed by the theory.

I should finish by mentioning one of the most stunning achievements of topos theory (to my mind; given the nature of the elephant a topologist would probably come up with something else), which is the connection of the notion of classical logic (certain toposes are Boolean, which means that their underlying logic will be classical) to the axiom of choice much discussed in mathematics. The results, rewarding one for getting 991 pages into the book (or skipping forward to them, as is more to be advised) give a description of Booleans toposes exactly in terms of the choice functions of certain of their objects, and, following Zermelo’s theorem, show that in any topos (including non-Boolean) the objects with choice functions are exactly those that are well-orderable. These results, and others around them, bring a remarkable new clarity to the connections between two of the most discussed concepts in the foundations of mathematics, classicality and choice.

Discussing "Separation Logic: A Logic for Shared Mutable Data Structures"

(Link)

Author: John C. Reynolds (Carnegie Mellon University)

Reference: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 55-74, doi: 10.1109/LICS.2002.1029817.

Why this paper? Cited by On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs, Compositional Verification of Interacting Systems Using Event Monads, and Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq.

How can we be sure that the programs we write do what they’re supposed to? An answer from the late 1960s is Hoare logic, which gives a formal relationship between programs and specifications. Crucially, Hoare logic can be used in a modular way, in the sense that parts of the program can be reasoned about separately, rather than demanding that an entire program must be reasoned about all at once – a completely impossible task even for some relatively small programs.

Traditional Hoare logic becomes unusable in the face of languages (for example, C) that allow the direct manipulation of memory within the code. Because there is nothing to stop two different program variables pointing to the same physical piece of memory, a manipulation that only seems to effect one variable may also effect another, even if that variable exists in some long distant piece of code. However, the direct manipulation of memory (and potential for ‘sharing’ that this creates) can be extremely useful, as can be seen in various examples in this paper by Reynolds. For example, we see a list reversal where instead of creating a new list that is a reversal of the input, we take the memory-saving approach of reversing by swapping values within the list.

This paper introduces the term separation logic, but mostly reports and summarises previous work by Reynolds and others (primarily Peter O’Hearn, Samin Ishtiaq, and Hongseok Yang, with inspiration from Rod Burstall and David Pym). The key innovation of this group is to change the logical language in which specifications can be stated. A separating conjunction ∗ joins the usual list of logical operators, with a proposition of form P ∗ Q holding if P and Q hold of entirely separate parts of memory. This allows modular reasoning to be restored via a frame rule that says that a true statement about a fragment of one’s code remains true if put in the context of other memory, so long as that extra memory remains separate from the fragment in question. Another connective called separating implication also joins the party, along with a constant stating that no memory is in use, and some syntax to allow one to talk about the content of memory. The paper goes on to present a treasure trove of examples, extensions, and directions for the future, with a heavy emphasis on the application of the logic to a variety of data structures and program constructs.

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.

Discussing 'A New Approach to Abstract Syntax with Variable Binding'

(Link).

Authors: Murdoch J. Gabbay and Andrew M. Pitts (University of Cambridge)

Reference: Formal Aspects of Computing Vol. 13(3-5), pp 341-363 (2002).

Why this paper? Cited by 9 (of a possible 29) of the papers in my Google Scholar Updates recommendations (where multiple citations from different papers by the same author(s) in my recommendations are disregarded).

Comments: My PhD and some of my subsequent research was built around something called nominal techniques; this is the journal version of the conference paper that introduced them (in fact the second author, Andrew Pitts, was my PhD supervisor). Already some clarification is necessary: computer science has for some reason developed an unusual publication culture in which peer-reviewed conferences, rather than journals, take center stage. But conference publication often imposes tight space limits on papers, which can force authors to tighten their prose, which I find no bad discpline, but more regrettably can mean some details or examples are omitted. Hence new research is often published twice, with a more detailed 'journal version' following the conference version, often years later because of the slowness of the journal review process (which itself is probably contributed to by so much work having to be reviewed twice!). Another clarification to my first sentence is that the word 'nominal', which has become the brand name under which all developments of this work by Gabbay and Pitts are grouped, does not appear in this paper. I believe it was introduced by Pitts in his 'Nominal logic' paper, which was published before this paper but written after it, thanks again to the vagaries of academic publication.

The problem this paper addresses is that of reasoning formally in the presence of names and binding, ubiquitous features of computer science applications and other formal settings like mathematics. Of course names are everywhere - think of variable names in programs, or the identifiers like x and y we use when we do maths. The precise names we use is at some level arbitrary; while we're doing our mathematical manipulations we better keep track of our xs and ys, but 'from the outside' it obviously wouldn't have mattered if we'd called our variables foo and bar instead. Binding (sometimes, scope) is simply the point where this 'outside' versus 'inside' distinction is made: some operations have the property that the choices of names inside the operation's domain are irrelevant to anything outside that operation's domain. Such structure is vital in software engineering applications where people worry about encapsulation, but is in fact virtually unavoidable in any sufficiently interesting formal setting.

Anyone with a passing interest in computing, or even logic or mathematics, would nod along to most of the previous paragraph, but perhaps would not become greatly interested. Names and binding are basic machinery, and there is no reason to spend time thinking about them, as opposed to getting on with using them! The twist comes when one tries to reason fully formally, for example to convince a computer that a certain program has a certain desirable property. This sort of reasoning, if successful, can yield guarantees about software far more robust than mere testing, but it is not easy, and names and binding structure turns out to be be one of the (many) barriers to doing this successfully. In particular, proofs involving structural induction, which are vital to programming languages applications in particular, do not play well with bound names. So there is a problem to be solved.

The solution proposed by Gabbay and Pitts (I should note that other candidate solutions exist, but I will not discuss them here) is to change the set theoretic foundations on which we build our mathematics, from the standard one to an alternative framework developed by Fraenkel and Mostowski in the 1930s for reasons completely unrelated to computer science. In this framework certain elements called atoms claim a privileged place, giving mathematics in this universe a slightly different flavour. This paper adapts this work in (to me) wildly surprising fashion to show that if we view these atoms as our names then we have just the right 'universe' in which to model, and reason in a reasonably intuitive way about, binding, up to and including the structural induction I mentioned earlier.

It should be acknowledged, of course, that doing mathematics in a 'different universe' sounds like an cumbersome (and possibly eccentric!) move. For this stuff to actually be used, the esoteric set theory needs to be at least partially hidden, and subsequent work, most notably the 'nominal logic' paper I mentioned above, has helped to do this. Still, all of the many subsequent applications of Gabbay and Pitts's work can be seen to rest on some of the most abstruse mathematics you can imagine, a story that must gladden the heart of any working theoretician!