国际象棋不变量

# 国际象棋不变量 来源：http://muratbuffalo.blogspot.com/2026/05/chess-invariants.html 国际象棋远比它看起来要棘手。它有非常多的规则：王车易位、吃过路兵、兵升变、牵制、闪击，以及逼和的死锁情况。它是一个并发系统，但具有一种非常特定的并发类型：交错执行。更具体地说，轮流走棋：白方，然后黑方，然后再白方。你猜我们这里对并发系统做什么？我们对它们建模，并提炼它们的不变量。 下面先是一些定义性设定。 [](https://blogger.googleusercontent.com/img/a/AVvXsEieheth329KZWFID8TgPUYxsXcddqVnJITtNzlQdKl_6ZijHM5eabj9Os0AuYsihkAkjrVy9ECIofotAr7MQWx8lI5BDbr8lbvhcMI7PdEmyYsFS8LerDsx00AOJTRBMCSo6ZoVLlOylVRhtB6Xo-bQSgkzSzkufGMjpNfPiKHLfHmfGN7DCCp_IlE-1Go) 在计算机科学或数学论文中，如果你把“第2节：模型与问题”写得足够好，那么论文的其余部分就会自然而然地写出来。有了这样的设定，你就能大致看到动作会是什么。 [](https://blogger.googleusercontent.com/img/a/AVvXsEikc32YDNgo2Ye1s9hJkkEE6xBVjHigF4Sv0I32t1TDwY-vrujJsaM70yEfiS49vhI2iJ-snRAxHAfz0_Qlgu_9x-0ivqIfMBFn0Z6KSsp9y3CWOuUfjwufV8oNc-Pj65phWy_KTTPIbYGkyYuZjr1UlpD0Wyu-9xi9PEmyADPzbxDyLPMHB5LxrQQgNd4) 实际上，先别管动作。让我们看看一些不变量。在推导不变量时，我们会问：什么必须是始终为真的？我发现将安全不变量分为两类很有用：状态不变量（关于单一状态的谓词）和转移不变量（关于一个步骤的谓词）。转移不变量不像状态不变量那样常用，但它们在推理系统转移时可能非常有用，尤其是当你需要推理系统的转移时。对于像国际象棋这样的系统，我认为转移不变量会非常方便，如下文所示。 ## 状态不变量 [](https://blogger.googleusercontent.com/img/a/AVvXsEhsJ4jS2lpTvflFJHGDMZcIFa81Ew3h3_HczmPIVV-rS6CIcSI07Wd-B0MpfBCKtQ8OzXsrgDzxzFCHEcNhK1HMleycrfyF_RuLaMIXt1XACUu81HuE610Z7Zb1YutnR5_usJtNHXzQNjT4jv37YbCWvd_MZlAeS6KAAkOOU0CxVg70bI1qHpnnCXX6FOI) `TypeOK` 表示每个变量都位于正确的空间内。这很无趣，但它捕获的 bug 比我愿意承认的还要多。`OneKingPerColor` 和 `BothKingsOnBoard` 也是合理性检查。`TurnParity` 是第一个有趣的不变量。它将两个状态变量联系在一起：白方在偶数步移动，黑方在奇数步移动。`MakeMove` 动作满足这个 `TurnParity`。`PreviousPlayerNotInCheck` 将规则“你必须在结束回合时不在被将状态”重新表述为“回头看：刚刚移动的玩家不被将军”。`NotBothInCheck` 是一个推论。 ## 转移不变量 这些是关于一对`<this, next>`的谓词，以括号形式书写：`[] [P]_vars`。它们表达的是事物如何在约束下变化。表示法很简单：`x` 是变量 `x` 在当前状态的值，而 `x'` 表示在下一个状态的值。 [](https://blogger.googleusercontent.com/img/a/AVvXsEhY9j3UHT8v9oALhxmfy6Mv2w-I2pcfQqm5yY3pWly5y4tws1vtVKrd9VFEWZulo5Fv-hhOW2l7jnis6Lmwa1a5N90NXZR526gPwQyrZenA_y-SsHgaZK67nDks3cYANLj61hanmhB2aMB679x20ubks06NsDaD6x-PkB0KKOyQ-xvkWqFwiCsiCaMVV2M) `MoveCountStrictlyIncreases` 和 `TurnAlternates` 表示每一步都会增加移动计数，同时颜色交替。如果某个转移违反了这一条，那就出问题了。`PieceCountNonIncreasing` 排除了凭空出现棋子的情况。`SingleCapturePerMove` 进一步收紧：每一步最多有一个棋子消失。`ExactlyTwoSquaresChange` 在这里是最强的。它表示每次移动恰好有两个方格发生变化：源方格（现在为空）和目标方格（现在持有移动的棋子）。 哈哈，没错，这仅仅是一个基本国际象棋规则的模型。这里有一个有用的练习：当加入王车易位、兵、吃过路兵之后，这些不变量中哪些仍然成立？加入王车易位后，`ExactlyTwoSquaresChange` 会被违反：一次移动中会有四个方格发生变化。类似地，吃过路兵会吃掉一个不在目标方格上的棋子，因此有三个方格发生变化。`PieceCountNonIncreasing` 在兵升变时仍然成立（当兵变成后时，计数不变）。 **更新**：James Corey 写道 (https://mastodon.acm.org/@jaymcor/116613347381723112)：正如往常，列举规则甚至在分析之前就让你开始思考。例如，似乎直到19世纪人们才明确不能将兵升变为王，这让人惊讶于一种试图将杀的反应：“Le roi est mort, vive le roi！”