This is about some recent advances on Bewl, my 10% time project at Springer. It’s a rather unusual project based on some quite advanced math, and may yet give insights into diverse math-related areas. Bewl is a language for doing set-like calculations with objects that are not sets. More precisely, Bewl is a domain specific language (DSL) for topos theory. That’s quite a mouthful, so let me explain.

Most calculations in math are based on sets. We have developed very strong intuition and expressive, compact notation for doing these calculations. So it is remarkable that with some minor changes, essentially the same language can be used to describe and manipulate objects in much wider classes of workspace. I believe that this will open up many unexplored possibilities. As applied to graphs (for instance) it will enable us to construct new graphs and investigate properties of them that we may not currently even know how to discuss.

Although these ideas seem promising, understanding and applying them is not easy. Topos theory is very abstract, perhaps as abstract as a branch of math can be. Like quantum mechanics, it requires a painfully disorienting process of scrapping your existing mental model and developing a new one. Many conceptual leaps are needed to develop the right vocabulary: that is, to identify and separate out concepts which we have accepted for so long as our mental furniture that it seems pedantic and unnatural even to invent names for them. The other side of the coin is that once you have made the leap, adopting the topos-theoretic point of view almost makes it impossible to do conventional math, because it so clearly highlights sets as an annoying legacy platform like MS-DOS 2.0 which ought to be optimized away.

To explain all this, I’ll first explain what I’m trying to do as a kind of ‘arithmetic of sets’ by analogy with the historical development of number systems. Then I’ll outline how it might be meaningful to talk about things like graphs and permutations as if they were sets. Finally I’ll give a summary of where Bewl is now.

Number systems

We first understand arithmetic in terms of the four operations ( + - * / ) as applied to the natural numbers ( 0, 1, 2, 3, …). Part of what makes these operations useful is that they obey certain laws that enable us to make shortcuts when working with them. For example a + b = b + a, and (a + b) + c = a + (b + c) ; together these laws tell us that we can add up a list of numbers in any order, grouping them however we like, and get the same total. These laws are so deeply embedded into our understanding of arithmetic that it almost seems unnecessary to point them out, but they are what makes arithmetic possible in the first place. The laws empower us to apply the intuitions we use every day.

We take the four functions of arithmetic for granted, but they must have emerged only by a long and tortuous process of abstraction. This process started with cavemen using piles of cowrie shells to do accounting transactions on a prehistoric beach, and it led to the four functions of arithmetic being enshrined in the school curriculum. Today it requires an unfamiliar mental effort to understand what that process must have involved.

Skating over many details, one arrives at the definition of a field as a collection of values equipped with operations ( + - * / ) satisfying a list of algebraic laws like commutativity of addition (a + b = b + a). The complex numbers form a field; so do integers modulo 11. It is then possible to develop a kind of science of number systems by studying fields. One can develop structure theories for them, construct new ones, and so forth.

Historically, one can see the development of arithmetic as a process of building larger and larger number systems as the limitations of each one are outgrown. Starting with the natural numbers N, one seeks a more satisfactory theory of subtraction (-), and so extends to the integers Z. Next, to get a better theory of division (/), one extends to the rational numbers Q, which form a field. After that come the real numbers R, the complex numbers C, and so on. We can use much the same language to do arithmetic in all of these systems, which also happen to provide a range of useful workspaces for applications outside pure math.

To summarize:

• from calculations with numbers, extract the operations ( + - * / ) and their algebraic laws
• define a field as a system equipped with operations satisfying these laws
• identify naturally occurring examples of fields
• explore the consequences of doing arithmetic in these systems
• develop constructions for building bigger and better fields out of existing ones

The first stage is the hardest, picking out the defining properties of the workspace under consideration. What happens when this process is applied to sets instead of numbers? The answer is topos theory.

Topos theory on the back of a postcard

Topos theory is a branch of mathematics which applies what programmers would call an aggressive refactoring to the category of sets - a foundational workspace within which almost all of conventional math is conducted (whether the practitioners realize it or not).

The steps in building the theory are:

• define the concept of category, a workspace of dots and composable arrows between them
• identify the category Sets as fundamental
• abstract out the operations and laws that make Sets useful
• define a topos as a category equipped with operations obeying these laws
• find other naturally occurring examples of topoi
• via internal categories, understand topoi as a complete foundation for math
• specify a language for describing constructions and deductions in a topos

