%%version of July 2, 2007 (6:37pm) % ---------------------------------------------------------------- % AMS-LaTeX Paper ************************************************ % **** ----------------------------------------------------------- \documentclass{amsart} \usepackage{graphicx} \usepackage{color} % ---------------------------------------------------------------- \vfuzz2pt % Don't report over-full v-boxes if over-edge is small \hfuzz2pt % Don't report over-full h-boxes if over-edge is small % THEOREMS ------------------------------------------------------- \newtheorem{thm}{Theorem}[section] \newtheorem{cor}[thm]{Corollary} \newtheorem{lem}[thm]{Lemma} \newtheorem{prop}[thm]{Proposition} \theoremstyle{definition} \newtheorem{defn}[thm]{Definition} \theoremstyle{remark} \newtheorem{rem}[thm]{Remark} \numberwithin{equation}{section} % MATH ----------------------------------------------------------- \newcommand{\norm}[1]{\left\Vert#1\right\Vert} \newcommand{\abs}[1]{\left\vert#1\right\vert} \newcommand{\set}[1]{\left\{#1\right\}} \newcommand{\Real}{\mathbb R} \newcommand{\eps}{\varepsilon} \newcommand{\To}{\longrightarrow} \newcommand{\BX}{\mathbf{B}(X)} \newcommand{\A}{\mathcal{A}} \newcommand{\regT}{{\rm T}} \newcommand{\regF}{{\rm F}} % ---------------------------------------------------------------- \begin{document} \title[A Symbolic Finite-state approach ]{A Symbolic Finite-state approach for Automated Proving of Theorems in Combinatorial Game Theory}% \author{Thotsaporn ``Aek'' Thanatipanonda}% \author{Doron Zeilberger}% \address{Department of Mathematics}% \address{Hill Center-Busch Campus}% \address{Rutgers University}% \address{110 Frelinghuysen Rd}% \address{Piscataway, NJ 08854-8019}% \address{USA}% \email{thot@math.rutgers.edu,zeilberg@math.rutgers.edu}% \subjclass{91A46}% \keywords{Combinatorial Game Theory}% %\date{May 7, 2007}% % ---------------------------------------------------------------- \begin{abstract} We develop a finite-state automata approach, implemented in a Maple package {\tt ToadsAndFrogs} available from our websites, for conjecturing, and then rigorously proving, values for large families of positions in Richard Guy's combinatorial game ``Toads and Frogs''. In particular, we prove a conjecture of Jeff Erickson. \end{abstract} \maketitle % ---------------------------------------------------------------- \section{Introduction} The game {\it Toads and Frogs}, invented by Richard Guy, is extensively discussed in ``Winning Ways''[1], the famous classic by Elwyn Berlekamp, John Conway, and Richard Guy, that is the {\it bible} of combinatorial game theory. \\ This game got so much coverage because of the simplicity and elegance of its rules, the beauty of its analysis, and as an example of a combinatorial game whose positions do not always have values that are numbers. \\ The game is played on a $1 \times n$ strip with either Toad(T) , Frog(F) or $\Box$ on the squares. Left plays T and Right plays F. T may move to the immediate square on its right, if it happens to be empty, and F moves to the next empty square on the left, if it is empty. If T and F are next to each other, they have an option to jump over one another, in their designated directions, provided they land on an empty square. (See [1], page 14).\\ \noindent In symbols: the following moves are legal for Toad: \\ \noindent $\dots \regT \Box \dots \;\ \rightarrow \;\ \dots \Box \regT \dots $,\\ $\dots \regT \regF \Box \dots \;\ \rightarrow \;\ \dots \Box \regF \regT \dots $ \;\ , \\ \noindent and the following moves are legal for Frog: \\ \noindent $\dots \Box \regF \dots \;\ \rightarrow \;\ \dots \regF \Box \dots $,\\ $\dots \Box \regT \regF \dots \;\ \rightarrow \;\ \dots \regF \regT \Box \dots \quad $ . \\ Already in ``Winning Ways''[1], there is some analysis of Toads and Frogs positions, but on {\it specific}, small boards, such as $\regT \regT \regT \Box \regF \regF$. In 1996, Jeff Erickson[2] analyzed more general positions. At the end he made five conjectures about the values of some families of positions. All of them are ``starting'' positions (i.e. positions where all T's are rightmost and all F's are leftmost).\\ To be able to understand the present article, readers need some knowledge of combinatorial game theory, that can be found in [1]. In particular, readers should be familiar with the notion of {\it value} of a game. Recall that values are not always numbers (not even surreal ones).\\ Let's recall the {\it bypass reversible move rule}, the {\it dominated options rule} (see [1] page 62-64) and Erickson's {\it Terminal Toads Theorem} (see[2]).\\ \noindent \textbf{Bypassing right's reversible move rule}\\ \begin{figure} [ht] \input{tf10.pstex_t} \caption{The Bypassing reversible move rule.} \end{figure} \noindent $G = H$ if $D^{L} \geq G.$\\ \noindent \textbf{The Dominated options Rule} \\ \noindent Let $G = \{A,B,C,... \mid D,E,F,.. \}.$\\ If $A \geq B$ and $D \geq E$ then $G = \{A,C,... \mid E,F,.. \}.$\\ \noindent \textbf{The Terminal Toads Theorem}: Let X be any position. Then\\ $ {\rm X} \regT \Box^{n} = {\rm X} \Box^{n} + n.$\\ The only notation we use is $ * \;\ ( = \{ 0 \mid 0 \})$. We will not use any shorthand notation like $\uparrow$, $\Uparrow$, etc.\\ Next, we will explain the method through examples, and describe how to implement the method when applied to certain classes of positions. Finally, we discuss a new conjecture and possible future work. \\ Everything is fully implemented in a Maple package, {\tt ToadsAndFrogs}, written by the first author, available from our websites. % ---------------------------------------------------------------- \section{A Symbolic Finite-State Method} \noindent We define two classes of positions:\\ \noindent Class {\bf A}: All the positions that have a {\it fixed} number of occurrences of $\Box$ and F, but a {\it variable} (symbolic) number of T's in-between the $\Box$'s and F's. \\ \noindent class {\bf B}: All the positions that have a {\it fixed} number of occurrences of T's and F's, but a {\it variable} (symbolic) number of $\Box$'s in-between the T's and F's. \\ \noindent $Aij$ := the class in which we have exactly $i$ occurrences of $\Box$ and exactly $j$ occurrences of $\regF$.\\ \noindent $Bij$ := the class in which we have exactly $i$ occurrences of $\regT$ and exactly $j$ occurrences of $\regF$.\\ For any {\it specific} position, we can always compute its value, by using the recursive definition of the value. But this is mere {\it number-crunching}. After collecting enough data, and examining it, if we are lucky, we (or rather our computers) can detect a uniform {\it pattern}, and {\bf conjecture} an {\bf explicit} formula for the values of the studied family, in terms of the symbolic parameters. Once conjectured, these conjectured explicit expressions can be proved by induction on the symbolic parameters. The beauty and novelty of our approach is that everything is done {\bf automatically}. First the {\it conjecturing} parts, but more dramatically, the {\it proving} part. We teach the computer how to conjecture, by looking for general patterns, and then how to use induction in order to prove its own conjectures. \\ This {\it activity} of {\bf computer-generated} mathematics is in sharp contrast to the traditional approach of [2], that merely uses the computer as a calculator, to generate numerical data, and everything else, the conjecturing, and the proving (when feasible) is done by humans. \\ We believe that the present methodology is of potential use in many other branches of mathematics, and ``Toads and Frogs'' is but an instructive arena for presenting a general approach for computer-generated research.\\ When we analyze each class of positions, we are naturally lead, by the recursive definition of the {\it value} (of a game), to other classes of positions. Luckily, at least in all the cases encountered so far, there are always a {\bf finite} number of different classes, that we can name ``symbolic states''. If the (symbolic) value of each ``state'' in the class is conjectured to have a (symbolic) explicit expression, then we can prove the truth of {\it all} these conjectures {\bf all at once} by applying induction on the recurrence relations. Note that in order for this to work we need to conjecture explicit expressions for {\bf all} the states, so we usually get much more than we bargained for. \\ We will demonstrate the method with the two simplest nontrivial classes: A11 and B11.\\ \noindent \textbf{First example}: Type A11: one $\Box$ and one F \\ \noindent Let $f(a,b)$ be the value of $\regT^{a} \Box \regT^{b} \regF$. \\ Let $g(a)$ be the value of $\regT^{a} \regF \Box$. \\ Here, of course, $\regT^{a}$ means $\regT$ repeated $a$ times, so the `game' $f(a,b)$, for example, stands for a doubly-infinite set of starting positions.\\ \noindent \textbf{Recurrences}: \\ Note that if any parameter of the function is negative then it returns NULL.\\ \begin{figure} [ht] \input{tf11.pstex_t} \caption{Recurrence for $f(a,0), a \geq 0$.} \bigskip $f(a,0) = \{ f(a-1,1) \mid g(a)\} , a \geq 0. $\\ \end{figure} \begin{figure} [ht] \input{tf12.pstex_t} \caption{Recurrence for $f(a,1), a \geq 0$.} \bigskip $f(a,1) = \{ f(a-1,2) \mid g(a)+1\} , a \geq 0.$ \\ \end{figure} \begin{figure} [ht] \input{tf13.pstex_t} \caption{Recurrence for $ f(a,b), a \geq 0, b \geq 2 $.} \bigskip $f(a,b) = \{ f(a-1,b+1) \mid \;\ \} , a \geq 0 , b \geq 2.$ \\ \end{figure} \newpage \begin{figure} [ht] \input{tf14.pstex_t} \caption{Recurrence for $g(a), a \geq 0$.} \bigskip $g(a) = \{ f(a-1,0) \mid \;\ \}, a \geq 0$. \\ \end{figure} The above recurrences can be easily used to crank out {\it numerical data} for small (and not so small) values of $a$ and $b$. Then the computer {\it automatically} makes the following {\it symbolic} conjectures.\\ \noindent \textbf{Conjectures}: \[ \begin{array}{llll} f(0,0) &=& -1. \\ f(a,0) &=& \{\{a-2 \mid 1 \} \mid 0 \} &, \;\ a \geq 1. \\ f(a,1) &=& \{ a-1 \mid 1 \} &, \;\ a \geq 0.\\ f(a,b) &=& a &,\;\ a \geq 0, \;\ b \geq 2.\\ g(a) &=& 0 &, \;\ a \geq 0.\\ \\ \end{array} \] Once conjectured, the proof is routine, and also can (and was!) done by computer. One checks the obvious initial conditions and verifies that the above expressions satisfy the above {\it defining} relations. Indeed, the computer easily verifies that \[ \begin{array}{llll} f(a,0) &=& \{f(a-1,1) \mid g(a) \} = \{\{ a-2\mid 1 \} \mid 0 \} &,\;\ a \geq 1. \\ f(0,1) &=& \{ \;\ \mid g(0)+1 \} = \{ \;\ \mid 1 \} = 0 = \{ -1 \mid 1 \}. \\ f(a,1) &=& \{f(a-1,2) \mid g(a)+1 \} = \{ a-1\mid 1 \} &, \;\ a \geq 1. \\ f(0,b) &=& \{ \;\ \mid \;\ \} = 0 &, \;\ b \geq 2. \\ f(a,b) &=& \{f(a-1,b+1) \mid \;\ \} = \{ a-1\mid \;\ \} = a &, \;\ a \geq 1, b \geq 2. \\ g(0) &=& \{ \;\ \mid \;\ \} = 0. \\ g(1) &=& \{f(0,0) \mid \;\ \} = \{ -1\mid \;\ \} = 0. \\ g(a) &=& \{f(a-1,0) \mid \;\ \} = \{\{\{ a-3\mid 1 \} \mid 0 \}\mid \;\ \}\\ &=& \{ \;\ \mid \;\ \}$ (!! by bypass reversible move rule) $= 0 &, \;\ a \geq 2. \\ \\ \end{array} \] Note that the above values for $f(a,0)$ ($a \geq 1$) agree with the case $b=1$ of Theorem 5.2 of [2]. \\ \noindent \textbf{Second Example}: Type B11: one T and one F. \\ \noindent Let $f(a,b,c) := \Box^{a} \regT \Box^{b} \regF \Box^{c}.$ \\ \noindent Now we have a {\it three-} parameter family!\\ \noindent \textbf{Initial Conditions and Recurrences}: \\ \[ \begin{array}{llll} f(0,0,0) &=& \{ \;\ \mid \;\ \}.\\ f(a,0,0) &=& \{ \;\ \mid (-a+1)+1\} = \{ \;\ \mid -a+2 \} &, \;\ a \geq 1.\\ f(0,0,c) &=& \{ (c-1)-1\mid \;\ \} = \{ c-2 \mid \;\ \} &, \;\ c \geq 1.\\ f(a,0,c) &=& \{ c-a-2\mid c-a+2\} &, \;\ a \geq 1, c \geq 1.\\ \end{array} \] \begin{figure} [ht] \input{tf15.pstex_t} \caption{Recurrence of $f(a,b,c), a \geq 0, c \geq 0, b \geq 1 $.} \bigskip $f(a,b,c) = \{ f(a+1,b-1,c)\mid f(a,b-1,c+1) \}, \;\ a \geq 0, c \geq 0, b \geq 1$.\\ \end{figure} By using these recurrences {\it numerically}, the computer cranks out enough data, that enables it to make the following\\ \noindent \textbf{Conjecture}: \\ \[ \begin{array}{llll} f(a,b,c) &=& \{ c-a-2\mid c-a+2\} &, \;\ a \geq 0, c \geq 0 , b\mbox{ is even}.\\ f(a,b,c) &=& \{\{ c-a-3\mid c-a+1\} \mid \{ c-a-1\mid c-a+3\}\} &, \;\ a \geq 0, c \geq 0, \, b \mbox{ is odd }.\\ \end{array} \] \\ \noindent \textbf{Proof:} by induction: on $b$. \\ \noindent \textbf{Base case}: $b$ = 0\\ We have \[ \begin{array}{llll} f(0,0,0) &=& 0 = \{-2 \mid 2 \} . \\ f(a,0,0) &=& \{\;\; \mid -a+2 \} = \{-a-2 \mid -a+2 \} , \;\ &a \geq 1.\\ f(0,0,c) &=& \{ c-2 \mid \;\ \} = \{c-2 \mid c+2 \} ,&c \geq 1.\\ f(a,0,c) &=& \{ c-a-2\mid c-a+2\} ,&a \geq 1, c \geq 1.\\ \end{array} \] \noindent \textbf{Induction step} on $b$ \\ \noindent Case 1) $b$ is even and $b \neq 0$: \[ \begin{array}{llll} f(a,b,c) &=& \{ f(a+1,b-1,c)\mid f(a,b-1,c+1) \} ,\;\ a \geq 0, c \geq 0.\\ &=& \{\{ c-a-4\mid c-a\} \mid \{ c-a-2\mid c-a+2\}\} \\ && \mid \{\{ c-a-2\mid c-a+2\} \mid \{ c-a\mid c-a+4\}\}\}.\\ &=& \{ c-a-2 \mid c-a+2 \}. \\ \end{array} \] \noindent Case 2) $b$ is odd \[ \begin{array}{llll} f(a,b,c) &=& \{ f(a+1,b-1,c)\mid f(a,b-1,c+1) \} &, a \geq 0, c \geq 0.\\ &=& \{\{ c-a-3\mid c-a+1\} \mid \{ c-a-1 \mid c-a+3\}\}. \\ \\ \end{array} \] The second example is related to the results of Erickson [2] as follows. The case $b=0$ is Lemma 4.1 of [2], while the case $a=0,c=0$ coincides with the case $a=1$ of Theorem 5.2. Note that we need the extra elbow-room of a three-parameter family to enable the inductive argument. \\ % ---------------------------------------------------------------- \section{How far can the symbolic finite state method go?} As we mentioned in the previous section, the finite state method works perfectly well when the value of every position in the class has a discernible pattern. This seems to be the case for class A. We wrote a computer program in Maple to first {\it calculate}, then {\it conjecture}, and finally {\it prove}, the values of general positions in class A automatically. The program now works for positions with any fixed number of $\Box$'s and with one Frog. For the class where we have more than one Frog, it is harder to find conjectures, for humans, and {\it even} for computers. We conjectured some classes with two Frogs(A12, A22, A32) by hand and put it in the computer program to prove the conjectures.\\ The list of the results for the classes A11, A21, A31, A41, A51, A12, A22, A32 can be found in both authors' websites. \\ As a very special case of our results for the class A32, we get a proof of Erickson's[2] conjecture 2, that claims that the value of $\regT^{a} \Box\Box\Box \regF \regF$ is $ \{ a-2 \mid a-2 \}$, ( $a \geq 2$).\\ In [3], the first-named author of the present paper discusses the value of {\it any} position with one $\Box$ and {\it any} number of Toads and Frogs (Therefore we are done with class $A1n$, $n \geq 1$). This general class with one $\Box$ is the only general class we are able to figure out the patterns for.\\ \noindent We now turn our attention to class B. We solved class B11 in the previous section. For B21: TTF, we already have a difficulty. The formulas in this class are long and hard to find in a canonical form. We will discuss this in the appendix.\\ % ---------------------------------------------------------------- \section{A Conjecture and Future Work} \noindent \textbf{Conjecture}: \\ 1) We always have ``nice compact'' formulas for every position in class A.\\ \noindent \textbf{Future Work}: \\ 1) Implement the symbolic finite state method for the class B21.\\ 2) We have seen systems of recurrence relations arising naturally in each class. We solved the recurrences by ``guessing'' (automatically, of course) the answers (using predefined {\it ansatzes}) and then proving them by induction. It would be interesting to develop general algorithms for systematically solving the recurrences, without the need for ``guessing''. \\ % ---------------------------------------------------------------- \renewcommand{\theequation}{A-\arabic{equation}} % redefine the command that creates the equation no. \setcounter{equation}{0} % reset counter \section*{APPENDICES} % use *-form to suppress numbering \appendix{} \section{On the difficulty of class B21: TTF} \noindent \textbf{B21}: TTF \noindent $f(a,b,c,d) := \Box^{a} \regT \Box^{b} \regT \Box^{c} \regF \Box^{d}.$\\ $g(a,b,c) := \Box^{a} \regT \Box^{b} \regF \Box^{c}.$\\ \noindent We already knew the solution of g since it is exactly B11.\\ We can now focus on f.\\ \noindent \textbf{Recurrences}: \[ \begin{array}{llll} f(a,0,0,0) &=& \{ \;\ \mid \;\ \} = 0.\\ f(a,0,0,d) &=& \{ g(a,1,d-1)+d-1 \mid \;\ \} \\ &=& \{\{\{ d-a-4 \mid d-a \} \mid \{ d-a-2 \mid d-a+2 \}\} \mid \;\ \} \\ &&,\;\ a\geq 0, \;\ d \geq 1.\\ f(a,b,0,0) &=& \{ f(a+1,b-1,0,0) \mid g(a,b-1,1)+1 \} \\ &&, \;\ a \geq 0, b \geq 1.\\ f(a,b,0,d) &=& \{ f(a+1,b-1,0,d) ,\;\ g(a,b+1,d-1)+d-1 \mid g(a,b-1,d+1)+d+1 \} \\ &&, \;\ a \geq 0, b \geq 1, d \geq 1.\\ f(a,b,c,d) &=& \{ f(a+1,b-1,c,d) ,\;\ f(a,b+1,c-1,d) \mid f(a,b,c-1,d+1) \} \\ &&, \;\ a \geq 0, b \geq 0, c \geq 1, d \geq 0.\\ \end{array} \] \noindent Note: $f(a,0,0,d)$ has been discussed before as lemma 4.3 by Erickson.\\ \noindent \textbf{A nice formula for $f(a,b,0,0)$}. \\ \noindent For b =1: \[ \begin{array}{llll} f(a,1,0,0) &=& \{ f(a+1,0,0,0) \mid g(a,0,1) +1 \} \\ &=& \{ 0 \mid \{ -1-a \mid 3-a \} +1 \} \\ &=& \left\{ \begin{array}{ll} \frac{1}{2} & \mbox{, a = 0,1} \\ \{0 \mid 3-a \} & \mbox{, a} \geq \mbox{2} \\ \end{array} \right. \end{array} \] \noindent For b $\geq$ 2 and b is even: \[ \begin{array}{llll} \noindent f(a,b,0,0) &=& \left\{ \begin{array}{ll} 1 & \mbox{, a = 0 } \\ -a+2 & \mbox{, a } \geq 1. \\ \end{array} \right. \\ &=& \{ \;\ \mid a \} -a+2. \\ \end{array} \] \noindent For b $\geq$ 2 and b is odd. \\ \[ \begin{array}{llll} f(a,b,0,0) = \left\{ \begin{array}{ll} \{1 \mid 1\} &, a = 0 \\ \frac{1}{2} &, a = 1 \\ -a+2 &, a \geq 2 .\\ \end{array} \right. \end{array} \] \\ However for $f(a,b,0,d) , a\geq 0, b \geq 1, d\geq 1$ , the formulas get longer and longer and we started to lose track of them, and consequently failed to find formulas in this case. It should be possible to write Maple code specifically to find a pattern for the values of positions in class B. The authors expect the formulas in other classes of type B (for example B22: TTFF) to be even more complicated than B21, since it has to build up from B21. \\ It appears that the positions in class B have periodicity and they need more care to formulate the right conjectures. \\ %----------------------------------------------------------------- \section{ About the program} Our Symbolic Finite-State Method was implemented by one of us (TT) in Maple. He first wrote a program to recursively calculate the values of games. Then he improved the program by making use of the symbolic computation capability of Maple, to formulate conjectures, and prove the values of game-positions. The whole proof process was completely automated. Below is the short description of the program. See the authors' web sites for complete details of the program.\\ \noindent \textbf{ToFr} \\ {\bf Input}: the specific position of the game. \\ {\bf Output}: the value of the game in canonical form.\\ \noindent \textbf{SVG} \\ {\bf Input}: the value of the game, could be symbolic. \\ {\bf Output}: the value of the game in canonical form.\\ Note: This program can also be used for other combinatorial games.\\ \noindent \textbf{MainConj} \\ {\bf Input}: number of $\Box$ and number of F. \\ {\bf Output}: The list of conjectures. \\ \noindent \textbf{Prove} \\ {\bf Input}: number of $\Box$ and number of F.\\ {\bf Output}: the values of all of the positions in this class.\\ The program currently only works for one Frog with any fixed number of $\Box$. With more than one Frog, it gets harder to find conjectures. But one could find conjectures by hand and feed them to the subfunctions in Prove. The program can help verify such humanly-made conjectures.\\ \noindent Obviously, there is still a lot of work to be done, but let's remember that \\ \noindent `` {\bf Every great artwork always starts from a rough draft}''.\\ % ---------------------------------------------------------------- \begin{thebibliography}{9} \bibitem{} Elwyn Berlekamp, John Conway, and Richard Guy, {\em{Winning Ways for your Mathematical Plays}}, Academic Press, New York, 1982. \\ \bibitem{} Jeff Erickson, {\em{New Toads and Frogs Results}}, in: ``Games of No Chance'', 299-310, Richard J. Nowakowski, ed., Math. Sci. Res. Inst. Publ. {\bf 29}, 1996.\\ \bibitem{} Thotsaporn ``Aek'' Thanatipanonda, {\em{Further Hopping with Toads and Frogs}}, preprint (available from the author's website) .\\ \end{thebibliography} \end{document} % ----------------------------------------------------------------