Waldek Hebisch <[EMAIL PROTECTED]> writes:
> > > AFAICS at practical level you do not need sets: only number of elements
> > > matter (plus ability to "lift" permutations). Numbers and permutations
> > > live in ordinary world, so why you go to type level?
> >
> > Hm, I think that's exactly what we do: permutations are elements of the
> > domain Permutation. This domain in turn is a species. I do not think that
> > you believe that, but just to make sure: we do not consider a single
> > permutation as a domain.
>
> We are talking about different things here. IIUC species are functors from
> finite sets to finite sets.
Yes.
> In particular they should act on morphims of category of finite sets. In
> practice, isomorphism classes of finite sets are determined by cardinality (a
> single number).
Yes.
> To take into account isomorphims minimally one needs to look at images of
> permutations of a single set. So permutations that I am talking about are at
> least formally are quite different than the elements of domain Permutation --
> they are morphims of the category of finite sets
... with bijections. Let's call this category B.
> I wonder if Aldor combinat handles this aspect...
I have not yet *really* thought this through, but as far as I currently can
see, we do not consider the morphisms of B (i.e., relabellings of structures)
at all, right now. In principle, we want to, because for some operations on
species, most importantly functorial composition, we know of no algorithm to
generate the isomorphism classes of the structures, except the "stupid brute
force approach": generate all structures and throw away those that arise from a
relabelling. (If I recall correctly, one can do a little better, but not
much).
I do want to keep in mind that we might want to consider also actions on the
set of labels other than relabelling. But I must admit that I do not *really*
understand yet how to reconcile species and more general finite group actions,
as considered by Adalbert Kerber and his group.
> > So, what do we gain by introducing the set of Dyck paths, or any other
> > species, as a separate domain instead of simply considering species as
> > elements of a single domain -- which we do additionally?
[...]
> > That is, you can give your grammar at the top level. In the other
> > approach, you would have to give the grammar to a wrapper function, which
> > then generates the objects:
> >
> > BinTree := grammar(B=X+B*B)
> >
> > and you would then have methods to generate them, find the generating
> > functions etc.:
> >
> > structures([1,2,3,4], BinTree)
> > generatingSeries(BinTree)
> >
> > But this doesn't integrate nicely with permutations, lists or sets, where
> > natural Aldor/Axiom domains exist.
>
> What is wrong with something like:
>
> SpeciesDomain(s : Species): SpeciesDomainCategory ==...
Hm, what would be Species and what would be SpeciesDomainCategory? What would
SpeciesDomain yield, eg., what's the result of SpeciesDomain BinaryTree
Integer?
> [...] my point of view is that we have three formal systems:
> Aldor with "fixed" types,
> full Aldor and
> Aldor types.
> By "fixed" types I mean that all types should (at least in principle) be
> determined at compile time. Aldor with "fixed" types is just a small subset
> of full Aldor. In other words, we have "identity" embedding form Aldor with
> "fixed" types to full Aldor.
>
> Full Aldor looks much more powerful, because you can do at runtime
> computations with types. But if you work only with types you are in the
> third formal system: Aldor types.
> Again Aldor types are just a small subset of full Aldor. My impression is
> that Aldor types give you rather weak programming language (quite a lot of
> things which work on elements do not work on types). This language is
> different (not isomorphic to) than Aldor with "fixed" types, but I think that
> it should be rather straightforward to express equivalent computation at
> element level
That looks like a very good insight.
> -- basically the only feature that types have and normal elements do not have
> is lazy evaluation. But it is known (and used in Axiom/FriCAS) that if you
> stick to apropriate protocol you can easily emulate lazy evaluation.
> Put it differently: power of types come from interactions with elements. So
> I was expecting something like "see, we compute this type, declare element
> and get such and such behaviour -- you can not do this with elements alone".
OK, but that's what we do. Well, nearly: that's what we make possible, so far
we only provided the backbone. Here is some (slightly simplified) code (from
the iso-experiment branch, but it would work with all branches, except that
"struct$Plus: % -> Record(left, right) and right$Times, left$Times is needed):
ACBinaryTree(L: LabelType): CombinatorialSpecies L with {
height: % -> Integer;
} == Plus(SingletonSpecies, Times(ACBinaryTree, ACBinaryTree))(L) add {
Rep == Plus(SingletonSpecies, Times(ACBinaryTree, ACBinaryTree))(L);
height(x: %): Integer == {
import from Integer;
X := struct rep x;
-- if X is a Singleton, the height is zero
X case left => 0;
-- otherwise, we have to compare the height of the left and the right branch
1 + max(height left X.right, height right X.right);
}
};
Maybe this comes closer to being a justification of our approach. I guess you
can still do this if BinaryTree would be an element of a domain
"CombinatorialSpecies". In this case, you'd have
CombinatorialSpecies:
decomposableObject: Grammar -> %
structures: % -> List Object
But the type "Object" is not trivial to specify. In fact, we did do this, and
Object becomes a type very similar to the type described in the aldor user
guide, or, if you prefer, "Any" in Axiom. You can then implement "height" as a
function that takes an element of Object. We didn't like that so much.
Please keep asking, your questions are very good!
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
