Extension of operators to sets

Most of the operators extend to sets, in a way which is consistent with the interpretation of sets as independent nondeterministic choices. Generally, a unary operator f obeys the law

        f{x,y} = {f(x),f(y)}

Thus, for example,

        -(2..3) = (-2..-3)

and

        ~{0,1} = {1,0}

For a binary operator *, we have

        {x,y} * z = {x * z, y * z}
        x * {y,z} = {x * y, x * z}

For example,

        3 + {4,5} = {7,8}

and

        0 & {0,1} = 0
        1 & {0,1} = {0,1}

(which are actually special cases of the laws given above for ``and'').

This behavior of sets is somewhat counterintuitive when the equality operator is applied to sets. For example, the result of

        {a,b} = {a,b}

is not equal to 1 (true). The way to understand this is to think of each set as representing an arbitrary choice among its elements. Thus, the result of the above expression is the set $\{0,1\}$, since we may choose equal elements or we may choose unequal elements.

The exception to the above rule is the ``in'' operator, which compares a value and a set of values. In this case, only the left represents a nondeterministic choice. That is:

        {x,y} in z = {x in z, y in z}

However, as stated previously,

        x in {y,z}   =   (x in y) | (x in z)

[N.B. This makes ``in'' the only operator in the language which is not monotonic with respect to set containment. The ``in'' operator is only monotonic in its left argument. A formal verification system that relies on monotonicity (such as ternary symbolic simulation) should allow only constant sets on the right hand side of ``in''.]