The invisible map

Let’s talk about writing computer code which corresponds to mathematics.

The basic idea: our code will correspond to mathematical definitions and proofs, and our code will compile if and only if our proofs are correct. Such systems do exist — but in this post, we will just imagine what this kind of code might look like, and how easy it would be for a mathematician to write it. The “de Bruijn factor” of a system like this is the ratio (size of program which proves a theorem in our system) / (size of LaTeX file which proves the same theorem), and ideally this number should be small.

The question we immediately run into is: what will our logical foundations be, or in other words which computer language we are going to use to write our computer code. Most mathematicians either know nothing about foundations (they just know that maths works, like Gauss and Euler knew), or they know that one possible choice for a foundational system is “set theory”.

Set theory

OK now let’s imagine writing code in a computer language corresponding to set theory. So what do we have? Well, we have one kind of object in this system, and it’s called a set. Everything is a set. Those set theory people have checked that what we call functions can be encoded as sets, an ordered pair or ordered quadruple of sets can be encoded as a set (in more than one way, so we just choose a way and stick to it), and even everyday objects such as groups and rings can be considered as sets. For example, a group is an ordered quadruple $(G,m,i,e)$ with $G$ a set, $m:G\times G\to G$ a function called multiplication (remember that $m$ is actually a set), another function $i:G\to G$ (inversion) and finally an element $e \in G$ called the identity element. Even $e$ is a set, because everything is a set. However asking what the elements of $e$ are is a “wrong question” in group theory somehow.

Ok so now we’re writing computer code, and we have variables because computer code has variables, and we have some variable $M$ , and it’s a set. But actually we are doing algebra, so we’re not actually thinking about $M$ as a set, and looking it, actually we can see that $M$ is some kind of ordered triple, and it is called $M$ , and so it is probably a monoid, or a module, or a metric space or something. Except that it isn’t, it’s just a set. We might accidentally call two things $M$ (who hasn’t seen this happen in maths lectures!) and this might lead to hard-to-debug problems. What’s even worse, is that in theory the set $M$ could genuinely represent more than one mathematical object. Perhaps somebody writing the library on natural numbers decided to define $3$ to be the set $\{0,1,2\}$ , and more generally they defined $n$ to be the set $\{0,1,2,\ldots,n-1\}$ . Then someone doing topology defined a topology on a set $X$ to be a set of subsets of $X$ satisfying some axioms. It then turns out that $3$ is a topology on $2$ (check it! It’s really true!). Someone making the library for symmetric groups had to decide how to make the symmetric group $S_n$ on $n$ elements, and they decided it was going to be permutations of the set $\{1,2,3,\ldots,n\}$ . Now think about what $S_n$ actually is if you do it this way — it will depend on your definition of ordered quadruple, but will ultimately be just a set whose elements are sets which will happen to be things like numbers, or sets of numbers, or sets of subsets of numbers, or sets of numbers which happen to also be numbers by coincidence. That’s all it is. And now imagine someone else doing some basic combinatorics who is looking at a question about collections of subsets of $\{1,2,3,\ldots,n\}$ , and then it turns out that $S_2$ is by complete coincidence an example of such a subset. Do we really want $M$ to genuinely represent more than one thing? What happens when we want to change the variable $M$ to be something else? “Let x=x+1” is an actual thing in computer code! When changing the topology on our set $X$ , could this mean that the meaning of the number 3 changes in a different part of our code? It might be funny that one way of setting up the natural numbers means that 3 is a topology on 2, but it might also have unintended consequences.

We can’t just let everything be a set. We will get impossible-to-debug errors. We need more structure. Here is an analogy.

Programming in assembly language

When I was a kid, I had an Acorn Atom computer, which could be programmed in two languages. One of them was BASIC. Variables in basic could be strings or integers, for example. A string couldn’t be an integer — this made no sense. But I could not write good graphical computer games in BASIC because it was too slow. So I had to learn the second language which this machine understood, which was 6502 Assembly Language. The 6502 processor was an 8 bit processor. In 6502 assembly language you had three variables A, X and Y, each of which was a number between 0 and 255, and you also had the concept of a “memory location”. A memory location was a 4-character hexadecimal string which pointed to a portion of memory on a computer chip which contained, guess what, a number between 0 and 255. Everything was a number between 0 and 255. Some of those numbers corresponded to whether a certain line of 8 dots on the screen were black pixels or white pixels. Some corresponded to links to hardware — for example the bit corresponding to the position $2^2$ at memory location B002 was connected to the internal speaker, so by continually adding 4 to this memory location one could make the computer beep. But it was still possible to write code. When I wrote code, I had to decide that certain memory locations would represent coordinates of objects on the screen, other memory locations would represent the black and write pixel drawings which I would draw at these locations, other memory locations would represent the velocity of the objects I was drawing and so on. I would typically plan out on a piece of paper which type of object was being stored at each region of memory. It is possible to write code in this way, just like it is possible to write computer code which does mathematics in bare set theory. But we do not teach assembly language to first year computer science undergraduates because it is much easier to learn to use a language like Python or C++ where there is some kind of typing system, where you see a variable $x$ and you can ask “what are you, $x$ ?” and get a useful answer such as “I am a list of real numbers” or “I am an integer”, rather than “I am a number between 0 and 255, so I hope you are keeping track yourself of what I am supposed to represent”.

