## Numbers vs Sets

November 7th, 2008 by ThorstenTo simplify: Mathematics has to do with numbers, while Computer Science is more concerned with types (let’s call them sets). On the level of the natural numbers there is a nice equivalence identfying a finite set with the number of its elements. The operations of addition and multiplication on numbers correspond to coproduct (or disjoint union) and (cartesian) product of sets. Indeed we even use the same symbols and . Exponentiation corresponds to function space , indeed category theoreticians use the exponential notation for the latter.

But then the ways part and the schism begins. For the Mathematicians the natural numbers are only half of the story (indeed a **semi**ring) and they hasten to add the negative numbers. If we want to keep exponentiation, we can’t stop at the integers, we get the rational numbers , algebraic reals and even algebraic complex numbers . The intuitive completion of these constructions are the complex numbers.

Negative sets don’t really make sense, we are more interested in infinite sets. E.g. we would like to have a fixpoint of successor: . Combining this with exponentiation leeds to larger sets like or ordinal notations

. This time the intuitive completion are sets.

But the story may have a happy ending. Once we start to analyze operations on those spaces, a new analogy seems to emerge. E.g. differentiation is well known as an operation on complex functions, but as Conor McBride observed it also makes sense as an operation on functors, i.e. operations on sets. Not on all functors, but then differentiation doesn’t work on all functions either. The analogy carries further, and indeed we can use a variation of Taylor’s theorem to analyze datatypes. Hence, here we seem to have a new union, the glimpse of a generalized calculus applicable to operations in numbers and sets.

One of the areas where this analogy has been exploited is the theory of species, where ideas from calculus are exploited to prove theorems about the combinatorics of structures. To me much of the literature seems to be written from the perspective of Mathematicians who know numbers and try to use them to analyze sets. I’d prefer to do it the other way around, start with sets and see whether we can steal ideas from conventional calculus.

This is basically the introduction to a more technical talk about *generalized species* which I will post separately.

November 10th, 2008 at 3:02 pm

No. Mathematice has to to with sets (let’s call them sets), while Computer Science is more concerned with types (let’s call them types).

November 10th, 2008 at 11:33 pm

Thank you for your deep insights…

November 19th, 2008 at 3:20 pm

Ok, what is the difference between sets and types? I am not sure. In classical set theory, the elements already exists before we sort them into sets (even if they are sets again), while in Type Theory an element can only be constructed once you know its type. However, types in programming are often treated similar: first there is the program then there is the type. Moreover, in Type Theory small types are often called sets (e.g. in Coq).

Hence I think that the terms sets and types have no clearly identifiable meanings and overlapping interpretations. I treat them basically as synonyms.

Thorsten

November 21st, 2008 at 5:26 pm

In set theory, there is a distinction between sets (which are the values of bound variables), and classes (for example the epsilon relation itself) given by abstraction

expressions {x | P(x) }, where P(x) is a formula with x free.

Set theorists are reasonably well-behaved about observing this terminological distinction, and it causes little problem.

“Type theory” is by comparision a terminological pig-sty. To my mind,

we should use the word “set” for an object of type Set, and “type” like

the set-theorists use “class”. We should use words like “small”, “large”,

“hyper-large” and so on to distinguish sets that have names in universes

inside Set. But even I don’t: it depends on who I am speaking to. There

are things that just fall off the tongue, like “W-type” that are just beyond

repair.

A number of people have struggled (a bit desperately) to find some terminology

that fits both what people actually say, and reality. There has been

“type/category” for “set/type” (in the Bibliopolis book), and I think

“type/kind” by Luo. And the “set/type” distinction has been more or less

scotched by the rise of constructive set theory, taking over the “S”-word

for something like its use in conventional set-theory.

We are all doomed. DOOMED!

Hank

December 4th, 2008 at 11:24 pm

Well, I shouldn’t be commenting just because I am annoyed, without anything interesting to say.

The first reason I was annoyed was the idea that “mathematics has to do with numbers”. You can look at the comments to this blog post to understand why.

The second reason was the suggestion to call the types “sets”. (Zermelo-Fraenkel) Set theory and type theory are two alternative (I would say competing) foundations for mathematics. They resolve the Russel paradox differently. They have different axioms and are just different. Types and sets should not be confused. I prefer set theory as a foundation for mathematics, but of course this is a matter of taste.

December 15th, 2008 at 5:22 pm

These are interesting comments! Sorry, but I got annoyed too because I couldn’t figure out what you wanted to say.

Re your first comment: Modern Mathematics is very much influenced by the success of calculus since Newton and only very little by ideas from Computer Science. That’s why I used the, admittedly, provocative phrase “Mathematics is about numbers”.

Re your 2nd. Obviously you have a point: we can use the type/set terminology to indicate the difference between a predicative hierarchy (ala Russell) and the restriction of comprehension (ala Zermelo). However, in Type Theory many people use the term Set to refer to small types, e.g. Coq uses the term Set to refer to Type(0) – the first universe.

Why do you prefer set theory? If you are interested in functional programming this seems slightly incoherent too me.

December 23rd, 2008 at 1:11 am

That was true in nineteenth century, much less so in twentieth and now. If we are talking about stuff everybody learns in school, then I think the essence of mathematics is much better represented by geometry than calculus.

Of course the choice of foundation is mostly subjective, so I can’t make a good rational argument that set theory is better that type theory for expressing mathematics. This is a matter of training and habit. For most mathematicians it is more natural to express mathematics in set theory because this is how they have been trained (indoctrinated?).

I am a fan of strong typing in programming languages. It is really a cheaper substitute for formal verification – it allows to assert certain properties of software you are writing and then those assertions are checked by the compiler. In this context we can say that types “protect you from writing nonsense” or “keep your story straight”. But in the context of (formalized) mathematics, where you have the real thing (every assertion has a proof), types don’t serve any purpose and only get in the way. See Harisson’s paper on Euclidean spaces for an example of hoops one has to jump to express a very simple concept of $latex R^n$ if the type system is not good enough, the issue about which he says “Of course, no problem arises in systems based on traditional set theory (such as Mizar)”.