象棋建模：不變量與狀態轉移的複雜性

象棋常被視為一種簡單的策略遊戲，但從軟體工程和形式驗證的角度來看，它簡直是邊際情況（edge cases）的噩夢。當嘗試對遊戲規則進行形式化建模時——特別是使用像 TLA+ 這樣的工具——其複雜性並非源於棋盤的幾何結構，而是源於在每一步移動中都必須維持的一套錯綜複雜的不變量（invariants）。

形式化建模需要對何謂「合法」狀態進行嚴謹的定義。在象棋中，這不僅僅涉及確保棋子位於正確的位置；它還需要追蹤移動歷史以驗證特定動作，並確保任何移動都不會導致國王處於非法狀態。

狀態與轉移不變量

形式化建模的核心在於區分狀態不變量（state invariants）與轉移不變量（transition invariants）。狀態不變量是一個對於遊戲中每一個有效狀態都必須成立的謂詞（predicate）。例如，象棋中一個基本的狀態不變量是：棋盤上任何時候都必須恰好有一個各色國王。

然而，轉移不變量則更為複雜。它們是針對一對狀態的謂詞：當前狀態與下一個狀態。它們定義了移動與吃子的規則。轉移不變量不是問「這個棋盤配置是否合法？」，而是問「根據遊戲規則，從狀態 A 到狀態 B 的移動是否合法？」。

這種區別至關重要，因為某些規則無法用簡單的狀態屬性來表達。例如，「吃過路兵」（en passant）規則完全取決於對手前一步所做的移動。如果沒有追蹤轉移過程，單憑棋盤狀態本身不足以判斷吃過路兵是否合法。

象棋規則的「隱藏」複雜性

許多開發者低估了實現象棋規則的難度，因為他們將其視為一系列簡單的移動。然而，遊戲中充滿了會使狀態機變得複雜的規則：

• 王車易位 (Castling)： 需要知道國王或車是否曾經移動過，這為遊戲增加了「隱藏」狀態。
• 吃過路兵 (En Passant)： 一種僅存在於一回合內的瞬時機會，需要特定的轉移歷史。
• 兵的升變 (Pawn Promotion)： 一種狀態變更，在到達特定座標時將一種棋子類型轉換為另一種。
• 逼和 (Stalemate)： 一種僵局條件，輪到該玩家移動時，其沒有任何合法移動，但並非處於被將軍的狀態。

正如一位評論者所指出的，這種複雜性使得即使是經驗豐富的開發者也能在這些挑戰與現實世界的系統整合之間找到相似之處。在建模一個擁有 1,500 年歷史的遊戲時，為了不「因法國兵法規則而哭泣」而奮鬥，提醒了我們：即使在現代的 CRUD 應用程式和計費整合中，狀態不變量違規的情況也屢見不見。

行為建模與數據建模

在如何處理這些問題上，存在著顯著的哲學分歧。有些人認為，當目標是表達行為時，專注於數據（狀態）並非正確的方法。

我發現專注於行為要有用得多，因此與其思考狀態轉移，不如專注於程式允許執行什麼，而不論底層的數據結構為何。

從這個角度來看，程式碼應該明確說明棋子為什麼不能移動，而不是僅僅計算狀態轉移在數學上是否可能。這種從「以數據為中心」到「以行為為中心」的建模轉向，可以使邏輯對人類來說更直觀、更易於閱讀與維護，即使它不太適合像 TLA+ 這樣的形式化驗證工具。

實作觀點

對於那些希望在程式碼中實現這些規則的人來說，函數式編程提供了一條引人注目的路徑。透過將規則建模為一系列轉換——擴展可能的移動、捨棄非法的移動、並完成吃子動作——系統會變得高度可擴展。這種方法允許輕鬆地添加新的棋子類型或自定義規則，而無需重寫核心引擎，將遊戲視為一系列經過篩選的可能移動集合，而非硬編碼的一系列 if-else 語句。