"@@" and ":>"

[drrtal...@gmail.com]

Hi,

I'm working through the TLA+ Hyperbook and in the section on function, 15.2, the operators "@@" and ":>" are used. What are these operators called (i.e., their spoken names, if you will)?

The ":>" operator is a mapping operator, mapping a single value from one set into a single value in another value.

The effect of the "@@" operator combines the domains of two functions and yields the value that corresponds an element of that union, but favoring the first of the two functions whenever both have that element in their respective domains.

Thanks,

Roger Alexander.

[Leslie Lamport]

I believe that the operator :> is written |-> in Z and probably B, and Knuth called that symbol \mapsto.  So "maps-to" seems like a good name for :> .   (Of course, it's also a good name for the  |->  in record expressions.)  If  DOMAIN f  is a subset of  DOMAIN g , then  f @@ g  could reasonably be called  "f overriding g" , while if the domains are disjoint, @@  could be read as "union".  This suggests the name "overriding union" for  @@ , but I'd just call it "at-at".

Leslie