8.1 Combinatorial Species and their Modelling in Aldor

According to [BLL98], a definition of combinatorial species is as follows.

Definition 8.1. A combinatorial species is a rule F that assigns to each finite set U a finite set F[U] and to each bijection σ : U V of finite sets a function F[σ] : F[U] F[V ]. Additionally, for all bijections σ : U V and τ : V W the relation F[τ σ] = F[τ] F[σ] should hold. If IdU denotes the identity map on U then we have F[IdU] = IdF[U].

Speaking in terms of category theory, a combinatorial species is nothing but an endofunctor F : B B from the category B of finite sets and bijections to itself.

In Aldor we could try to design the category of finite sets and bijections, but thinking in terms of mathematical sets removes information about the elements of a set. In Aldor it is more natural to speak of a set whose element belong to a certain type. So we can speak of a set of Integer or a set of String, but it is hard in Aldor to simply speak of sets without specifying the element type.

So we tend to implement combinatorial species over sets of a certain type similar to the type constructor Set or List.

Since for a combinatorial species mostly the number of elements in the underlying set is of importance, but not the true nature of that elements, it would probably have been possible to always use mappings from Set(Integer) to Set(Integer) to represent a combinatorial species, but in view of operations on species that are defined later, it seemed more appropriate to just pass a parameter to the definition of a combinatorial species. For lack of a better name, we call that parameter L and require that it satisfies the category LabelType. Our understanding is that L is a pool to take the labels from that can be used to label structures.

We are not trying to correctly model the mathematical category B of finite sets in Aldor, since that is currently not our main concern.

Let us give a similarity of our design to some constructions in the Aldor library. In the Aldor library there exists a type constructor Set which tries to model finite sets. However, Set is defined as

Set(L: PrimitiveType): with { ... } == add { ... }

So, in fact, we have several set types, namely one for each choice of L. In Aldor it seems quite natural to provide the type of the elements of a set.

There is the species E of sets, defined by E[U] = {U}, see [BLL98, p. 8]. For each finite set U, there is a unique E structure, namely the set U itself. We intend to extend the Set constructor to become a combinatorial species by (informally speaking) defining for each type L (see above) a functor EL (which corresponds to Set(L)) and restrict the set U to a set of elements of type L.2 In our interpretation of the theory, the type L can be considered as the type of labels which are attached to the structure.

A general combinatorial species can be seen in a similar way. Instead of having a functor

F : B → B
(1)
which assigns to any set U a set F[U], we impose more structure and provide a way to build
FL : BL → BF(L)
(2)
depending on a type L. In the above notation

If, for simplicity, we think of L as being a set, then

ToDo 12
rhx 7 14-Aug-2006: I should actually define F(L) rigorously, but I am not so sure about (2). Basically, FL and F(L) are quite connected, but not really the same. F(L) is that what we are going to define to be Aldor implementations of combinatorial species (something like Set(L)), and FL is represented below by the function structures from F(L).

That should be made more precise!

Maybe we should say that structures is the part of FL that operates on the objects of BL. However, for that to be precise, we need to turn BL into a category.

A short account on combinatorial species can also be found at http://en.wikipedia.org/wiki/Combinatorial_species and in [Ker91].