Ralf Hemmecke <[EMAIL PROTECTED]> 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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer