Any finitely terminating non-deterministic algorithm can be made deterministic by using depth-first search on the tree of possible executions.
Or, to explain it another way: each time you have a non-deterministic choice, fork the program into multiple copies, one per possible choice. Forking might be done by calling the operating system's
fork() call (very expensive), or by capturing all the relevant state of the variables and storing it in a set of pending items to explore (potentially tedious to write the code), or by replacing the
choice() with a recursive call that makes a copy of all of the relevant state (
S') and iteratively tries each of the possible choices (easiest to implement in this case).
Here is an example of how to implement the latter transformation. The state at the
choice statement is the value of
i. So, we do the following:
search(S', i, u):
if u in S'
S' = S' + u # this needs to copy the set, not update it destructively
i = i + 1
for_each u in S'
for u in [1,2,..,n]
search(S', i, u)
for u in [1,2,..,n]:
search(emptyset, 1, u)
search contains all of the code after the
choice statement, until the next
choice statement. We had to rip the for-loop over i apart to make this work, but the transformation was fairly mechanical.
This is a general method that can be used on any terminating non-deterministic algorithm -- not just this one.