Backtracking

From the SETL Wiki

Backtracking is an advanced feature of SETL that facilitates logic progremming.

The two primitives essential for employing backtracking are ok and fail. The functions of these primitives can be viewed in two ways:

1. True non-determinism
   • A fail statement is unreachable. The interpreter will pre-emptively choose a path of execution that avoids it.
   • ok is also pre-emptive. It returns true if possible, unless this would cause a fail statement to be reached sometime in the future, in which case ok returns false instead.
2. Trial-and-error (the actual implementation)
   • ok splits the current process in two, a bit like fork, except that the two subprocesses are executed sequentially instead of in parallel. Like fork, ok returns a different value in each subprocess, but its return value is a boolean value rather than a process ID.
   • fail asserts that the most recent decision for ok to return true was incorrect, terminates the current process, and transfers control to the sibling process in which ok had returned false instead. Control then resumes from the statement following ok as if it had returned false.

[edit] A simple example: Eulerian path

Suppose we want to write a program to find a Eulerian path through the following graph:

Now imagine we don't know the algorithm to find a solution, but we know how to verify that one is correct. We might come up with a program like this:

program euler;

const edges := unstr '{{a b} {a c} {b c} {b d} {c e} {d e}}';
const nodes := +/ edges;

var path := [];
var traversed := {};

print(edges, nodes);
path := [pickNode(nodes)];
(while traversed /= edges)
  current := path(#path);
  neighbours := nodeNeighbours(current);
  next := pickNode(neighbours);
  traversed with:= {current, next};
  path with:= next;
end;

print("Valid path found:", path);

proc nodeNeighbours(node);
  return {} +/ {edge in (edges - traversed) |
                node in edge} less node;
end proc;

So far we haven't figured out a way choose the next node in the path, so for now let's just prompt the user for it:

proc pickNode(selection);
  if #selection > 0 then
    loop
    doing
      print("Choose one of", selection, ":");
      flush(stdout);
      get(choice);
    until
      result in selection
    do
      result := choice;
    end;
    print("Thanks!");
    return result;
  else
    print("Reached a dead end!");
    stop;
  end if;
end proc;

end program;

This will work if the user is present and willing to do the work for us! Imagine they enter:

b
a
c
e
d
b
c

the program will correctly identify this as a valid path, but if the user tries an invalid path such as:

a
b
c
a

the program will stop them there and inform them that they have reached a dead end (ABCA cannot be the prefix of any valid path.)

So now we know how to verify a path, we can convert this to a brute-force method for finding one:

proc pickNode(selection);
  if exists choice in selection | ok then
    return choice;
  else
    fail;
  end if;
end proc;

We are now telling the computer

1. that it must guess the following node at each step
2. how to identify when it has guessed wrong

The first thing to note about the new version of pickNode is that if given an empty selection set, the exists check will fail, because there is no element in selection to test (and the ok is never evaluated.) Since the test fails, the second branch of the if statement is taken and fail is executed, indicating that a previous guess was incorrect.

Now let's step through the program to see how it works:

1. nodes is initialised to {a b c d e}, path to [] and traversed to {}.
2. First we call pickNode to select a starting point from among all five nodes.
3. Within pickNode, the exists quantifier iterates through the set of nodes in arbitrary order. Suppose it picks 'a' first.
4. The first call to ok (after duplicating and saving the program state) returns true. The quantifier is now satisfied, 'a' is assigned to choice, and pickNode returns this node.
5. Now, we know that no valid Eulerian path starts at A. We can temporarily ignore how pickNode is implemented, because there is no way to choose a sequence of nodes such that the main loop will terminate. pickNode will be called a few more times, but the effort is futile.
6. Inevitably we will reach a dead end and pickNode will be called again with an empty selection set. Now the second branch is taken, which leads to the fail statement.
7. This causes the interpreter to revert to the previously-saved state, where the exists quantifier was iterating through the nodes in the graph, and was about to apply the ok predicate to 'a'.
8. We are now in the second subprocess, in which ok returns false. The guard condition now fails for 'a' rather than succeeding as in the previous attempt.
9. As the forall quantifier has not yet found a node that satisfied the predicate, it tries another. Suppose it picks 'b' this time.
10. ok is called again. As this is a "fresh" test, it again splits the current process in two, and in the first process it returns true. pickNode now returns 'b' in this new subprocess.
11. path is now set to ['b'] and the main loop is entered once more to build a path.
12. This time, pickNode will succeed on every call, because there is no way to reach a dead end in this graph as long as either B or C is chosen as the starting node, hence the fail statement will not be executed again. Eventually the program will print the valid path and terminate.

The situation is slightly more complicated with this graph:

because as well as picking a suitable starting node (C or D) the choice of the second node is also significant. If we start by traversing the edge CD then we will eventually hit a dead end at D. This will again trigger the fail statement and backtrack to the point where D was chosen as the successor of C. Either A or E will be chosen instead in the second subprocess, resulting in a valid path being found.

[edit] Notes

There are two other primitives associated with backtracking: lev and succeed. These are less commonly used.

To date only CIMS SETL has implemented backtracking.
GNU SETL recognises the keywords ok, fail, back, lev and succeed but will raise a run-time error if any of them are encountered during execution.