[om] CD questions on the occasion of permu1

[George Goguadze]

Small note regarding composition of permutations:

 I think defining a separate symbol for this makes sence.  (At least I did it
when translating chapter6 of IDA to OMDoc)
As you see, depending on the interpretation one might want to use here 'times'
from 'arith1' or
 'left_compose' from 'fns1'. But theory of permutations should possess its own
multiplication symbol that is an instance of both - 'times' from 'arith1' - that
is the multiplicative operator
on a semi-group and 'left_compose' from 'fns1' since it is indeed just the
composition of functions.
This is exactly the meaning of this particular operation - that it can be both of
them - and this fact can be represented in OMDoc by providing appropriate
morphisms of corresponding theories.



Michael Kohlhase wrote:

> > 7. Regarding the composition of permutations vs the operator *: I have
> >    avoided (so far) from using the symbol times from arith1. The
> >    reason is that times might stand for either left or right compose.
> >    For power there is no problem (there is an FMP in arith1 relating
> >    it to times and whichever times we choose, the anwer is the
> >    same). So we could use it. Nevertheless, so far I didn't.  I might
> >    get into trouble when I use Group(perm1,perm2,...,permN) as
> >    suggested in the CD group1.html, where it says "The n-ary function
> >    Group. The group generated by its arguments.  The arguments must
> >    have a natural group operation associated with them."  Left-compose
> >    is less natural than right_compose, some say....  I probably should
> >    avoid this symbol to avoid ambiguity.  (In other words, I think
> >    that Group in CD group1 lacks an indication of the multiplication;
> >    I suggest that it be added as a first argument.)  Is there a better
> >    solution?
> >
> >    BTW, note that power(x,n) is something like <OMA><OMS cd="????"
> >    name="apply"/> <OMS cd="arith1" name="times"/>....< which makes it clear
> >    that power is implicitly related to times.
>
> I think that we want to use specific symbols for composition of
> permutations, even if they are PRESENTED the same as times, and if
> permutations with concatenations are a semigroup. If we wanted to stress
> this, it would be better to add this as a FMP or CMP.
>
> > 8. Since right_compose is defined only for two arguments, I
> >    need the construct "apply" to describe multiplication of more than
> >    one permutation (in order to avoid long expressions with many
> >    occurrences of right_compose, that is).
> >    Question: can't we allow left_compose and right_compose two have
> >    at least two arguments (instead of exactly two)?
>
> I do not see any problem in defining n-ary composition; indeed it would be
> quite convenient (and justified since binary composition is
> associative). You only need to say what the meaning is, and maybe define a
> notion of currying, i.e. (a*b)*c = a*(b*c) = a*b*c
> you could even define unary composition *(a)=a and *()=empty
> permutation,...
>



>
> > 10. Is there anything else that strikes you as odd, remarkable,... in
> > permu1.ocd?

Some more small questions :

What about defining a sign (signum) of a permutation?
or the fixed points of a permutation fix(g) ...
Do we need the names for S_n (symmetric group) and A_n (alternating group) here
or should  they be introduced into the setname2 (why not) ?  Or are these symbols
somehow redundant ?

Regards,
George

--
George Goguadze                   | Im. Stadwald 36.1, 66123,
Faculty of Computer Science       | Saarbruecken
University of Saarland            | tel/fax: +49681302 5322/5076
http://www.activemath.org/~george | email:george at activemath.org


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://openmath.org/pipermail/om/attachments/20021016/84b774c0/attachment.htm