Production rules for search (and lex ordering)

01 Mar 2017

This is a silly game, but anyway.

Set up:

We assume you have a graph (nodes and edges) explicitly on a piece of paper (printed out or something), and it's small enough that you can comprehend it visually, and you don't mind marking it up.

You will need blank index cards and a writing implement.

Decide on locations for four spots for index cards: the blank ones, the "TODO" stack, the "FOCUS" stack, and the "DONE" stack.

Create an index card for the starting node, put it in the FOCUS stack, and cross off the starting node in the graph.

Rules of play:

  1. If both the FOCUS spot is empty and the TODO spot is empty, then you're done!
  2. If the FOCUS spot is empty, but the TODO spot is not, move the top card from the TODO stack into the FOCUS spot.
  3. If the FOCUS spot is non-empty, and the corresponding node in the graph has a neighbor that has not been crossed off, create a new card for that neighbor, put it on the top of the TODO stack, and cross off the neighbor on the graph.
  4. If the FOCUS spot is non-empty, and every neighbor of the corresponding node in the graph is crossed off, put the card in the FOCUS spot into DONE.

Lex ordering

Why does this game terminate? Let's try to use Lex ordering to prove it.

Lex ordering is dictionary ordering, generalized to tuples of numbers. For example, in lex ordering (a, b, c) is bigger than another tuple (d, e, f) if a is bigger than d in the usual way, or if a is equal to d and b is bigger than e. If a equals d and b equals e then we fall back to comparing c to f.

Let's use this 4-tuple: (unmarked non-neighbors, unmarked neighbors, number of items in TODO, number of items in FOCUS)

When we focus using rule 2, then we change the set of neighbors. In principle, switching focus could increase the number of unmarked non-neighbors, if we had some unmarked neighbors before the switch. However, because we always mark all of the neighbors before switching focus, Rule 2 never increases the number of unmarked non-neighbors, and sometimes unmarked non-neighbors become unmarked neighbors, decreasing the number of unmarked non-neighbors.

Also, when we focus using rule 2, we decrease the number of items in TODO. We increase the number of items in FOCUS, but we don't mind that.

When we mark a neighbor with rule 3, we decrease the number of unmarked neighbors (and increase the number of items in TODO, but we don't mind that), but we never increase the number of unmarked non-neighbors.

When we unfocus using rule 4, we decrease the number of items in FOCUS, and we don't increase any other quality.

So in every case, we go downward in lex ordering.

Note: I am not certain that this argument is ironclad.