Ralf Hemmecke <[EMAIL PROTECTED]> writes:
> 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,
(I believe you wanted to write: nothing)
> Martin wants dependent types working properly.
Yes, but that's not the only point here. In fact, dependent types as above are
supported in Axiom. Ooops, sorry there is a typo, it should read:
SPECIES ==> (L: LabelType) -> CombinatorialSpecies L;
To make Axiom understand the snippet above, I need that a domain constructor is
regarded as a function. "Plus" will take two such functions and return another
one.
> > 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 ....
That's only half of the story, namely where you regard the collection of all
species. But of course, the species of permutations is a useful domain, too:
on the one hand, I want to be able to work with objects that are permutations,
on the other hand, I want to work with the species of permutations as an
object. In our project, we reach this goal. In fact, we do have a proof of
concept implementation of SpeciesRing, where the objects are then the various
species, i.e., Rep is CombinatorialSpecies(L).
> > Note: IIUC currently you essentially have one type for labels. To support
> > nontrivial label types one can add argument to SpeciesRingCategory.
The problem is that it does not work to fix a label type. For example, the Rep
of (partitional) composition is
Rep == Record(
tag: Partition L,
left: F SetSpecies L,
right: SetSpecies G L);
(F and G are the given species.) Thus, we consider the species F, but with
labels beings sets! It's even worse for functorial compostion:
Rep == F G L;
> > 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?
All of that. If you are not concerned about speed, you can define the domain
Permutation as Compose(SetSpecies, Cycle).
structures set [a,b,c,d]
will then give the 24 permutations. And it is not difficult to (aldor-)extend
this domain to include all the usual operations on permutations you want, like
composition, inversion, etc.
Martin
-------------------------------------------------------------------------
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
