On Wednesday, November 15, 2006 7:39 PM Ralf Hemmecke wrote: > > On 11/16/2006 01:20 AM, Gabriel Dos Reis wrote: > > | > 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) (+) > > ... > > | 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? >
It is indeed a remarkable achievement of the level of abstraction that these formulas are (nearly) identical but refer to seemingly very different things! >From a categorical perspective, the + and × above stand for abstract direct sum and direct product like the disjoint union and cartesian product of intuitive set theory. Or you can read the same equation like a production rule in a grammar (universal algebra) and then + denotes an altenative construction and × denotes a pair (or triple as in the case above). The X denotes a "production". And the general abstract solution is represented by a particular structure preserving operation called a functor which in the example above can be thought of as mapping types into more complex type structures - lists and binary trees - this is also called a "functor" or type constructor in Axiom and Aldor. >From the point of view of combinatorics (counting structures) these operations behave just like the usual arithmetic ones, so we also have the interpretation to which you referred as the solution of a numerical quadratic equation. The reference to complete partial orders is a way to define an ordering or "size" of the solutions of the equation so that it makes sense to speak of the (unique) "least" or "greatest" solution. http://en.wikipedia.org/wiki/Complete_partial_order (Depending on the application the adjective "continuous" might also be applicable.) There are other ways to achieve effectively the same thing in category theory via universal constructions such as limits and co-limits. The most important thing is to be able to define abstractly the essential characteristics of the + and × operations. >From my point of view, the best way to understand least fixed points is to also try to understand greatest fixed points at the same time. As I mentioned in a previous message the Stream type in Axiom (and some other languages) is related to the same defining equation as the List functor X = 1 + T * X except that it is greatest fixed point solution rather than the least fixed point. It is seems easy (trivial?) to understand the action of the List type constructor but it is a little more challenging to understand the Stream constructor. Playing with Stream in Axiom makes this a little easier. In particular Streams are possibly infinite types corresponding to possibily repeating sequences of things of a given Type. For example expand(1..) is the sequence of PositiveIntegers. And repeating [1,2,3] is a sequence of those three Integers repeated 1,2,3,1,2,3,... indefinitely. In Axiom such infinite repeating sequences have a convenient finite representation as a circular list (denoted by a bar over the list of repeated elements). Now having thought about Stream as a type constructor solution of the equation X = 1 + T * X, I would like to ask you what you think might be the equivalent greatest fixed point solution of X = 1 + T * X * X Recall first that the least fixed point solution corresponds to the BinaryTree type constructor. I think I know the answer although I have not seen this written anyware else, so I want to see if you come to the same conclusion. :-) Ultimately it is the connection to Azcel and Jon Barwise's notions of non-wellfounded sets that intrigues me most. Please forgive me for going on about this ... Regards, Bill Page. _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer