There are a few analysis rules we can suggest which restrict the number of possibly optimal strategies. One is that it is always a losing move to leave a rectangle larger than 1x1. Because that would be equivalent to letting the opponent have the first move in a smaller game of Chomp.
Zermelo's theorem has a counterpart for infinite games, specifically, on when an infinite game has a winning strategy. It goes by the name of the Gale--Stewart theorem; I find it particularly neat that the condition essentially ends up being topological (the game has a winning strategy if the set of games which Holmes wins form an open or closed subset in the space of all games).
One of my favourite examples of a non-constructive proof is the following:
Prove that there exist two irrational numbers a and b such that a raised to the power of b, a^b, is a rational number.
Consider the number (x^x)^x where x is the square root of 2. Now, (x^x)^x = x^(x²) = x² = 2, a rational number.
So, if x^x is irrational, then we can take a = x^x and b = x (which is irrational, since x is the square root of 2), and we’re done.
On the other hand, if x^x is not irrational, then it is rational and we can choose a = b = x, and we’re done.
Either way, there exists a pair of irrational numbers a and b such that a^b is rational but we don’t necessarily have to construct a and b explicitly to prove that assertion.
They used a computer to analyze a portion of chess: Queen vs Rook and Bishop endgames.
There are a few of them where black can win because the Queen starts out pinned by the Bishop or something but in most cases the Queen is not in imminent danger of being taken, traded, or trapped. Does the side with the Queen have a forced win then? Yes. Let's say the side with the Queen is white. The way they did it was they constructed first all positions in which white was in a position to administer checkmate or to safely take the bishop or the rook without causing stalemate. Rotations and reflections are considered equal.
Then they constructed all positions where white was on move and could make a move such that all possible black replies led to one or another of those previously identified as winning positions. In each case, they recorded on just that the position was won, but a move that won.
In this way they worked backward until all initial legal positions with white on move were tagged with the winning move.
Forward-looking analysis would have been much more difficult computationally than working back from simple won positions to more complicated ones.
Strange... Just try the first move: depending on which square you hit, you'll bite off a rectangle, or two rectangles, as it it were the second move. Oh, well, I understand: the program immediately makes the next move!
There are a few analysis rules we can suggest which restrict the number of possibly optimal strategies. One is that it is always a losing move to leave a rectangle larger than 1x1. Because that would be equivalent to letting the opponent have the first move in a smaller game of Chomp.
Zermelo's theorem has a counterpart for infinite games, specifically, on when an infinite game has a winning strategy. It goes by the name of the Gale--Stewart theorem; I find it particularly neat that the condition essentially ends up being topological (the game has a winning strategy if the set of games which Holmes wins form an open or closed subset in the space of all games).
In another life I wrote a blog post explaining this, picking Conway's Sylver coinage as a starting point. Readers of this blog might like it (https://pas201.user.srcf.net/posts/2020-08-06-Winning-Strategies.html), pardon the shameless self-advertising.
One of my favourite examples of a non-constructive proof is the following:
Prove that there exist two irrational numbers a and b such that a raised to the power of b, a^b, is a rational number.
Consider the number (x^x)^x where x is the square root of 2. Now, (x^x)^x = x^(x²) = x² = 2, a rational number.
So, if x^x is irrational, then we can take a = x^x and b = x (which is irrational, since x is the square root of 2), and we’re done.
On the other hand, if x^x is not irrational, then it is rational and we can choose a = b = x, and we’re done.
Either way, there exists a pair of irrational numbers a and b such that a^b is rational but we don’t necessarily have to construct a and b explicitly to prove that assertion.
They used a computer to analyze a portion of chess: Queen vs Rook and Bishop endgames.
There are a few of them where black can win because the Queen starts out pinned by the Bishop or something but in most cases the Queen is not in imminent danger of being taken, traded, or trapped. Does the side with the Queen have a forced win then? Yes. Let's say the side with the Queen is white. The way they did it was they constructed first all positions in which white was in a position to administer checkmate or to safely take the bishop or the rook without causing stalemate. Rotations and reflections are considered equal.
Then they constructed all positions where white was on move and could make a move such that all possible black replies led to one or another of those previously identified as winning positions. In each case, they recorded on just that the position was won, but a move that won.
In this way they worked backward until all initial legal positions with white on move were tagged with the winning move.
Forward-looking analysis would have been much more difficult computationally than working back from simple won positions to more complicated ones.
The example you mentioned:
https://www.math.ucla.edu/~tom/Games/chomp.html
doesn't follow the rule.
It does: the board is just flipped horizontally from my example.
Strange... Just try the first move: depending on which square you hit, you'll bite off a rectangle, or two rectangles, as it it were the second move. Oh, well, I understand: the program immediately makes the next move!