TUTORIAL1-TOWERS-OF-HANOI

The Towers of Hanoi Example 
Major Section:  TUTORIAL-EXAMPLES

This example was written almost entirely by Bill Young of Computational Logic, Inc.

We will tackle the famous ``Towers of Hanoi'' problem. This problem is illustrated by the following picture. 

  

          |        |        |
          |        |        |
         ---       |        |
        -----      |        |
       -------     |        |
          
          A        B        C
We have three pegs -- a, b, and c -- and n disks of different sizes. The disks are all initially on peg a. The goal is to move all disks to peg c while observing the following two rules.

1. Only one disk may be moved at a time, and it must start and finish the move as the topmost disk on some peg;

2. A disk can never be placed on top of a smaller disk.

Let's consider some simple instances of this problem. If n = 1, i.e., only one disk is to be moved, simply move it from a to c. If n = 2, i.e., two disks are to be moved, the following sequence of moves suffices: move from a to b, move from a to c, move from b to c.

In general, this problem has a straightforward recursive solution. Suppose that we desire to move n disks from a to c, using b as the intermediate peg. For the basis, we saw above that we can always move a single disk from a to c. Now if we have n disks and assume that we can solve the problem for n-1 disks, we can move n disks as follows. First, move n-1 disks from a to b using c as the intermediate peg; move the single disk from a to c; then move n-1 disks from b to c using a as the intermediate peg.

In ACL2, we can write a function that will return the sequence of moves. One such function is as follows. Notice that we have two base cases. If (zp n) then n is not a positive integer; we treat that case as if n were 0 and return an empty list of moves. If n is 1, then we return a list containing the single appropriate move. Otherwise, we return the list containing exactly the moves dictated by our recursive analysis above. 



  (defun move (a b)
    (list 'move a 'to b))


  (defun hanoi (a b c n)
    (if (zp n)
        nil
      (if (equal n 1)
          (list (move a c))
        (append (hanoi a c b (1- n))
                (cons (move a c)
                      (hanoi b a c (1- n)))))))
Notice that we give hanoi four arguments: the three pegs, and the number of disks to move. It is necessary to supply the pegs because, in recursive calls, the roles of the pegs differ. In any execution of the algorithm, a given peg will sometimes be the source of a move, sometimes the destination, and sometimes the intermediate peg.

After submitting these functions to ACL2, we can execute the hanoi function on various specific arguments. For example: 



  ACL2 !>(hanoi 'a 'b 'c 1)
  ((MOVE A TO C))


  ACL2 !>(hanoi 'a 'b 'c 2)
  ((MOVE A TO B)
   (MOVE A TO C)
   (MOVE B TO C))


  ACL2 !>(hanoi 'a 'b 'c 3)
  ((MOVE A TO C)
   (MOVE A TO B)
   (MOVE C TO B)
   (MOVE A TO C)
   (MOVE B TO A)
   (MOVE B TO C)
   (MOVE A TO C))
From the algorithm it is clear that if it takes m moves to transfer n disks, it will take (m + 1 + m) = 2m + 1 moves for n+1 disks. From some simple calculations, we see that we need the following number of moves in specific cases: 


   Disks   0   1   2   3   4   5   6   7  ...
   Moves   0   1   3   7  15  31  63  127 ...
The pattern is fairly clear. To move n disks requires (2^n - 1) moves. Let's attempt to use ACL2 to prove that fact.

First of all, how do we state our conjecture? Recall that hanoi returns a list of moves. The length of the list (given by the function len) is the number of moves required. Thus, we can state the following conjecture. 



  (defthm hanoi-moves-required-first-try
    (equal (len (hanoi a b c n))
           (1- (expt 2 n))))
When we submit this to ACL2, the proof attempt fails. Along the way we notice subgoals such as: 


  Subgoal *1/1'
  (IMPLIES (NOT (< 0 N))
           (EQUAL 0 (+ -1 (EXPT 2 N)))).

This tells us that the prover is considering cases that are uninteresting to us, namely, cases in which n might be negative. The only cases that are really of interest are those in which n is a non-negative natural number. Therefore, we revise our theorem as follows: 



  (defthm hanoi-moves-required
    (implies (and (integerp n) 
                  (<= 0 n))    ;; n is at least 0
             (equal (len (hanoi a b c n))
                    (1- (expt 2 n)))))
and submit it to ACL2 again.

Again the proof fails. Examining the proof script we encounter the following text. (How did we decide to focus on this goal? Some information is provided in ACLH, and the ACL2 documentation on tips may be helpful. But the simplest answer is: this was the first goal suggested by the ``proof-tree'' tool below the start of the proof by induction. See proof-tree.) 



  Subgoal *1/5''
  (IMPLIES (AND (INTEGERP N)
                (< 0 N)
                (NOT (EQUAL N 1))
                (EQUAL (LEN (HANOI A C B (+ -1 N)))
                       (+ -1 (EXPT 2 (+ -1 N))))
                (EQUAL (LEN (HANOI B A C (+ -1 N)))
                       (+ -1 (EXPT 2 (+ -1 N)))))
           (EQUAL (LEN (APPEND (HANOI A C B (+ -1 N))
                               (CONS (LIST 'MOVE A 'TO C)
                                     (HANOI B A C (+ -1 N)))))
                  (+ -1 (* 2 (EXPT 2 (+ -1 N))))))
It is difficult to make much sense of such a complicated goal. However, we do notice something interesting. In the conclusion is a term of the following shape. 


   (LEN (APPEND ... ...))
We conjecture that the length of the append of two lists should be the sum of the lengths of the lists. If the prover knew that, it could possibly have simplified this term earlier and made more progress in the proof. Therefore, we need a rewrite rule that will suggest such a simplification to the prover. The appropriate rule is: 


  (defthm len-append
    (equal (len (append x y))
           (+ (len x) (len y))))
We submit this to the prover, which proves it by a straightforward induction. The prover stores this lemma as a rewrite rule and will subsequently (unless we disable the rule) replace terms matching the left hand side of the rule with the appropriate instance of the term on the right hand side.

We now resubmit our lemma hanoi-moves-required to ACL2. On this attempt, the proof succeeds and we are done.

One bit of cleaning up is useful. We needed the hypotheses that: 



  (and (integerp n) (<= 0 n)).
This is an awkward way of saying that n is a natural number; natural is not a primitive data type in ACL2. We could define a function naturalp, but it is somewhat more convenient to define a macro as follows: 


  (defmacro naturalp (x)
    (list 'and (list 'integerp x)
                  (list '<= 0 x)))
Subsequently, we can use (naturalp n) wherever we need to note that a quantity is a natural number. See defmacro for more information about ACL2 macros. With this macro, we can reformulate our theorem as follows: 


  (defthm hanoi-moves-required
    (implies (naturalp n)
             (equal (len (hanoi a b c n))
                    (1- (expt 2 n))))).
Another interesting (but much harder) theorem asserts that the list of moves generated by our hanoi function actually accomplishes the desired goal while following the rules. When you can state and prove that theorem, you'll be a very competent ACL2 user.

By the way, the name ``Towers of Hanoi'' derives from a legend that a group of Vietnamese monks works day and night to move a stack of 64 gold disks from one diamond peg to another, following the rules set out above. We're told that the world will end when they complete this task. From the theorem above, we know that this requires 18,446,744,073,709,551,615 moves: 



  ACL2 !>(1- (expt 2 64))
  18446744073709551615
  ACL2 !>
We're guessing they won't finish any time soon.