国际象棋不变量

国际象棋不变量 获取链接 Facebook X Pinterest 电子邮件其他应用程序 - May 21, 2026 国际象棋比看起来要棘手得多。它有很多规则：易位、过路、典当晋级、钉住、发现检查以及相持的僵局情况。它是一个并发系统，但具有一种非常特殊的并发性：交错执行。更具体地说，轮流：白色，然后黑色，然后白色。你知道我们在这里用并发系统做什么吗？在这里，我们对它们进行建模，并提取它们的不变量。首先是一些设置定义。在 CS 或数学论文中，如果你把“第 2 部分：模型和问题”写得足够好，论文的其余部分就会自然而然地写出来。通过此设置，您可以看到将要执行的操作。事实上，忘记行动。让我们看看一些不变量。不变量 当导出不变量时，我们会问：什么必须始终为真？我发现将安全不变量分为两个阵营很有用：状态不变量（是单个状态上的谓词）和转换不变量（这是一个步骤上的谓词）。转换不变量不像状态不变量那样常用，但它们非常有用，特别是当您推理系统的转换时。状态不变量 TypeOK 表示每个变量都位于正确的空间中。这很无聊，但它发现的错误比我愿意承认的还要多。 OneKingPerColor 和 BothKingsOnBoard 也是健全性检查。 TurnParity 是第一个有趣的。它将两个状态变量联系在一起：白方走偶数步，黑方走奇数步。 MakeMove 操作满足此 TurnParity 。 PreviousPlayerNotInCheck 重申了“你必须在未受控制的情况下结束回合”的规则，即“回头看：刚刚移动的玩家未处于受控制状态”。 NotBothInCheck 是一个推论。转换不变量 这些是对 <> 对的谓词，用括号形式编写： [][P]_vars 。它们表达了事物如何随着约束而变化。表示法很简单：x是变量x在这个状态下的值，x'表示下一个状态下的值。 MoveCountStrictlyIncreases 和 TurnAlternates 表示每个步骤都会随着颜色翻转而增加移动计数。如果过渡把事情搞砸了，那就是出了问题。 PieceCountNonIncreasing 排除了凭空出现的碎片。 SingleCapturePerMove 加强了这一点：每一步最多消失一个片段。 ExactlyTwoSquaresChange 是这里最强的。它说每次移动都会改变两个方格，源（现在是空的）和目的地（现在持有移动的棋子）。哈哈，是的，这只是基本国际象棋规则的模型。这里一个有用的练习是考虑当我们添加易位、兵、过路人时，哪些不变量仍然存在？当我们添加王位易位时，ExactlyTwoSquaresChange 就被违反了：一步棋中有四个方格发生变化。同样，en passant 吃掉了不在目标方格上的棋子，因此三个方格发生变化。 PieceCountNonIncreasing 在 pawn 提升后继续存在（当 pawn 成为皇后时，计数不变）。抽象 tla 获取链接 Facebook X Pinterest 电子邮件 其他应用程序 评论 匿名者说...您是否使用过任何验证工具（TLC、Apalache、TLAPS，...）来推断当我们添加易位、典当等时，哪些不变量仍然存在？ 2026 年 5 月 21 日上午 9:38 发表评论