[om] permutation1 CD

[Arjeh Cohen]

                              Eindhoven, October 21, 2002.

Thank you Andrew S., George G., Mike D., and Michael K., for answers
to my 10 questions re the permutation CD.

A new version of the CD permu1.ocd for
permutations can be found at
         http://www.win.tue.nl/~amc/oz/om/cds/permutation1.html 
(or extension ocd for the source).
I would still appreciate receiving comments.

Here is an overview of the discussion, including some responses of
mine to the issues raised.

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.

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

RESPONSE: 
OK. Stimulated by this answer, I added two more symbols: sign
(suggested by George) and are_distinct, which ought to be in a more
general CD in future, I suppose.

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

MICHAEL:
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

MIKE:
I agree that long names are better.  The idea that the filename should
be the CD name does however suggest that it shouldn't be more than 8
characters to support ISO9660 (CD) file systems etc.  On the other hand
this seems a pretty archaic restriction tehse days.

RESPONSE: I have changed the name to permutation1.

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

MY RESPONSE: agreed that we should get to one CD. I object to
the suggested specific change of names for two reasons:
  1) By choosing cycles as the building block for a permutation,
  the permutants can be different from natural numbers. We need not and
  we should not inherit a limitation of Magma and GAP.
  2) I would like to stay close to formal introductions of
  permutations, like the one in the make by Volker Sorge and Martin
  Pollet, where a permutation is a set of cycles.

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?

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


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

RESPONSE: Point taken. I have changed "permlist" into "perm".
By the way using apply_to_list(perm,[a_1,...,a_n]) you get the same as
perm(a_1,...,a_n).

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

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



ANDREW:
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)

RESPONSE: shouldn't arg1(f(a,b)) be arg(1,f(a,b))??
Otherwise: yes...who will produce a proposal?
Or even a CD for such a purpose?

MIKE:
I'm not sure that the semantics of `numerator' is that it returns the
first argument of the constructor `rational' (not least because you can
say "numerator(r)".  At the moment we haven't tried explicitly to
standardise names but have inherited `selector' from MathML (giving 
`vector_selector', `matrix_selector', `list_selector'). 

RESPONSE: 
The symbol "rational" in "nums1" does not require that its
arguments are in normal form. So rational(4,6), rational(-4,-6) and
rational(2,3) are all admissible and all represent 2/3.  So you will
have to specify whether you mean denominator(rational(4,6)) to be 2 or
4. In the latter case, it is just arg(1, rational(4,6)), in the former
it is more of a function.

On a different note, we may want the symbol quotien to generalize
 rational.
Thus quotient(a,b) represents the equivalence class
of (a,b) under (a,b) ~ (c,d) iff ad = bc.

5. Magma and Gap do not work with permutations of arbitrary objects
   (to the best of my knowledge), so I would not know how to implement
   the most general notion of permutation (as in the CD) there. But
   for positive integers as entries (read: permuted elements), there
   should be no problem with any of the symbols.




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 permutation1.ocd is large because of
   examples, FMP's etc., not because of the number of symbols it
   defines.

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

Mike:
I think the thought was that FMPs should be clearly understandable
(hence the associated CMP) and have a didactic purpose.  Saving space
wasn't the reason.
 
Michael:
> 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.

Mike:
I agree.  We don't have any concept of inheritance in OpenMath.

RESPONSE: I haven't formulated the FMP's of some CMP's. With enough
operators like arg and/or apply_to_list this is certainly possible.

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.
 
Andrew:
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?

RESPONSE: I don't think so: (1,2,3) acts on 1, 2 and 3 by sending 1 to
2, 2 to 3 and 4 to 1, regardless of compositions.  But (1,2) o (1,2,3)
= (2,3) with o = left_compose and (1,3) with o = right_compose. I
think the best way out is for your general (and quite useful) Group
construct in group1.html to require that the first argument be the
multiplication. The I can use it in the permgrp CD I want to write
soon.

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)?
   
Michael:
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,... 

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

RESPONSE: I will (left or right) compose a letter to James with a
request for some changes in the existing CDs. This n-arity might be
one of the requests.

9. (Mainly for David Carlise:) How can I create .omcd files (with the
   four letter extension). How can they be useful?

DAVID: (quoting from the top of my head:) it is automatically
manufactured when you submit to the NAG site.

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

MICHAEL: 
BTW, the links to the STS signatures do not work there.

RESPONSE:
This requires extra work by hand. I have no use for the STS right now,
so I did not do the work. On the other hand, the GAP codec translates
the notion defined nicely into GAP constructs.

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


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

RESPONSE: I made a mistake, thanks for pointing it out.


GEORGE:
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 ?

RESPONSE: 
Fix(g) is a problem in that we do not specify the domain. In fact
the world minus support (g) is equal to Fix(g).

Sign(g) can be defined by help of cycle_type. I added it as a symbol
and mentioned the cycle_type definition as an FMP.

A_n S_n etc. I can put into a future CD for permutation groups.


=========================================================================================









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