|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Hanoi}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{The towers of Hanoi \label{psv2000hanoi}% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 We are given 3 pegs $A$, $B$ and $C$, and $n$ disks with a hole, such |
|
12 that no two disks have the same diameter. Initially all $n$ disks |
|
13 rest on peg $A$, ordered according to their size, with the largest one |
|
14 at the bottom. The aim is to transfer all $n$ disks from $A$ to $C$ by |
|
15 a sequence of single-disk moves such that we never place a larger disk |
|
16 on top of a smaller one. Peg $B$ may be used for intermediate storage. |
|
17 |
|
18 \begin{center} |
|
19 \includegraphics[width=0.8\textwidth]{Hanoi} |
|
20 \end{center} |
|
21 |
|
22 \medskip The pegs and moves can be modelled as follows:% |
|
23 \end{isamarkuptext}% |
|
24 \isamarkuptrue% |
|
25 \isacommand{datatype}\ peg\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isanewline |
|
26 \isamarkupfalse% |
|
27 \isacommand{types}\ move\ {\isacharequal}\ {\isachardoublequote}peg\ {\isacharasterisk}\ peg{\isachardoublequote}\isamarkupfalse% |
|
28 % |
|
29 \begin{isamarkuptext}% |
|
30 Define a primitive recursive function% |
|
31 \end{isamarkuptext}% |
|
32 \isamarkuptrue% |
|
33 \isacommand{consts}\isanewline |
|
34 \ \ moves\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ peg\ {\isacharequal}{\isachargreater}\ peg\ {\isacharequal}{\isachargreater}\ peg\ {\isacharequal}{\isachargreater}\ move\ list{\isachardoublequote}\isamarkupfalse% |
|
35 % |
|
36 \begin{isamarkuptext}% |
|
37 such that \isa{moves}$~n~a~b~c$ returns a list of (legal) |
|
38 moves that transfer $n$ disks from peg $a$ via $b$ to $c$. |
|
39 Show that this requires $2^n - 1$ moves:% |
|
40 \end{isamarkuptext}% |
|
41 \isamarkuptrue% |
|
42 \isacommand{theorem}\ {\isachardoublequote}length\ {\isacharparenleft}moves\ n\ a\ b\ c{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}{\isacharcircum}n\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isamarkupfalse% |
|
43 \isamarkupfalse% |
|
44 % |
|
45 \begin{isamarkuptext}% |
|
46 Hint: You need to strengthen the theorem for the |
|
47 induction to go through. Beware: subtraction on natural numbers |
|
48 behaves oddly: $n - m = 0$ if $n \le m$.% |
|
49 \end{isamarkuptext}% |
|
50 \isamarkuptrue% |
|
51 \isamarkupfalse% |
|
52 \end{isabellebody}% |
|
53 %%% Local Variables: |
|
54 %%% mode: latex |
|
55 %%% TeX-master: "root" |
|
56 %%% End: |