[om] CD questions on the occasion of permu1
george at ags.uni-sb.de
Wed Oct 16 16:03:48 CEST 2002
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
> > 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 ?
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...
More information about the Om