Fixing set theory

OK so this is easy to fix. Let’s make a typing system for our set theory programming language. Let us actually give up on the idea of letting a variable $M$ in our programming language represent a set. We will make it so that the only things we will allow as variables will be ordered pairs. If $M$ is a variable, then the set $M$ will be an ordered pair $(n,X)$ , where $X$ is the actual set we are talking about, and $n$ is a natural number. And then we will simply make a list:

0 : set
1 : group
2 : ring
3: field
4: metric space

and so on. The idea is that the natural number $n$ will tell us the “type” of the set $X$ . Now we can figure out if $M$ is a module or a metric space by looking at its type (the natural number). We will no longer have an issue with the “bare set” $X$ coincidentally being interpretable as two or more things, because each time we use it, it will come with its type attached. Problem solved! That’s true — but another problem has appeared.

Is a field a ring?

Every field is a ring. Every mathematician knows that. Except that in our new “typed” system, it is no longer literally true that a field is a ring. A field is a pair $(3,F)$ and a ring is a pair $(2,R)$ . So what we actually have now is an “invisible map”, which takes a field $(3,F)$ and spits out a ring $(2,F)$ . The functions can be more complicated than this in fact — every ring is a group under addition, but remember that a ring is something like an ordered sextuple or whatever, whereas a group is only an ordered quadruple, so the function sends $(2,(R,+,-,\times,0,1))$ to $(1,(R,+,-,0))$ — it is a slightly more complicated function than you might think. Every metric space “is” a topological space but when you think about it, this invisible function is actually quite involved, because you have to make the topology from the metric. Mathematicians ignore these functions, and furthermore it is absolutely fine to ignore these functions in practice, but if you are writing a formal proof verification system then you have to decide how to deal with this. You either make it untyped, in which case it really is true that every field is a ring, but some fields might also be topologies by accident and you run the risk of really-hard-to-debug errors later on — or you make it typed, in which case it is no longer true that every field literally is a ring, but there is an invisible function which sends fields to rings. Such a system needs to have some good system of invisible functions — or coercions, as they are called in computer science: “take this object of this type, and let’s just pretend it has that type instead, by applying this function without even mentioning it”.

Invisible functions

Lean, and indeed all the other interactive theorem provers I have ever used (i.e. Coq and Isabelle/HOL), use some kind of typing system, because they are all designed by computer programmers, and computer programmers for some reason have an aversion to designing systems where natural programs might end up with incredibly-hard-to-debug errors. The typing system is baked into the core of these systems, and invisible functions are everywhere. The natural numbers are defined in these systems. By adding additive inverses we get the integers; by adding multiplicative inverses of non-zero elements, we get the rationals. In Lean the reals are defined to be equivalence classes of Cauchy sequences of rationals. Now ask yourself this question. Is a natural number a real number? No it is not. How can we fix this? Well here is a proposal: we could make a new hybrid object which contains all real numbers which aren’t natural numbers, represented as Cauchy sequences, and then stuffs in the original natural numbers in, in place of the real numbers which are actually natural numbers. We now have to deal with the complaints from the number theorists who are working with the rational numbers and want to represent a real rational number as an equivalence class of pairs of integers rather than a Cauchy sequence, and complaints from the computer scientists who now have to write a really ugly hybrid addition function on those reals, of the form “just add Cauchy sequences in the usual way — oh — except if the answer happens to be a natural number, in which case do something else”, especially because there is no algorithm to answer the question “is this real number a natural number” in general (take some problem where you have some integral coming from physics or whatever, and the conjecture is that that the answer is 42, and this has been checked to 1000 decimal places, but nobody can prove it: such questions do exist).

OK so here is another proposal: we just define an invisible function which takes a natural number $n$ in and spits out the corresponding real number $n$ . And guess what, it works. This function is invisible to mathematicians but in Lean it is there.

“A subgroup of a group is itself a group”

We finally get to what motivated me to write this post, which was a Twitter exchange I had with Tim Gowers, Andrej Bauer and others in March, during which point Tim said “I still don’t really understand the problem. A typical book on group theory will point out that a subgroup of a group is itself a group”. There is no problem Tim — a subgroup of a group can certainly be thought of as a group, and certainly for a mathematician it will do no harm to do so. But it turns out that typing systems turn out to be (a) really powerful and (b) really useful, and one thing we learnt in Lean over the past two years is that it turns out that if $G$ is a group then it is worth letting subgroups of $G$ have their own type! Mathematicians and computer scientists are working together using Lean and other systems, and are trying to figure out the best typing system for mathematics, and it is an interesting question which is as far as I can see not particularly well understood, although we are getting there. Types in Lean are unsurprisingly indexed by strings of characters, not natural numbers. For example Group is a type, and subgroup G is a type. And there’s an invisible function from subgroup G to Group. And it doesn’t matter. But it is actually there. Hence, in Lean, it is strictly speaking not true that a subgroup of a group is a group. But it doesn’t matter.

