8.11 Product of Species

Definition 8.10. [BLL98, chp. 1.3] Let F and G be two species of structures. The species F ⋅ G (also denoted FG), called the product of F and G, is defined as

(37)

where the sum is taken over all pairs (U₁,U₂) for which U = U₁ ∪ U₂ and U₁ ∩ U₂ = ∅.

The transport along a bijection σ : U → V is carried out by setting, for each (F ⋅ G)-structure s = (f,g) on U,

(38)

where σ_i = U_i is the restriction of σ on U_i, i = 1,2.

Definition 8.11. The cardinality species N is the species of structures defined by

(39)

for any finite set U and

(40)

for any bijection σ : U → V and n = cardU = cardV an N-structure on U.

Proof. Define the mapping ν : E → N for any finite set U by

(41)

Then for any bijection σ : U → V between two finite sets U and V of cardinality n it holds

(42)

and

(43)

Furthermore, ν has an inverse given by

(44)

Therefore ν is a natural isomorphism from E to N. __

There exists exactly one structure for every input set U, so N(x) = E(x) = e^x. Clearly, N ⋅ N has an exponential generating series e^2x. Look at (37) to understand that the sum symbol must be interpreted as a disjoint union.

Let us for a while assume the above sum in (37) is an ordinary (non-disjoint) union. Then

(N ⋅ N)[]	= N[∅] × N[] ∪ N[] × N[∅]
	∪ N[] × N[] ∪ N[] × N[] ∪ N[] × N[]
	∪ N[] × N[] ∪ N[] × N[] ∪ N[] × N[]
	= ×∪×
	∪×∪×∪×
	∪×∪×∪×
	=

This has some consequence for the representation of the product of species. We must explicitly make the pairs disjoint by tagging them. According to (37) we tag the parts by the pair (U₁,U₂) which is given through the Subset species.

The tag tells something about the split of the input set s of the function structures.

We have to create the objects generatingSeries, isomorphismTypeGeneratingSeries and expression first, before we start initialization. For example, the following variant would lead to a runtime error when a species is defined recursively:

The reason is that Aldor would—due to the first set! instruction in the second line above—descend to the initialization of F(L) and G(L) before initializing isomorphismTypeGeneratingSeries.

Thus, we need to call init after defining all recursively generated constants, but before using them.

The same situation occurs in the Plus constructor.

For the product of species we need to generate all decompositions of a set U into subsets U₁ and U₂ such that U₁ ∪ U₂ = U and U₁ ∩ U₂ = U. Thus we can simply iterate over all structures of the species of subsets.

Exchanging F and G in the input of Times does, of course, not yields identical structures, i. e.Times is not commutative.

In order to avoid infinite recursion for recursively defined structures, we first check whether the coefficient of the generating series that corresponds to the input list u or v is zero. If it is, there is no need to recurse any further, since no structures must be generated. Note that it is not sufficient to test whether the coefficient of the generating series corresponding to the input list s is zero: infinite recursion may result, if, for example, the coefficient corresponding to v vanishes, but not the coefficient corresponding to u.

The domain ExponentialGeneratingSeries is implemented in such a way that a series knows approximately about its order, thus, accessing the coefficient of the series, will not lead to infinite recursion though the species and the generating series are defined by the same equations.

The isomorphismTypes in the product species are generated in a manner very similar to the generation of the structures. In fact, we simply replace structures by isomorphismTypes for all occurrences.