Chess invariants

Join the discussion

• Hacker News
• 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."

  by NicoHartmann
• Payments have a gargantuan amount of possible transitions and invariants that are far from trivial to encode.
  by epolanski
• I read these images of source code the same way as I read images of math formulas on Wikipedia: Not at all.
  by nilslindemann
• 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.

  by duesabati
• > 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.

  by seanhunter
• Anyone know what language is being used in the blogpost?
  by rauljara
• TLA+ i think
  by nonethewiser
• If you like this, you're probably gonna like this: https://en.wikipedia.org/wiki/Chessboard_complex
  by unprovable
• This is delightful. Thanks.
  by srean
• > 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?

  by TacticalCoder
• 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.

  by gryn
• 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.
  by somat
• So many of these invariants are redundant and so few of them encode any of the interesting rules of chess.
  by mathgradthrow
• > 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?

  by stymaar
• 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))))

  by ferd
• > 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.

  by yewenjie
• 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.
  by juujian
• 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.

  by JohnKemeny
• 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.
  by sobellian
• > 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.

  by CSMastermind
• > 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.

  by vunderba
• 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.

  by cainxinth