Something to cheer us up

Independent of all that, my teenage daughter is stuck at home and is doing art. Here is some.

7 Responses to The invisible map

John Doe says:

April 30, 2020 at 12:32 pm

I think you didn’t stress it enough: type system is not just a convenience – it’s vital. In CS mistakes can be critical and shouldn’t be tolerated because lives and property depend on it. While mathematicians are used to tolerate mistakes in hope that it will eventually be fixed by someone else. It’s just happened that Lean can be used as an interactive theorem prover. It’s also true that it’s a software development system. Well, at least Lean 4 is intended as such.

LikeLike

- xenaproject says:
  
  April 30, 2020 at 1:15 pm
  
  In mathematics we use types but only implicitly. Mathematicians have a very high-level interface for talking about objects, which is essential: if we spent all our time fretting about pernickety little issues such as invisible maps, we would never get anywhere. One reason I am so interested in getting undergraduates to use Lean is that I want to see where they say “but this is obvious, why is the system complaining?” and then try to understand whether the issue is that the “obvious” issue is *not* obvious, or whether the interface for mathematics which we are building is not yet perfect.
  
  But under the hood, where not all mathematicians want to go, I am now coming to believe that a type system is vital.
  
  LikeLike
  
  - John Doe says:
    
    April 30, 2020 at 2:42 pm
    
    You say: “if we spent all our time fretting about pernickety little issues such as invisible maps, we would never get anywhere.” But didn’t you play a Devil’s advocate here? That argument was probably valid for Euler or Gauss, but Leibniz already would not agree with it. “Calculemus!”
    
    LikeLike
galoisrepresentations says:

April 30, 2020 at 5:51 pm

Clicked on the link because of the art. It is good!

LikeLike

JC says:

May 3, 2020 at 4:11 pm

You mentioned “one thing we learnt in Lean over the past two years is that it turns out that if G is a group then it is worth letting subgroups of G have their own type!”

May I ask what is the reason behind that?

LikeLike

- xenaproject says:
  
  May 3, 2020 at 4:54 pm
  
  This is not really mathematics, this is all to do with foundational matters and what turns out to work best in practice in the specific system you’re working with. The answer is that Lean has a powerful “dot notation”, meaning that if A has type B, and there’s a theorem called B.blah, then instead of writing B.blah(A) to apply it to A, you can just write A.blah. If B is the word `subgroup` then this is quite convenient, because if A is a subgroup it might well be called something like A, so A.blah is a lot briefer than subgroup.blah A. This was one of the key reasons for making subgroups a type. The other was that we were trying to use type class inference to check that subsets were subgroups, and Lean 3’s type class inference was not quite designed to do this and the results were not perfect.
  
  We are currently in the process of replacing the typeclass `is_subgroup` with the new type `subgroup G`.
  
  LikeLike
  
Tom Leinster says:

May 13, 2020 at 11:34 am

Very nice post; thanks! And the artwork reeled me in too.

The place you arrive at is pretty much the place that category theorists call home. For example, consider the thing about groups vs subgroups. In any category, one defines the “subobjects” of an object X to be the isomorphism classes of monomorphisms into X. (Here two monos i: Y –> X, i’: Y’ –> X are said to be “isomorphic” if there’s an isomorphism between Y and Y’ making the obvious triangle commute.) In categories such as Set and Group, the monomorphisms are the injections, and two monos into X are isomorphic iff they have the same image. So subobjects in Set are subsets, and subobjects in Group are subgroups.

From the categorical viewpoint, the difference between subsets and sets, or between subgroups and groups, becomes quite striking. For instance, one can always talk about the intersection of two subsets of a given set (or subgroups of a given group), but in ordinary mathematical practice – “generic” mathematics – forming the intersection of two abstract sets is not really an operation that makes sense. And the “invisible map” that takes a subset of X and realizes it as a set is something categorically more or less standard: it’s the composite of forgetful functors Mono(X) –> Set/X –> Set, where Mono(X) is the category of monomorphisms into X and Set/X is the category of all maps into X (a “slice category”), both with commutative triangles as their maps. And similarly for groups and subgroups.

Actually, there’s an example demonstrating the power of invisible maps that you might like. Here it is. Every open subset of a topological space X can be realized as a topological space in its own right, and that space comes equipped with a continuous map into X. If we write Open(X) for the poset of all open subsets of X, then this gives us a functor

Open(X) –> Top/X,

where again Top/X is a slice category (objects are continuous maps into X, maps are commutative triangles). The nice thing is this: applying some completely standard and general categorical constructions gives first a pair of adjoint functors between the category of presheaves on X and the category Top/X of spaces over X, and then the equivalence of categories between *sheaves* on X and étale bundles over X. Zero creative input is needed here! Granted some generic category theory, your original “invisible map” automatically generates the notions of sheaf and étale map, plus the equivalence between them, and for that matter the sheafification construction. (Details here: https://golem.ph.utexas.edu/category/2010/02/sheaves_do_not_belong_to_algeb.html)

LikeLike