> Chess is a lot trickier than it looks. It has so many rules: castling, en passant, pawn promotion, pinning, the discovered check, and the deadlock case of stalemate.
As a kid playing chess with other neighborhood kids back in the day, absolutely none of us even knew about the en passant rule. My first exposure around the same time was completely by accident thanks to a passing reference in a CRPG called Betrayal at Krondor. It comes up in a story about a game that nearly costs an innkeeper her establishment when she loses because of a move she didn’t even know existed.
cainxinth 7 hours ago [-]
A lot of adult players don’t know it either.
If I play a casual game with someone who doesn’t know about en passant and they make a move that opens them up to it, I don’t attempt to take the piece, but I do point it out to them and recommend we use the rule in future games.
> The player’s choice is not restricted to pieces that have been captured previously
I grew up playing chess but my grandfather always insisted that pawns could only be promoted to captured pieces so when I played him we had to play a that variant.
I suspect this came from players not having extra pieces with their chess sets.
yewenjie 1 days ago [-]
> Chess is a lot trickier than it looks. It has so many rules: castling, en passant, pawn promotion, pinning, the discovered check, and the deadlock case of stalemate.
Nit: Pinning and the discovered check are not really rules, but rather names of tactics.
JohnKemeny 1 days ago [-]
Well, if a piece is pinned it's illegal to move it.
Rule 3.9.2: No piece can be moved that will either expose the king of the same colour to check or leave that king in check.
TheOtherHobbes 1 days ago [-]
Unlike en-passant and castling, pinning and discovered checks are consequences of lower-level rules.
At the "Is this move legal?" level, they don't need unique rules of its own if the lower-level rules are specified correctly.
JohnKemeny 1 days ago [-]
3.9.2: no piece can be moved if that exposes or leaves its own king in check.
333c 1 days ago [-]
That's a consequence of not being allowed to put yourself in check (by any means).
anamexis 1 days ago [-]
The only way to put yourself in check is by moving.
yifanl 1 days ago [-]
The only action you can ever take in chess is moving.
PowerElectronix 1 days ago [-]
You can resign, too.
thejokeisonme 1 days ago [-]
You can put yourself in check by moving the king. That has nothing to do with pinning. Adding a rule for pinning is redundant.
anamexis 6 hours ago [-]
It isn’t an added rule for pinning. It’s the only rule about putting yourself in check.
333c 1 days ago [-]
Did you mean putting your opponent in check? In chess, you are not allowed to put yourself in check.
anamexis 1 days ago [-]
You said “ That's a consequence of not being allowed to put yourself in check (by any means).” My point is that there are no other means.
333c 1 days ago [-]
I was replying to a comment quoting an official rule saying "no piece can be moved if that exposes or leaves its own king in check."
I was pointing out that that specific rule (read to mean that moving a piece pinned against a king is not allow) is not strictly necessary. Putting oneself in check is not allowed regardless of whether it's because you moved a piece that was pinned against your king or moved your king directly into the line of sight of an opponent's piece. These are the different "means."
As a sibling comment points out, "The only action you can ever take in chess is moving," so it's not particularly meaningful to say that the only way to put yourself in check is by moving.
anamexis 1 days ago [-]
And likewise, it's not particularly meaningful to say "That's a consequence of not being allowed to put yourself in check (by any means)."
The rule, "3.9.2: no piece can be moved if that exposes or leaves its own king in check." covers both the case of moving a pinned piece as well as moving the king into check, i.e. it covers all "means" of putting yourself into check.
wavemode 1 days ago [-]
That rule doesn't mean it's illegal to move a piece that's pinned. It just means that it's illegal to move it to a square that would expose the king. For example a pawn that's pinned vertically can still push forward, it just can't capture diagonally.
That's why treating colloquial concepts like "pinning" as though they are rules in and of themselves is not really precise or productive.
gobdovan 1 days ago [-]
You can also pin a pawn to a queen, but the pawn can still legally move.
HiroProtagonist 1 days ago [-]
You're both right, depending on whether you mean relative pin vs absolute pin.
zonotope 5 hours ago [-]
Well, a minor piece can be pinned in front of a queen. It would be legal to move the minor piece in that case, but you'd most likely lose the game if both sides' material were even before the move. Pinning is a tactic, not a rule.
munchler 1 days ago [-]
The point is that, logically, the first part of that rule (“expose the king”) is implied by the second part (“leave that king”), so the first part is redundant. You could simplify the rule to:
No piece can be moved that will leave the king of the same color in check.
gpm 1 days ago [-]
Pedantically I disagree, to leave something in a condition it must have been in that condition in the first place. We could have a game where you're allowed to place your king in check, but if it is in check at the start of your turn you must fix that.
While we're being pedantic though it's not a property of the piece that might be able to be moved that will place the king in check. It's a property of the move. For example we might imagine you have a rook between an enemy rook and your king. You can move the rook along the line between the enemy rook and the king, but not perpendicular to it.
The rule should be:
No move can be made where the moving players king is in check in the resulting position
1 days ago [-]
emil-lp 1 days ago [-]
You should submit it to FIDE.
saberience 1 days ago [-]
Pinning isn’t a rule, it’s just something that arises from other rules.
Also, pinning can happen with pieces that don’t include a king, which means you can just move out of the pin and expose whatever other piece.
It’s just a chess tactic, not a rule. It’s like saying a chess skewer is a rule too.
juujian 1 days ago [-]
And discovered check means that it is not sufficient to check the position of the piece you have moved, you also need to check the position of other pieces to see whether there is a new check.
ferd 1 days ago [-]
Shameless plug: a code walkthru modeling the rules of chess, ment as an exercise/teaching functional programming (in Clojure):
> apparently it wasn't until 19th century that people made clear that you couldn't promote a pawn to a King, surprising an attempted checkmate by responding Le roi est mort, vive le roi!
That's the coolest thing ever though, why would you ban such a move, where's the rule of cool when you need it most?
rauljara 1 days ago [-]
Anyone know what language is being used in the blogpost?
While I think everything written in this post is correct, what really is starting bothering me is this over-focus/attention on data even when what you want to express is behavior, let me explain:
The post talks about "transition invariants" that should be somehow different from "state invariants" yet it describe them as:
> These are predicates over a <<state, next-state>> pair ...
i.e. it still is about state, but I find it much more useful to focus on behavior so instead of thinking about how state transition you focus on what the program is allowed to perform, regardless of the underlying data structure.
What I mean is that I'd like the code to tell me why a certain piece can't do such move instead of why it cannot transition it's position to another position and basically dumping its state in my head and there I have to execute the program myself.
seanhunter 1 days ago [-]
> instead of thinking about how state transition you focus on what the program is allowed to perform
The state transition is what the program is or isn't allowed to perform. The state they're talking about in the invariant isn't the program state, it's the game state.
nilslindemann 1 days ago [-]
I read these images of source code the same way as I read images of math formulas on Wikipedia: Not at all.
AMerrit 1 days ago [-]
A nice read. I've been playing around with my own chess program and trying to implement a lot of chess variants like Double Chess and 7 Queen's Chess.
NicoHartmann 1 days ago [-]
I can't wait to show this to my manager next time he asks why it's taking three weeks to build a simple CRUD app.
"Look, if this guys TLA+ logic struggles to model a 1,500-year-old game without crying over a French pawn-capture rule, you can't expect me to integrate Stripe billing without a few state invariant violations."
epolanski 1 days ago [-]
Payments have a gargantuan amount of possible transitions and invariants that are far from trivial to encode.
NicoHartmann 12 hours ago [-]
I showed this to my manager and his response was: "So... three days?"
teiferer 1 days ago [-]
This is just the beginning. You could create more and more advanced invariants. And I am sure that this could be a way to "solve" chess, i.e., prove that it's a draw with perfect play.
arvyy 1 days ago [-]
doubtful, or at least not useful ones. Like, you could describe some invariant along the lines of "the position is winning for the side-to-move, iff there exists move, such that position' := ApplyMove(position, move) is losing for the (now other) side-to-move". But that's just restating minimax algorithm that people have known for 50 years.
As someone dabbling abit around chess engine development, I'm very often impressed by the many intricacies and observations made by people who pushed the envelope. It just doesn't sound plausible people wouldn't have discovered these killer invariants by now if they existed
teiferer 1 days ago [-]
I agree it's hard and non-obvious. If it wasn't then chess would have long been solved by now.
Let's start from the other end. Just a pawn and two kings. It's possible to describe some quite succinct rules for when that's a draw versus a win for the side with the pawn. Agreed? Club players know these by heart. You could write that doen as invariants. As long as the side with the pawn stays inside the "green zone" of the state space, there is nothing the other side can do to void mate. And vice versa, if the game is in the red zone and the other player manages to stay inside that red zone, there is nothing the side with the pawn can do to win. Those areas of the state space, green and red zones, can be described as invariants, in contrast to just enumerating them. It's very compact and can easily be checked by a machine that it's correct.
Now let's add a pawn. And another. And a rook perhaps. The more you add, the harder the condition is to describe, but we live in the age of billion-node-sized neural nets, we have the resources. Eventually you get all pieces on the board, and if the starting position satisfies the draw invariant, that's it. And likely the 960 freestyle chess positions too.
ctchocula 2 minutes ago [-]
> Let's start from the other end. Just a pawn and two kings. It's possible to describe some quite succinct rules for when that's a draw versus a win for the side with the pawn. Agreed? Club players know these by heart. You could write that doen as invariants. As long as the side with the pawn stays inside the "green zone" of the state space, there is nothing the other side can do to void mate.
The flaw in this line of reasoning is that it's easy to come up with a theorem that works for KP vs K. However as the number of pieces increases, it becomes impossible to distill all the branches of possible moves into a simple theorem like that. If what you said were possible, endgame would be a simple flowchart, but look at how much time even GM players use in endgame and how often mistakes are made, and you'll recognize Chess endgame is not distillable into a simple flowchart when there are even as few as 7 pieces on the board.
Given the above, the only option is enumeration, if you want to prove that in all cases the outcome is White win or draw.
necklesspen 23 hours ago [-]
You may want to take a look at the Shannon number, we would need quite a large neural net to solve chess in this way.
teiferer 13 hours ago [-]
The Shannon number is about the size of the state space. What I am dreaming up here is to avoid explicit enumeration by succinct descriptions in the form of logical formulas which have the potential of cutting down the representation size dramatically.
halfcat 17 hours ago [-]
People have done this. They call it tablebases [1]. They’ve computed 7-piece tablebases, but not 8 pieces.
”After the completion of the 7-man, some people were curious about the feasibility of building the 8-man. Ronald de Man estimated that without modifying much the generator, the task requires computers with 64 TB RAM and 2000 TB hard disks[10] (cost about $640K and $40K respectively in 2020). The generator can be modified to work on much cheaper computers with 64 GB RAM but that may need a few thousand years of computing”
And to solve chess you’d need to calculate the 32-piece tablebases.
Like your sibling comment, you seem to be missing my point. Tablebases are fundamentally enumerating positions explicitly even though they use lots of tricks to make that more efficient. I'm talking about foregoing that entirely.
vintermann 1 days ago [-]
That king promotion rule sounds like it made the game more fun.
TacticalCoder 21 hours ago [-]
> It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns: white, then black, then white.
"Chess is a game of imperfect information, but with a very specific kind of imperfectness: fully available information. More specifically, ever single information is visible: you see all your opponents' pieces and he sees all yours, you see how much time he's got left, and he sees how much time you have left".
Who knew it? Chess is actually a concurrent game of imperfect information: with that definition, it's not unlike a real-time strategy game like Warcraft 3.
Who would have guessed it?
somat 21 hours ago [-]
I sometimes dream of actual concurrent wego chess. It ends up a bit involved without a computer, each side has to commit to a move in secret(write it down on a pad) then comes the tricky part, a solid set of rules for situations that don't resolve cleanly under normal chess. stuff like collisions(do we bounce, halt, mutual annihilation?), pass throughs, escapes. I don't play much chess but it sounds like it could be a lot of fun.
gryn 20 hours ago [-]
huh ? where did you see the second quote, I can't find it the post. Was it there before ?
the game is very much a game of perfect information.
phoe-krk 1 days ago [-]
Screenshots of code? In 2026?...
grg0 1 days ago [-]
That's how you know "principal research scientist" are true credentials. I'm sure the offline version is a postscript instead of pdf.
1 days ago [-]
TZubiri 21 hours ago [-]
0.01% chance you are a genius stumbling unto a whole new paradigm
99.9% chance you could have solved this in a couple of hours with some ifs and loops
fnord77 1 days ago [-]
side question, which CS class(es) teach about invariants?
The well-known algorithms book Cormen et al. describes a lot of algorithms using loop invariants. I must say I never really liked this approach but I admit it makes things easier to reason about.
shellfinity 24 hours ago [-]
[flagged]
anthk 1 days ago [-]
[dead]
Rendered at 19:28:51 GMT+0000 (Coordinated Universal Time) with Vercel.
As a kid playing chess with other neighborhood kids back in the day, absolutely none of us even knew about the en passant rule. My first exposure around the same time was completely by accident thanks to a passing reference in a CRPG called Betrayal at Krondor. It comes up in a story about a game that nearly costs an innkeeper her establishment when she loses because of a move she didn’t even know existed.
If I play a casual game with someone who doesn’t know about en passant and they make a move that opens them up to it, I don’t attempt to take the piece, but I do point it out to them and recommend we use the rule in future games.
I grew up playing chess but my grandfather always insisted that pawns could only be promoted to captured pieces so when I played him we had to play a that variant.
I suspect this came from players not having extra pieces with their chess sets.
Nit: Pinning and the discovered check are not really rules, but rather names of tactics.
Rule 3.9.2: No piece can be moved that will either expose the king of the same colour to check or leave that king in check.
At the "Is this move legal?" level, they don't need unique rules of its own if the lower-level rules are specified correctly.
I was pointing out that that specific rule (read to mean that moving a piece pinned against a king is not allow) is not strictly necessary. Putting oneself in check is not allowed regardless of whether it's because you moved a piece that was pinned against your king or moved your king directly into the line of sight of an opponent's piece. These are the different "means."
As a sibling comment points out, "The only action you can ever take in chess is moving," so it's not particularly meaningful to say that the only way to put yourself in check is by moving.
The rule, "3.9.2: no piece can be moved if that exposes or leaves its own king in check." covers both the case of moving a pinned piece as well as moving the king into check, i.e. it covers all "means" of putting yourself into check.
That's why treating colloquial concepts like "pinning" as though they are rules in and of themselves is not really precise or productive.
No piece can be moved that will leave the king of the same color in check.
While we're being pedantic though it's not a property of the piece that might be able to be moved that will place the king in check. It's a property of the move. For example we might imagine you have a rook between an enemy rook and your king. You can move the rook along the line between the enemy rook and the king, but not perpendicular to it.
The rule should be:
No move can be made where the moving players king is in check in the resulting position
Also, pinning can happen with pieces that don’t include a king, which means you can just move out of the pin and expose whatever other piece.
It’s just a chess tactic, not a rule. It’s like saying a chess skewer is a rule too.
https://neuroning.com/boardgames-exercise/notebooks/walkthro...
The implementation makes it really easy to add new piece types or rules. For example, here's the full logic for rooks (sans castling):
That's the coolest thing ever though, why would you ban such a move, where's the rule of cool when you need it most?
The post talks about "transition invariants" that should be somehow different from "state invariants" yet it describe them as:
> These are predicates over a <<state, next-state>> pair ...
i.e. it still is about state, but I find it much more useful to focus on behavior so instead of thinking about how state transition you focus on what the program is allowed to perform, regardless of the underlying data structure.
What I mean is that I'd like the code to tell me why a certain piece can't do such move instead of why it cannot transition it's position to another position and basically dumping its state in my head and there I have to execute the program myself.
The state transition is what the program is or isn't allowed to perform. The state they're talking about in the invariant isn't the program state, it's the game state.
"Look, if this guys TLA+ logic struggles to model a 1,500-year-old game without crying over a French pawn-capture rule, you can't expect me to integrate Stripe billing without a few state invariant violations."
As someone dabbling abit around chess engine development, I'm very often impressed by the many intricacies and observations made by people who pushed the envelope. It just doesn't sound plausible people wouldn't have discovered these killer invariants by now if they existed
Let's start from the other end. Just a pawn and two kings. It's possible to describe some quite succinct rules for when that's a draw versus a win for the side with the pawn. Agreed? Club players know these by heart. You could write that doen as invariants. As long as the side with the pawn stays inside the "green zone" of the state space, there is nothing the other side can do to void mate. And vice versa, if the game is in the red zone and the other player manages to stay inside that red zone, there is nothing the side with the pawn can do to win. Those areas of the state space, green and red zones, can be described as invariants, in contrast to just enumerating them. It's very compact and can easily be checked by a machine that it's correct.
Now let's add a pawn. And another. And a rook perhaps. The more you add, the harder the condition is to describe, but we live in the age of billion-node-sized neural nets, we have the resources. Eventually you get all pieces on the board, and if the starting position satisfies the draw invariant, that's it. And likely the 960 freestyle chess positions too.
The flaw in this line of reasoning is that it's easy to come up with a theorem that works for KP vs K. However as the number of pieces increases, it becomes impossible to distill all the branches of possible moves into a simple theorem like that. If what you said were possible, endgame would be a simple flowchart, but look at how much time even GM players use in endgame and how often mistakes are made, and you'll recognize Chess endgame is not distillable into a simple flowchart when there are even as few as 7 pieces on the board.
Given the above, the only option is enumeration, if you want to prove that in all cases the outcome is White win or draw.
”After the completion of the 7-man, some people were curious about the feasibility of building the 8-man. Ronald de Man estimated that without modifying much the generator, the task requires computers with 64 TB RAM and 2000 TB hard disks[10] (cost about $640K and $40K respectively in 2020). The generator can be modified to work on much cheaper computers with 64 GB RAM but that may need a few thousand years of computing”
And to solve chess you’d need to calculate the 32-piece tablebases.
[1] https://www.chessprogramming.org/Syzygy_Bases
"Chess is a game of imperfect information, but with a very specific kind of imperfectness: fully available information. More specifically, ever single information is visible: you see all your opponents' pieces and he sees all yours, you see how much time he's got left, and he sees how much time you have left".
Who knew it? Chess is actually a concurrent game of imperfect information: with that definition, it's not unlike a real-time strategy game like Warcraft 3.
Who would have guessed it?
the game is very much a game of perfect information.
99.9% chance you could have solved this in a couple of hours with some ifs and loops
There’s a book called Logic for Programmers: https://leanpub.com/logic#table-of-contents
https://www.swi-prolog.org/
The Simply Logical book as a start:
https://book.simply-logical.space/src/simply-logical.html you can get a PDF just fine.
Also, for hardcore mode, get paper and pen, I'm not kidding: (again, just use SWI Prolog): https://www.ida.liu.se/~ulfni53/lpp/bok/
Another approach. Scheme and Logic:
S9 Scheme, get the bleeding edge version and compile it. Enough to do the book:
https://www.t3x.org/s9fes/
Sketchy Lisp, intro to Scheme:
https://archive.org/details/sketchy-lisp
Logic Progamming in Scheme: https://www.t3x.org/amk/index.html