Chess invariants (opens in new tab)

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.It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns: white, then black, then white.You know what we do with concurrent systems here? Here we model them, and we distill their invariants.Here is some setup definitions first.In a CS or math paper, if you writ...