[om] CD questions on the occasion of permu1

[Michael Kohlhase]

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