Chess invariants

unprovable

If you like this, you're probably gonna like this: https://en.wikipedia.org/wiki/Chessboard_complex

yewenjie

> 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.

NicoHartmann

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."

vintermann

That king promotion rule sounds like it made the game more fun.

rauljara

Anyone know what language is being used in the blogpost?

phoe-krk

Screenshots of code? In 2026?...

fnord77

side question, which CS class(es) teach about invariants?

duesabati

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.

ferd

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

nilslindemann

I read these images of source code the same way as I read images of math formulas on Wikipedia: Not at all.

vunderba

> 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.

teiferer

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.

AMerrit

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.

sobellian

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.

mathgradthrow

So many of these invariants are redundant and so few of them encode any of the interesting rules of chess.

stymaar

> 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?

TacticalCoder

> 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?

TZubiri

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