Decidability of chess on an infinite board

Question

The recent question Do there exist chess positions that require exponentially many moves to reach? of Tim Chow reminds me of a problem I have been interested in. Is chess with finitely many men on an infinite board decidable? In other words, given a position on an infinite board (say $\mathbb{Z}\times \mathbb{Z}$, though now pawn promotion is not possible) with finitely many men, say with White to move, is there an algorithm to determine whether White can checkmate Black (or prevent Black from checkmating White) against any Black defense?

Answer 1

There is a positive solution for the decidability of the mate-in-$n$ version of the problem.

Many of us are familiar with the White to mate in 3 variety of chess problems, and we may consider the natural analogue in infinite chess. Thus, we refine the winning-position problem, which asks whether a designated player has a winning strategy from a given position, to the mate-in-$n$ problem, which asks whether a designated player can force a win in at most $n$ moves from a given finite position. (And note that as discussed in Johan Wästlunds's question checkmate in $\omega$ moves?, there are finite winning positions in infinite chess which are not mate-in-$n$ for any finite $n$.) Even so, the mate-in-$n$ problem appears still to be very complicated, naturally formulated by assertions with $2n$ many alternating quantifiers: there is a move for white, such that for every black reply, there is a countermove by white, and so on. Assertions with such quantifier complexity are not generally decidable, and one cannot expect to search an infinitely branching game tree, even to finite depth. So one might naturally expect the mate-in-$n$ problem to be undecidable.

Despite this, the mate-in-n problem of infinite chess is computably decidable, and uniformly so. Dan Brumleve, myself and Philipp Schlicht have just submitted an article establishing this to the CiE 2012, and I hope to speak on it there in June.

D. Brumleve, J. D. Hamkins and P. Schlicht, "The mate-in-n problem of infinite chess is decidable," 10 pages, arxiv pre-print, submitted to CiE 2012.

Abstract. Infinite chess is chess played on an infinite edgeless chessboard. The familiar chess pieces move about according to their usual chess rules, and each player strives to place the opposing king into checkmate. The mate-in-$n$ problem of infinite chess is the problem of determining whether a designated player can force a win from a given finite position in at most n moves. A naive formulation of this problem leads to assertions of high arithmetic complexity with $2n$ alternating quantifiers---there is a move for white, such that for every black reply, there is a counter-move for white, and so on. In such a formulation, the problem does not appear to be decidable; and one cannot expect to search an infinitely branching game tree even to finite depth. Nevertheless, the main theorem of this article, confirming a conjecture of the first author and C. D. A. Evans, establishes that the mate-in-$n$ problem of infinite chess is computably decidable, uniformly in the position and in $n$. Furthermore, there is a computable strategy for optimal play from such mate-in-$n$ positions. The proof proceeds by showing that the mate-in-$n$ problem is expressible in what we call the first-order structure of chess $\frak{Ch}$, which we prove (in the relevant fragment) is an automatic structure, whose theory is therefore decidable. Unfortunately, this resolution of the mate-in-$n$ problem does not appear to settle the decidability of the more general winning-position problem, the problem of determining whether a designated player has a winning strategy from a given position, since a position may admit a winning strategy without any bound on the number of moves required. This issue is connected with transfinite game values in infinite chess, and the exact value of the omega one of chess $\omega_1^{\rm chess}$ is not known.

The solution can also be cast in terms of Presburger arithmetic, in a manner close to Dan Brumleve's answer to this question. Namely, once we restrict to a given collecton of pieces $A$, then we may represent all positions using only pieces in $A$ as a fixed-length tuple of natural numbers, and the elementary movement, attack and in-check relations are expressible for this representation in the language of Presburger arithmetic, essentially because the distance pieces---rooks, bishops and queens---all move on straight lines whose equations are expressible in Presburger arithmetic. (There is no need to handle sequence coding in general, since the number of pieces does not increase during play.) Since the mate-in-$n$ problem is therefore expressible in Presburger arithmetic, it follows that it is decidable.

Answer 2

Yes, because any chess position can be translated into Presburger arithmetic. For a fixed initial combination of piece types, let's define a position to consist of an (x, y) location for each piece as well as a bit (c) to indicate whether or not it has been captured. Multiplication of these parameters is not required to describe the legality and the effects of any one move, so in Presburger arithmetic we can recursively define the proposition "White cannot capture Black's King in fewer than t moves starting from initial position X.", then apply the axiom schema of induction to get an expression meaning "White cannot ever checkmate starting from initial position X." Since Presburger arithmetic is complete we will always be able to prove either this statement or its negation.

EDIT: Summary of how this is supposed to work:

1. P(A) = It is White's move and White has not yet won in position A.
2. R(A, B) = Position B legally follows in one move from position A.
3. Q(A, 0) = P(A)
4. Q(A, t) = for all B: (R(A, B) -> there exists C: R(B, C) -> Q(C, t - 1))
5. S(A) = Q(A, 0) and (for all t: Q(A, t) -> Q(A, t + 1))

This works fine at least up to line four where Q(A, t) is defined recursively. If Q(A, t) could be defined as a predicate in Presburger arithmetic then I think line five would also work. But this is a serious problem and maybe breaks the whole approach.

Answer 3

There's no such algorithm under at least one rigorous specification of the question.

Consider a position in which there is a black king at (0,0) and no other black pieces; white rooks at $(1,5)$ and $(-1,5)$, and possibly a white queen at a position of the form (0,$n$) for some large $n$. Picture a king backed into a long tunnel. Then white can checkmate black (and does, from the start) if and only if the queen actually exists somewhere along the tunnel. If there are only two rooks, I believe that the king can stave off checkmate by moving off towards infinity indefinitely (see my explanation in the comments below).

Using positions like that, given any r.e. set $K$ and any number $m$, I can make a chess position such that white can checkmate black if and only if $m \in K$: I put the queen at $(0,n+5)$ if and only if $m$ is enumerated in $K$ after exactly $n$ steps. So I can decide membership in $K$, relative to an oracle for your problem. Actually I only need an oracle that works for indices of computable positions. This shows that any solution to your problem is of degree at least $0'$.

Note: I have taken a "position" to be a function from locations on the board to pieces. You could try to work around this solution by specifying something else as a "position". For example, you could make a position a function from a list of pieces to locations on the board, and that might lead to a different solution. However you need to require the list to explicitly say how many pieces there are from the beginning, or a variation of this solution will still apply.

Answer 4

Yes. There is a finite board size that has essentially the same solution structure as all larger boards and an infinite board, and we can find it by solving the game completely for increasing board sizes until that ultimate size can be recognized. (The infinite board is different from a very large board only in that it has no edges or corners, so its solution structure is smaller.) Eventually this is possible, because there are only a finite number of pieces, and therefore only a finite number of equivalence classes of solution structures. When the number of such equivalence classes stops growing, we are done. Basically, all positions with pieces not close to the edge of the board but far from the center (say those with pieces inside an annulus) can be identified with more bounded positions (those surrounded by that annulus), because the pieces with an infinite number of options (Queen, Rook, Bishop) can go anywhere (up to parity) with no more than 2 moves, and the other pieces are forced to walk long distances for which all that matters are their relative path lengths to a certain precision. When one set of pieces moves far enough away from another set of pieces that the two sets are now in general position, these sub-problems interact in an equivalent way, so the description of the complete solution will eventually stop increasing with board size.

More generally this strategy works for any chess-like game in which the pieces can be classified into "ultra-mobile" and "para-mobile" types with constant and linear freedom respectively. For example it is also true for checkers because all pieces are para-mobile.

I am still unable to specify the equivalence between positions precisely enough to set an explicit bound on the necessary size of the finite board in terms of the number of pieces n, but I guess that it is O(f(n!)) for some polynomial function f whose order is O(n), or in other words O((n!)^(k*n)) for some k, using the construction technique that I have suggested. The super-exponential term is contributed by the para-mobile pieces and the polynomial by the ultra-mobiles. In any case I have intended only to demonstrate that the necessary board size has a computable bound.

Answer 5

I would like to convince everyone that this problem is undecidable. I cannot prove it for chess, as I lack the ability to design certain configurations but I think they must exist. And even if they don't, for some chess-like game they certainly do which shows that the attempts to prove decidability should be incorrect.

Hm, after reading the comments to the original question carefully, I realised that there is already a pointer to an argument very similar to mine by Tsuyoshi Ito: http://www.redhotpawn.com/board/showthread.php?threadid=90513&page=1#post_1708006 I still leave my proof here, as in fact two counters are enough and maybe mine is more detailed.

The reduction relies on the notion of counter machine*. It is undecidable whether a counter machine with only two counters halts or not. So our goal would be to simulate any such machine with a chess position. I can see two ways for this.

i, Build two separate configurations, such that both have a starting part and a moving part that can change (to store the state). Also, the moving parts would be connected, eg. by rooks, which could checkmate, if released, so this is why if one states moves 1, the other has to move k, and so on.

ii, Build a single configuration, that depending on its state, moves l horizontally and -k vertically. Also, place a rook at (0,0) that would never move but could guarantee that the configuration can "sense" when it gets back to an empty counter.

So all left to do is to design such configurations, which I guess should be possible with some effort and knowledge of chess. Also, note that in both cases the construction uses a piece whose range is not bounded, I wonder if this is really necessary.

*I realized that the definition on wikipedia is different from what I want. In fact, my machine should be probably called a 2-stack machine that can push only one letter to the stack. So I want a finite state machine with two counters that are empty at the beginning and it can increase or decrease any counter by one or check whether a counter is zero or not. The problem of whether such a machine halts or not, is undecidable.