[sc34wg3] Tau: The role in operator

Robert Barta sc34wg3@isotopicmaps.org
Sun, 1 Aug 2004 21:33:11 +1000

On Sat, Jul 31, 2004 at 07:00:04PM -0400, Lars Marius Garshol wrote:
> 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 = ...
> 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?

Lars (et.al),

This is clearly a typo. It should read

  p -> r = {a element-of m | exists p : <r, p> element-of a}

It basically delivers ALL assertions in the map where p is a player of
the role r.