Top
Best
New

Posted by ingve 8 hours ago

Chess invariants(muratbuffalo.blogspot.com)
71 points | 45 comments
NicoHartmann 7 hours 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 6 hours ago|
Payments have a gargantuan amount of possible transitions and invariants that are far from trivial to encode.
ferd 5 hours ago||
Shameless plug: a code walkthru modeling the rules of chess, ment as an exercise/teaching functional programming (in Clojure):

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):

  (defn expand-pmove-for-rook [pmove]
    (->> pmove
      (expand-pmove-dirs [↑ ↓ ← →])
      (pmoves-discard #(or (pmove-on-same-player-piece? %)
                           (pmove-changed-direction? %)))
      (map pmoves-finish-capturing-opponent-piece)
      (pmoves-finish-and-continue))))
vunderba 4 hours 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.

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.

mathgradthrow 1 hour ago||
So many of these invariants are redundant and so few of them encode any of the interesting rules of chess.
sobellian 2 hours ago||
The historical rules also left ambiguous promotion to the opposite color: https://chess.stackexchange.com/questions/8291/pawn-promotio.... This rule was clarified later to restrict to the same color.
yewenjie 7 hours 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 7 hours 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.

wavemode 2 hours 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.

TheOtherHobbes 7 hours 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 6 hours ago||
3.9.2: no piece can be moved if that exposes or leaves its own king in check.
333c 6 hours ago||
That's a consequence of not being allowed to put yourself in check (by any means).
anamexis 5 hours ago||
The only way to put yourself in check is by moving.
thejokeisonme 2 hours 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.
yifanl 4 hours ago||||
The only action you can ever take in chess is moving.
PowerElectronix 3 hours ago||
You can resign, too.
333c 4 hours ago|||
Did you mean putting your opponent in check? In chess, you are not allowed to put yourself in check.
anamexis 4 hours 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 4 hours 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 3 hours 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.

gobdovan 7 hours ago||||
You can also pin a pawn to a queen, but the pawn can still legally move.
HiroProtagonist 5 hours ago||
You're both right, depending on whether you mean relative pin vs absolute pin.
munchler 6 hours 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 2 hours 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

emil-lp 5 hours ago|||
You should submit it to FIDE.
saberience 5 hours 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 7 hours 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.
AMerrit 2 hours 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.
nilslindemann 4 hours ago||
I read these images of source code the same way as I read images of math formulas on Wikipedia: Not at all.
unprovable 8 hours ago||
If you like this, you're probably gonna like this: https://en.wikipedia.org/wiki/Chessboard_complex
srean 5 hours ago|
This is delightful. Thanks.
rauljara 6 hours ago|
Anyone know what language is being used in the blogpost?
nonethewiser 5 hours ago|
TLA+ i think
grg0 3 hours ago||
Correct. Also: https://www.learntla.com/
More comments...