[Axiom-developer] Axiom-Combinat / non-extending category

[Martin Rubey]

Dear Ralf, *

I now merged the modified signatures as outlined below with the axiom-port. The
result is quite promising.

I can use generatingSeries of all constructors, including Plus and Times.

I cannot use structures, of course, since this uses a dependent type now:

structures: (L: LabelType, List L) -> Generator %

The generator is not a problem, there is an easy workaround. However, the
dependent type is a show stopper, I'm afraid.

I'm willing to pay 200$ from my own pocket if somebody makes Axiom understand
signatures like that.

Furthermore, I tried to define a domain

)abb dom TEST Test
A: CombinatorialSpecies == Plus(CharacteristicSpecies(1), 
CharacteristicSpecies(1))


in various forms, but all I get is the error message

non extending category

Well, I guess that's not so interesting anyway. We can use the aldor compiler,
after all.


I rather like the new signature.


Martin


Martin Rubey <address@hidden> writes:

> A short report:
> 
> I modified species.as.nw, replacing CombinatorialSpecies L by
> CombinatorialSpecies, adding the LabelType in the representation of
> CharacteristicSpecies.
> 
> (I didn't bother to modify the other basic species yet)
> 
> The operation elements$LabelType is not needed in this approach, and in fact, 
> I
> wouldn't know how to implement it.
> 
> Extending Set is not possible, for reasons discussed recently on this list. We
> would need to create a new domain SetSpecies.
> 
> Plus and Times stay nearly the same, only the signature changes to
> 
> Plus(F: CombinatorialSpecies,G: CombinatorialSpecies): CombinatorialSpecies
> 
> and F L has to be replaced by F everywhere, structures(List L) changes to
> structures(L: LabelType, List L), etc.
> 
> Note that the Rep of Plus, Times, etc. won't change.
> 
> Things seem to work. I'll have a look whether Axiom likes this version better.
> 
> 
> 
> Martin