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

[Gabriel Dos Reis]

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)."  I'm not familiar
with the theory of species.  At any rate I did not intend "least" in
terms of numerical coefficient.

| > The interesting bit about those inductive definition is that they come
| > with "fold" (reduce in Axiom-speak) for free.
| 
| Hmmm, lazyness is important here. Unfortunately the internal
| definition of formal power series in AC does not allow to write
| equation (+) as such. One first has to say (something like)
| 
| g: FormalPowerSeries Integer := new();
| set!(g, 1+x*g*g);
| 
| where x corresponds to the inteterminate of "FormalPowerSeries Integer".

Aha! Good point.  Now, I just need you to point me to a good
introductory point on species.

-- Gaby