"Linked List" puzzle

Question

Suppose $E$ is a topos, and consider the operations $0,1,+,\times$ (denoting the initial and terminal objects, the coproduct, and the product), and recall that $E$ satisfies the usual arithmetic laws, such as the distributive law.

For the unfamiliar, one should think of objects in $E$ as sets, but of course they don't have to be. An "element" of a "set" $A$ means a map $B\rightarrow A$ for some object $B$. If $B=1$, we say the element $1\rightarrow A$ is a unit element of $A$, and you can think of these instead if you prefer, but note that the "generalized" elements $B\rightarrow A$ of an object $A$ completely define $A$, whereas the unit ones don't.

Suppose $A$ is an object of the topos $E$. A "linked list of type A" is a new object $L$ of the topos in which an element is either the word "null" (meaning empty list) or a pair $(a,l)$ where $a$ is an element of $A$ and $l$ is an element of $L$. Equationally:

(*) L=1+AxL.

By this point, you should understand these things. Ok, now I'm going to tell you the weird puzzle. Suppose we want to "solve" for $L$, so that we can see what it really is. To do this, I'm going to cheat. In a topos, there is no such thing as subtraction nor division.

$$L=1+A\times L$$ $$L-(A\times L)=1$$ $$L\times(1-A)=1$$ $$L=1/(1-A)$$ $$L=1 + A + A^2 + A^3 + \cdots$$

So a linked list of type $A$ is "either the empty list, or an element of $A$, or an ordered pair of elements of $A$, or a triple in $A$, etc."

This faulty computation has led to the correct answer. Once this answer is found, one can check topos-theoretically that it is correct (although note that toposes aren't guaranteed to have infinite coproducts). My question is:

Q: where is this computation actually taking place?

Clearly, as the topos of finite sets is the background for the usual arithmetic of natural numbers, it stands to reason that one would generalize toposes as natural numbers were generalized to rational ones. Has or can this be done? Can this calculation make sense in some appropriate context?

Answer 1

The theory of species is the full answer to your question -- but in this specific case all that is needed are some very basic properties of polynomial functors.

Let's focus on you fixed-point equation $L=1+A \times L$, and observe that by unrolling it you can generate your infinite sequence $L = 1 + A + (A \times A) + \ldots$, without using subtraction or division.

Now, you mentioned you were working with objects, and so what you want to do is find the object which is the fixed point of the endo-functor $F(X) = 1 + A \times X$. IIRC, Arbib and Manes proved back in the 1970s that in any topos, any polynomial functor (of one variable) will have a least fixed point (that is, the category of $F$-algebras will have an initial algebra). (Morally this is because trees can be encoded with natural numbers.)

Species only start coming into their own when you start considering non-free combinatorial constructions. E.g., think about what the "generating functor" for unordered sequences should be -- I won't say because it will spoil the surprise.

Answer 2

One can get the same series in a subtraction- and division-free way by iterating the first equation, $L = 1+AL = 1 + A + AAL = 1 + A + AA + AAL = \dots$. This derivation may "live" in a more modest environment than one allowing division or subtraction as bona fide operations.

Answer 3

There is a short and very nice article on something related: "Objects of Categories as Complex Numbers" by Marcelo Fiore and Tom Leinster

The authors give a criterion when polynomial equations in a rig (=ring without negatives, like the rig of iso classes of objects in a topos), that you got by calculating as if you were in a ring, are actually valid (Thm 5.1 there). This applies to the first three lines of your calculation. I wonder if one could somehow extend their approach to "rings with infinite sums", to cover the remaining steps...

Answer 4

I agree that Joyal's species are sort of key here, although the kinds of data types being considered here are not exactly the same thing.

My guess is that 1/(1-A) should be seen as a kind of "generating function" for the formal power series 1 + A + A² + A³ ... and that the relevance of power series can be explained by some simplicial structure hiding somewhere. It's certainly true that one can take derivatives and integrals of these data types: see Conor McBride, The Derivative of a Regular Type is its Type of One-Hole Contexts.

There is a direct interpretation of division which comes up when computing "Taylor series" of these datatypes: e.g. the type Aⁿ/n! is the n-element multiset, since Aⁿ is an n-tuple and n! can be read as the action of the permutation group. Unfortunately, the formalism does not quite work out: see http://www.cs.nott.ac.uk/~ctm/Dissect.pdf for a reference. This may be related to Baez and Dolan's work on groupoid cardinality (arxiv: math.QA/0004133).