[Axiom-developer] Re: FW: data structure vs. mathematical structure

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

| On 11/16/2006 01:20 AM, Gabriel Dos Reis wrote:
| > Ralf Hemmecke <address@hidden> writes:
| > | > The definition you gave is it: least fixed point of
| > | >     X |-> 1 + T × X × X
| > | | Hmmm, good question. In Aldor-combinat (AC) we deal with
| > combinatorial
| > | species. They encode actual structures. The corresponding generating
| > | series G(x) for binary trees given by your X above has to fulfil the
| > | equation
| > | | G(x) = 1 + x * G(x) * G(x)                                (+)
| > | | As a quadratic formula it has at most 2 solutions. And only one
| > of
| > | those solution is a power series with only non-negative
| > | coefficients. Since I don't know what it should mean to say "there are
| > | -5 trees with 3 nodes", it is clear which solution I choose for the
| > | generating series.
| > | | Assuming that I understand a bit of the theory of species, then
| > there
| > | is only *one* solution to
| > | |       X = 1 + T * X * X.
| > | | We are not yet dealing with "virtual species" which would allow
| > | negative coefficients in the generating series.
| > I realize my sentence could be ambiguous:  I meant "least fixed point
| > in the category of continuous partial orders (CPO)."
| 
| Well, it seems you have to be even more precise. I still cannot
| understand that. You mean X, 1, T are continuous partial orders?
| And what does then + and × stand for?

First consider CPO, the category of complete partial partial orders,
where the morphisms are continuous functions.  Here 

  * 1 denotes "the" least object 

  * + is the discriminated union
  
  * × is the Cartesian product


Both "+" and "×" are (bi)functors of CPO.  More generally any
"polynomial" expression is a functor in CPO.  For example, if T is a
fixed object of CPO, 

    X +-> 1 + T × X, where X ranges over CPO

is a functor, so is

    X +-> a + T × X × X

There is a general theorem that says that any polynomial (endo)functor F of
CPO has a least fixed point.  Notice that, in reality, this fixed
point is understood as "F(X) is isomorphic to X", but one usually writes 
F(X) = X.  The set of finite lists of element of type T can be thought
of as the least fixed point of 

    X +-> 1 + T × X

Similarly, the set of finite binary trees can be thought of as the
least fixed point of 

    X +-> 1 + T × X × X

The categorial viewpoint explains very neatly the generalization of
the reduce operator (over lists) to more general inductive types.

| > Aha! Good point.  Now, I just need you to point me to a good
| > introductory point on species.
| 
| The short one you find at
| 
| http://en.wikipedia.org/wiki/Combinatorial_species


Thanks!  It looks like we are actually using the same terminology
(except that I was not doing any natural number interpretation).

| and the book I currently like best is given as the second reference on
| the above page:
| 
| François Bergeron, Gilbert Labelle, Pierre Leroux, Théorie des espèces
| et combinatoire des structures arborescentes, LaCIM, Montréal
| (1994). English version: Combinatorial Species and Tree-like
| Structures, Cambridge University Press (1998).

Thanks!

-- Gaby