IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The Towers of Hanoi - formulating the problem
The framework for "the towers of Hanoi" problem supposes there to be three pegs and several disks all of different diameters that can be stacked up on the pegs. The restriction is that any disks stacked on a peg must be arranged so that smaller disks are above larger disks. The problem is how, starting with all the disks stacked on one peg, to move them all to another peg one disk at a time, observing the stacking restriction at each move. The problem is generalized to any number of disks.
We shall also consider some variants of the basic problem, various solutions, and various questions about solutions.
For purposes of this exposition, we formalize the pegs by Def Peg == {1...3}; we also define a notation for indication the peg that differs from two given pegs:
We formalize the disks by consecutive numbers {1...n} ranking their diameters, where 1 represents the smallest disk and n the largest.
We represent a stacking situation by a function of type {1...n}Peg that indicates for each disk which peg it is on; observe that this representation is possible because we are representing only those situations where all the disks are on pegs and are stacked in order of size.
We formalize a one disk move between stacking situations by
Def Moving disk k of n takes f to g Def == (i:{1...n}. f(i) = g(i) Peg ik)
Def == & (i:{1...k-1}. f(i) f(k) Peg & g(i) g(k) Peg)
"Moving disk k of n takes f to g" represents situation g {1...n}Peg being gotten from situation f {1...n}Peg by moving the disk k {1...n}. The first conjunct, i:{1...n}. f(i) = g(i) ik, signifies that disk k and no other has been moved. The second conjunct signifies that all the disks smaller than k are located on a peg other than the source peg f(k) and the destination peg g(k) of the move. Note that the first conjunct implies that in the second conjunct the f(i) and g(i) are equal; the formulation given mentioning both f(i) and g(i) simply makes it more obvious that a move can be reversed:
Thm*n:, f,g:({1...n}Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g Moving disk k of n takes g to f
A sequence of stacking situations, whether or not it represents a sequence of legal moves, will be represented as a function over a range of consecutive integers with explicitly indicated endpoints:
s {a...z}{1...n}Peg
A function over consecutive integers is used for convenience of relating positions in a sequence, and the endpoints are allowed to vary (rather than always starting at 1, say) to make combination of sequences somewhat more perspicuous (given the functional representation) than continually shifting the index sets. The property of being a sequence of stacking situations related by consecutive moves is
Defs is a Hanoi(n disk) seq on a..z Def == x,x':{a...z}.
Def == x+1 = x' (k:{1...n}. Moving disk k of n takes s(x) to s(x'))
The x' has been introduced to make pattern matching a little simpler when using this lemma.
Finally, the subject of the towers of Hanoi problem, a restricted kind of sequence of stacking situations, is conveniently formulated as
s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)
which is a sequence whose first stacking situation locates all disks at Pegp, and whose last locates all disks at q.
Pegi:{1...n}. f(i) = g(i)
Peg
i
k)
, f,g:({1...n}
k:{1...n}. Moving disk k of n takes s(x) to s(x'))
i.p) & s(z) = (