So the topos theorists have already done the hard work. They have rewritten the foundations of mathematics to distil out the mechanics of set-like reasoning (used for almost all conventional math) to allow almost similar calculations on more general objects that aren’t sets.

But doing calculations in topoi is hard, like doing arithmetic the old fashioned way; consider trying to do long division without even having a slide rule.

The motivation for Bewl was to make it easier to explore topoi by doing these calculations in software.

Towards an arithmetic of set-like objects

Consider the following classes of objects:

• finite sets
• graphs
• fuzzy sets
• permutations

Each of these forms a topos, a workspace in which certain combinatory operations are possible.

Just as we can use the familiar operations ( + - * / ) to work with numbers, so we can use a modified set of four operations to work with sets: (+ * ^ Ω). The first three of these are addition, multiplication and exponentiation. As applied to sets, they work as ‘lifts’ of the corresponding operations on numbers. What I mean by this is that, for example, the size of A + B is just the size of A plus the size of B. So A + B is a disjoint union of A and B, something you’d get by photocopying A and putting it next to a separate photocopy of B. Without getting bogged down in the details, you can see that each set can be seen as representing the number that counts its elements. The pseudo-operation Ω is a bit more complicated and I won’t attempt to describe it here, except to say that every topos has an ‘object of truth’ which encodes the truthiness of logical statements. For sets, the situation is simple: the truth object is just the two-element set { true, false } with their ordinary meanings.

Taking graphs as an example, addition (+) is just the operation of combining two graphs together by putting them side by side, as with sets. It is obvious that this operation + obeys the laws you might expact, like A + B = B + A, and 0 + A = A where 0 is the empty graph.

It is not so obvious that there are also constructions of multiplication and exponentiation for graphs, which obey the expected arithmetic-type laws such as distributivity:

A * (B + C) = (A * B) + (A * C)
A ^ (B + C) = (A ^ B) * (A ^ C)

This essentially means that you can do a form of arithmetic with graphs. But we’re already not in Kansas anymore; for graphs, the truth object is more complicated (there is a non-Boolean ‘graph of truth’) and a lot of small print is involved in making sure that the definitions all fit together properly and obey the right laws. Once the internal language is applied, we go beyond doing four-function arithmetic with these operations, into an interesting new world where we are talking richly about graphs in their native language. I would guess that some of the constructions already known to graph theorists are echoed here, but that a lot of it will be entirely new.

It’s a similar story for fuzzy sets (appropriately defined, with a concept of variable membership) and permutations. The Bewl DSL offers a new and more expressive language in which to talk about their theories. (To touch on a separate mystery that this might help explain, I believe that the current theory of permutation parity (which classifies rearrangements of a finite set as either odd or even) is inadequate, and that investigating the topos of permutations using Bewl might illuminate it.)

This is only a taste, and there are many other naturally occurring examples of topoi, but at least you can see that Bewl might have something to say about some quite diverse types of object, and it may be intriguing that there could be a single language capable of all this.

A history of the project

Bewl was partly inspired by this music theory paper, whose calculations in the topos of triads must have been very awkward without a computer. It seemed worthwhile to try writing software to facilitate this kind of calculation. Also, the Mitchell-Benabou internal language seemed to be a natural fit for a DSL.

So the most immediate requirement was to write a kind of four-function calculator for topoi. First I had to translate the topos axioms into software, resulting in an application programmer interface (API) for which one could then write implementations. The DSL then re-emerges as a high level alternative to the low-level ‘categorical machine-code’ provided by the bare topos API.

Bewl has twice outgrown the programming language it was written in. I wrote an initial version in Java, then ported it to Clojure and finally Scala, which so far has been a perfect fit: the DSL is tightly integrated with Scala’s type system in a way which wouldn’t have been possible with the first two languages.

There are several topos implementations so far:

• finite sets
• permutations
• group actions
• monoid actions

For the last three, it turned out to be easier to work in greater generality, and so they actually work for algebraic structures defined inside the topos itself. Thus, given a group object G in a topos T, I can construct the topos of G-actions considered as objects within T.

The last topos implementation listed is the only way to construct a non-Boolean topos. Unfortunately the current code is very slow. However the most recent breakthrough is an idea for speeding it up, based on some straightforward computational algebra. This is the current focus of activity in Bewl.

If I can do that, significant insights may emerge, because the theory of monoid actions seems to be a neglected field with some interesting connections to semigroups, automata and the theory of music.