On 05/16/2008 11:30 PM, Waldek Hebisch wrote: > Martin Rubey wrote: >> Note that one of the most fundamental reasons why the species (AKA >> combinat) project doesn't work well with panAxiom / SPAD, is that >> functions are treated specially in panAxiom / SPAD. >> >> If you can come up with a SPAD-compatible replacement for the >> construct >> >> SPECIES == (L: LabelType) -> CombinatorialSpecies L; >> Plus( >> F: SPECIES, >> G: SPECIES >> )(L: LabelType): CombinatorialSpecies(L) == add [...] >> [...] >> >> you shall be praised and I'll stop talking about language semantics >> from now on and refer to you instead.
> Martin, you keep posting this code, but this snippet is meaningless > without telling what your goals are. Of course, just that little part tells nearly anything, but I guess, Martin wants dependent types working properly. (Sorry, I don't know SPAD so well.) > If the goal is to implement species theory I would probably start: > > SemiRing():Category == .... > > SpeciesRingCategory():Category == SemiRing with -- add extra > operations like composition and differential .... You are semi-right. This issue is perhaps not appropriate for this thread. It is a design decision to construct species as domains (or rather domain constructing functors). The reason was that we wanted to be able to write something like L = 1 + X*L (as an Aldor expression) and have support from the compiler to produce the right code. Of course, we can later consider the collection of our so constructed species domains and take them as elements of a semi-ring. We are not that far and therefore did not implement the semiring structure yet. But that is on the todo list. > Note: IIUC currently you essentially have one type for labels. To > support nontrivial label types one can add argument to > SpeciesRingCategory. > To put it differently: the snippet alone look obscure to me. > Apparently you (Ralf and Martin) are trying to translate categorical > definition directly to Aldor code. Nearly. > But categorical definition at least formally operates on classes, so > is directly uncomputable. Choosing representation you throw out some > aspects. It is not clear which aspects you retain. I hope we can continue the discussion on the aldor-combinat-devel list. The relevant section is at http://www.risc.uni-linz.ac.at/people/hemmecke/AldorCombinat/combinatsu14.html#x27-320008.1 and you certainly see that this is not yet really formal. Species theory works on sets. But neither in Aldor nor in SPAD I will ever have sets. What I can have are sets with elements of a particular type. (OK, one could box up every type as something of type Object, but that would mostly throw away all the typing beauty of Aldor.) And if you speak about "classes" ... do you meant classes in the sense of set theory? We don't really need that since, if F is a species then the most important questions are, what are the structures with labels {a_1, ..., a_n}? The input is a finite set and the output as well. > Also, it would help if you say what combinat can do. Looking at code > I see that it can compute generating functions. It seems that you > also have code to enumerate corresponding sets, but it is not clear > what is the result: if I have species of permutations can I compose > resulting permutations? Indeed, we are very weak in the documentation. But from the exports of CombinatorialSpecies http://www.risc.uni-linz.ac.at/people/hemmecke/AldorCombinat/combinatsu16.html#noweb.NWf7R7q-1eUam8-1 you can see that for a particular species, we can compute various kinds of generatingSeries and we can generate all labelled and all unlabelled structures of a given size. Now the point is, that the number of basic species is rather small. The main advantage is that one can easily build up more complicated species from the basic species by certain semi-ring and other operations. That even includes definitions of species by mutual recursive equations. Look for example at http://www.risc.uni-linz.ac.at/people/hemmecke/AldorCombinat/combinatsu69.html#x103-15000024.11 and more specifically at "testRecursive2()". The interesting part is that we did not have to write any program that resolves that recursion (as for example MuPAD-Combinat does). The Aldor compiler does the work for us. Did this help a bit? Ralf ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ Aldor-combinat-devel mailing list Aldor-combinat-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/aldor-combinat-devel
