[sc34wg3] Tau: The role in operator

[Lars Marius Garshol]

When going through the Tau model at the RM workshop today we found one
strange thing that we couldn't quite account for.

The role in operator is defined as

  a upm r = ...

but it seems very strange that

  - the a is given in the operator, since the operator really operates
    on the m to produce 'a's, rather than the other way around, and

  - the text says "Given a map m, a name r, AN IDENTIFIER P, we define
    ..." yet the "a upm r" doesn't have any p in it.

We discussed this at the RM workshop when Ann presented the model and
agreed that there are two possible interpretations:

  1) m up r = {a | a element-of m ^ exists p | <r, p> element-of a}
  
  2) m up <r, p> = {a | a element-of m ^ <r, p> element-of a}


Did we miss something, or is there a problem with the notation here?
Also, which of the two interpretations is the intended one?

I thought Robert meant 2), Ann that Robert meant 1), and I now agree
with Ann. Whether Robert does is a different question, of course. :)

-- 
Lars Marius Garshol, Ontopian         <URL: http://www.ontopia.net >
GSM: +47 98 21 55 50                  <URL: http://www.garshol.priv.no >