第六章：狀態機
狀態機 是一個簡單的數學模型，用於描述系統如何從一種狀態轉移到另一種狀態。它是分析演算法和系統行為的有力工具。
6.1 狀態與轉移
一個狀態機由以下三部分組成：
- 狀態： 系統可能處於的所有情況。
- 起始狀態： 系統開始時的狀態。
- 轉移規則： 定義如何從一個狀態移動到下一個狀態的規則。
狀態機可以被視為一個有向圖，其中節點代表狀態，邊代表轉移。
6.2 不變量原理
不變量： 一個關於系統狀態的性質，如果在起始狀態為真，且在每一次轉移後都保持為真，則該性質稱為不變量。
不變量原理： 如果一個性質是不變量，那麼無論系統運行多久，該性質在所有可達狀態下都為真。
🧪 互動挑戰：機器人迷宮（不變量證明）
一個機器人從座標 (0, 0) 出發。它只能執行兩種移動：
A: 右移 1 格，上移 2 格 (+1, +2)。
B: 右移 2 格，上移 1 格 (+2, +1)。
挑戰： 請試著到達目標點 (1, 1)。
🔍 觀察任務： 每次移動後，注意右側黃框中「(X+Y) mod 3」的數值。
它會改變嗎？出發點 (0,0) 的值是 0，目標點 (1,1) 的值是 2。
🤖
當前狀態
X: 0
Y: 0
(X + Y) % 3 = 0
6.3 部分正確性與終止性
在驗證程式時，我們通常關心兩件事：
- 部分正確性： "如果程式結束，那麼結果是正確的。"（這通常使用不變量來證明）。
- 終止性： "程式最終一定會結束。"
證明終止性：派生序列
證明終止性的一個標準方法是找到一個自然數值的函數，該函數在每一步都嚴格遞減。
State
➡️
f(n)
➡️
f(n-1)
...
0 (結束)
因為自然數集是良序的（沒有無限遞減序列），所以狀態機最終必須停止。
🧪 互動：穩定婚姻 — Gale-Shapley 演算法
3 個男生（M1,M2,M3）和 3 個女生（W1,W2,W3）的穩定婚姻問題。每按一次「執行一輪」，模擬一輪求婚過程。
不變量：一旦女生有了求婚者，她始終有求婚者，且不會變差。
偏好順序：
M1 偏好：W1 > W2 > W3 W1 偏好：M2 > M1 > M3
M2 偏好：W2 > W1 > W3 W2 偏好：M1 > M2 > M3
M3 偏好：W1 > W3 > W2 W3 偏好：M1 > M2 > M3
M1 偏好：W1 > W2 > W3 W1 偏好：M2 > M1 > M3
M2 偏好：W2 > W1 > W3 W2 偏好：M1 > M2 > M3
M3 偏好：W1 > W3 > W2 W3 偏好：M1 > M2 > M3
準備開始…按「執行一輪求婚」開始模擬。
教材來源：Mathematics for Computer Science (Lehman, Leighton, Meyer)