[om] Re: questions regarding a permutation CD

[Andrew Solomon]

hi Arjeh,

> 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).

The only symbol defined by permut1 is "permutation" which has the same
semantics as your "permlist". I think it's bad to have more than one
CD applicable to permutations. I suggest:
* change your "permlist" to "permutation"
* change your "permutation" to "permcyc" 
* Then you can just say "permu1" subsumes "permut1" and 
"permut1" is deprecated!

As to the name itself, I'm not too worried.

> 3. The definition of a permutation has been set up so that there is a
>    unique data structure for each permutation if you regard the
>    arguments of permutation as a single set. This is convenient and
>    aligns with proof planning of Volker Sorge and Martin Pollet. I have made a
>    shortcut though by letting permutation(list of cycles) take over
>    the role of the abstract data structure "set(sequence of cycles)".
>    In other words, I did not want to top set(sequence of cycles) off by
>    writing permutation(set(sequence of cycles)). Is this OK?

A) I think this is dodgy:-)  

>    (is_perm helps in the present approach!)
>    BTW likewise, PermList (with the same meaning as in GAP) is not
>    applied to an OM list, but just has the list entries for argument.

B) I think this is fine but the name should just be "perm" or something.

I got tripped up on first reading, and didn't notice that the cycles were 
disjoint and thought order was important.

I believe that 

<omobj> 
  <oma>
   f
   a1
   a2
  ...
   an
  </oma>
</omobj> 

can only be used when f is an n-ary function symbol. In case (A) 
"permutation" can only be unary, whereas "perm", like the "list" operator
itself, is just a function symbol with a variable number of arguments.
"permlist" on the other hand, should take a list.

In general, I think we need to be strict about the semantics of
the OpenMath language rather than define it in CDs.

> 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>...

Here's an off-the-wall idea similar to Michael's: why not give
the arguments of function symbols names when we're defining them - something
like second-class symbols in a CD. If you don't define them, they
default to arg1 ... argn.  Then we could assert eq(arg1(f(a,b)), a)
but if we had given the arguments names, then we could say
eq(numerator(rational(a,b)),a)

> 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'm not sure I understand all this. Leftness or rightness of composition
is actually defined by leftness of rightness of the action. You appear to have
(implicitly) defined the action to be a left action in "permlist", 
so a*b can mean nothing but do b then do a.

Perhaps I'm misunderstanding?

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

In the final example of permlist

> eq (permlist ( 5 ,  1 ,  3 ,  2 ,  4 ) ,  4 ) 2

there is something fishy. It appears to be an omobj consisting of
a boolean 
  -- eq (permlist ( 5 ,  1 ,  3 ,  2 ,  4 ) ,  4 ) 
  // a comparison of the permutation with 4
and an integer 
  -- 2

I think what you wanted was a further application of the permutation to 4:

eq (permlist ( 5 ,  1 ,  3 ,  2 ,  4 )( 4 ),  2)

again, perhaps I missing something?



cheers

Andrew
--
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