Session 4   Nondeterminism and Sets

1  Nondeterminism

1.1  Why Nondeterminism?

Our algorithms for computing the maximum element of the tuple inp examine the elements in order, starting with inp[1].  However, that's not necessary; the elements can be examined in any order.  If you're designing an algorithm just for use in one program, examining them in a particular order is fine.  But there may be other programs in which it would be better to examine them in some other order.  If you're writing the algorithm for others to use, it's best to allow it to examine the elements in any order.  Of course, this is silly for our simple example; but it could be an issue for a subtle, complicated algorithm.  So, you should know how to do it.

1.2  The with Statement

An algorithm that allows multiple executions is said to be nondeterministic.  We've already introduced nondeterminism into algorithm TupleMax by allowing it to start with inp having any of a set of initial values.  We now add nondeterminism in the rest of the execution.  This is done in PlusCal with the with statement.  For any identifier id that does not already have a meaning and any set-valued expression S, the statement

with (id \in S) { body }

To examine the elements of inp in a fixed order, we used a while statement with an integer-valued loop variable i to examine inp[i].  To examine the elements in an arbitrary order, we use a while statement with the set-valued loop variable I to examine inp[i] for an arbitrarily chosen element i of I.  Here is an outline of the two ways of examining the tuple's elements:

      fixed order                         arbitrary order
variables ... i = 1 ;               variables ... I = 1..Len(inp)
  ...                                 ...
  while (i =< Len(inp)) {             while (I /= {}) {
    examine inp{i] ;                    with (i \in I) {       
    i := i + 1                            examine inp{i] ;
  }                                       I := I \ {i}   
                                        }
                                      }

The complete algorithm TupleMaxND that examines the elements in an arbitrary order is in specification Session4, which is among the ones you downloaded.  Open that specification and examine the code.  The translation is included, as is a model you can run to test the algorithm.  For all nondeterministic algorithms, TLC checks all possible executions.

Exercise 1   Write an algorithm SillyTupleMax by modifying TupleMax to work in the following silly way.  It repeatedly examines an arbitrary element of the tuple inp and terminates with max equal to that value if it is the maximum value of all the tuple's elements.  Thus, if it's lucky, it can terminate after trying a single element.  If it's very, very unlucky, it can keep picking non-maximal elements and never terminate.  Show the answer.

--algorithm SillyTupleMax {
   variables inp \in Tuples, max = minValue, I = 1..Len(inp), b = (I /= {}) ;    
   { while (b) {
       with (i \in I) {
         if (\A j \in I : inp[i] >= inp[j]) {
            max := inp[i] ;
            b := FALSE
          }
       }
     } ;
     assert IF inp = << >> THEN max = minValue
                           ELSE /\ \E n \in 1..Len(inp) : max = inp[n]
                                /\ \A n \in 1..Len(inp) : max >= inp[n]
   }
}

It is possible for algorithm SillyTupleMax never to terminate.  For example, for any input tuple not all of whose element are the same, it is possible for the with statement to keep choosing some i for which inp[i] is not maximal.  Why the possibility of nontermination doesn't cause TLC to report an error is explained in the next session.

In either TupleMaxND or your algorithm SillyTupleMax, change the with (i \in I) to with (i \in {}) and run the translator.  What do you think the algorithm now does?  Run TLC and find out.

TLC should have reported the error: Deadlock reached.  The with statement is supposed to execute its body with i equal to an element of the empty set, which is impossible because there is no such element.  So, execution must stop.  Why is this deadlock?

2  More About Sets

2.1  Specifying a Subset

If S is a set and exp is a Boolean-valued expression, then

{x \in S : exp}

{n \in Int : n % 2 = 0}

{n \in Int : IsPrime(n)}    and    {n \in Nat : IsPrime(n)}

2.2  Building a Set

If S is a set and exp is any expression, then

{exp : x \in S}

Let's compare these two ways of defining the set of even integers:

EvenInt1  ==  {n \in Int : n % 2 = 0}     
EvenInt2  ==  {2 * n  : n \in Int}

The building construct has an abbreviation involving multiple bound variables similar to that of the quantifiers \A and \E.  For example,

{<<i, j, k>> : i, j \in Int, k \in Nat}

{ { {<<i, j, k>> : i \in Int} : j \in Int } : k \in Nat }

Exercise 3   Write the set of all pairs <<p, q>> of integers such that p is less than q.  Show the answer.

2.3  Sets of Sets

SUBSET

{ {}, {1}, {2}, {3}, {1,2}, {1,3}, {2,3}, {1,2,3} }

Mathematicians call SUBSET S the powerset of S; they write it P(S) or sometimes 2S—the latter notation because if S is a finite set with n elements, then SUBSET S has 2n elements.  Note that for any sets S and T, the these two expressions are equal:

S \subseteq T     and     S \in SUBSET T

UNION

UNION {S1, S2, ... , S99}   and   S1 \cup S2 \cup  ... \cup S99

• Any set S equals UNION (SUBSET S).
• Any set S of sets is a subset of (possibly equal to) SUBSET (UNION S)

Exercise 4   Use UNION to write the set of all tuples of length at most 21 whose elements are "a", "b", or "c".  Show the answer.

Puzzle 1   Define Intersect so that for any set S of sets, Intersect(S) is the intersection of the sets in S—that is, the set of all elements that are in all the elements of S.  Show the answer.

Intersect(S)  ==  {v \in ... : \A r \in S : v \in r}

Puzzle 2   What does this set equal: {(x \in S) : x \in S}?  Show the answer.

2.4  The Cartesian Product

{<<s, t>> : s \in S, t \in T}

Exercise 5   What is this set: (S \X T) \X U ?  Show the answer.