[om] CD questions on the occasion of permu1
Michael Kohlhase
Michael_Kohlhase at asuka.mt.cs.cmu.edu
Wed Oct 16 14:27:23 CEST 2002
Arjeh,
> Here are ten questions regarding the newly conceived CD permu1.ocd for
> permutations. The CD can be found at
> http://www.win.tue.nl/~amc/oz/om/cds/permu1.html
BTW, the links to the STS signatures do not work there.
> I would greatly appreciate comments.
>
>
> 1. The CD may be too large. Ideas how to chop it up into smaller ones?
> For instance, cycle is more general than permutations. It could
> just as well be used for graph construction, so perhaps it should
> go elsewhere (where?)
> Also, order and cycle_type might be considered less basic than the
> others and so could well go into a permu2.
I do not think that this too large, it is for instance much smaller than
transc1. It only defines 8 symbols, I think that up to 20 should be no
problem.
> 2. The name: There is a CD called permut1 by Andrew Solomon, so a I
> chose a variation. It could be abbreviated to perm1 or elongated to
> permut1 (if Andrew and James agree), permutat1, or permutation1 (not sure
> though that such long names are allowed).
I think that long names (unabbreviated are better, since they can otherwise
get quite cryptic). "permutation1" would be my preference. I have looked in
the standard, and I could not find a restriction (there was the intuition
once that the file name should be the same as the cd name, but that should
not be a problem still).1
> 4. A symbol can stand either for a `real' function (like sin) or a
> constructor (like `rational'). At any rate, in the encodings you
> can often preform surgery and find the arguments back. But not on
> the abstract OpenMath level. So my question is: what is our general
> approach to finding arguments of contructors? In the example of
> `rational(123,456)', would you like numerator and denominator to be
> around so that the children (123 and 456) of the expression can be
> accessed? the vector_selector is an example (in a case where the
> number of compnents may very...). We find the i-th argument of an
> OM list by applying the list to <OMI>i</OMI> using an <OMA>...
I think that the constructors for "structures" should be treated in a
uniform way in OpenMath -- if to be simpler for humans to use. That was the
reason I proposed the addition of a record constructor in OpenMath. What I
would do now (it was the only thing that caught flak in Pisa) is use a
content dictionary for structures, and use that in the for the
constructors. OOOOh, I just realize that this does not really apply here.
> 6. Regarding FMP's: there are many one could write. What are the
> practical guidelines here? James has written some guidelines. These
> are (roughly): have CMP correspond with FMP and don't put in too
> many. The current version of permu1.ocd is large because of
> examples, FMP's etc., not because of the number of symbols it
> defines.
I beg to disagree, the FMPs are part of the fun, since they go a long way
to make the meaning and the usage of the symbols declared in the CD
clear. How can they do any harm in a world of 20 Gb minimum hard drives
even in laptops.
> 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?
If you were to do this in OMDoc, then you could make the setup of the whole
theory a little more structured: you would define three theories
1) permutations as mappings "pam"
Definition: A permutation is a certain bijection of a set X
2) permutations as sets of cycles "psc"
Definition: a permutation is a certain set of cycles
is_perm witnesses this property
3) permutations as lists of integers "pil"
Definition: a permutation is a list of integers
then you would construct theory morphisms; something like
tm1: pam --> psc, YOU ARE MISSING A COERSION FUNCTION HERE; the inverse
of permutation
tm2: psc --> pam, P |--> permuation(P)
im: pil --> pam, L |--> permutation(elements(L))
to show that these are theory morphisms, you would have to show that
a) P is a psc-permutation, iff permutation(P) is a pam-permutation
b) for any list of integer permuataion(elements(L)) is a pam-permutation
tm1 and tm2 show that the theories pam and psc are equivalent, im shows
that pil is a specialization of both. An added feature of this way of doing
things would be that the FMPs and CMPs can be transported between the
theories.
Michael
--
om at openmath.org - general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems
More information about the Om
mailing list