[fricas-devel] Re: desired semantics

[Ralf Hemmecke]

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.)

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/

[Martin Rubey]

Post by Ralf Hemmecke

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)

Post by Ralf Hemmecke
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.

Post by Ralf Hemmecke

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).

Post by Ralf Hemmecke

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;

Post by Ralf Hemmecke

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/