算法正確性：非確定性相鄰交換排序的部分正確、終止與總正確

目標與範圍

在有限狀態模型 M 中，狀態是 (1,2,3) 的六個排列，初始狀態 (3,2,1)，每步可非確定性地交換任一個相鄰逆序對，Halt={(1,2,3)}。以後置條件「遞增排列且為輸入的重排」證明 M 的部分正確性、終止性與總正確性：用排名函數 inv（逆序數）證明每條執行至多 3 步，且每條極大執行停在 Halt。再以變體 M′（允許交換任何相鄰對）說明一條成功路徑與部分正確都不足以得到總正確，以變體 M″（錯誤的停止條件）說明終止不足以得到正確。

在 MKO 範圍內工作：使用前一條目的有限狀態模型，Halt 狀態為執行終點（假設 a1）；模型非確定性，責任針對所有可能執行（假設 a2）。不處理 Hoare 邏輯的一般規則、公平性或實際程式語言語義，不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• nat_induction
• finite_counting_basics
• numeric_evaluation

• G1 — 模型 M=(S,Init,Step,Halt)：S 是 (1,2,3) 的六個排列 123、132、213、231、312、321；Init={321}；對 s=(x1,x2,x3)∉Halt，若 x1>x2 則有邊 s→(x2,x1,x3)，若 x2>x3 則有邊 s→(x1,x3,x2)；Halt={123}，停止狀態沒有外出邊（MKO 假設 a1）。
• G2 — 後置條件 Q(s)：s 的三項遞增（x1<x2<x3），且其項目恰是輸入 321 的項目 {1,2,3} 的重排。前置條件：初始狀態屬於 Init。
• G3 — 變體 M′：S、Init、Halt 同 M，但對 s∉Halt，任一相鄰對都可交換，不論是否逆序。變體 M″：S、Init 與交換規則同 M（只交換相鄰逆序對），但 Halt″={s∈S ∣ x1<x2}，並截斷 Halt″ 的外出邊。
• G4 — M 是非確定性的：所有責任都針對從 Init 出發的每一條可能執行，一條成功路徑不足以證明（MKO 假設 a2）。 這裡終止性量化於極大執行（無窮執行亦算極大）；有限但未極大的執行只是可繼續延伸的前綴，不要求前綴本身已到達 Halt。

• s=(x_1,x_2,x_3) — 狀態：1、2、3 的一個排列，簡寫為 x1x2x3，例如 321
• Q(s) — 後置條件：遞增且為輸入的重排
• \mathrm{inv}(s) — 逆序數 [x1>x2]+[x1>x3]+[x2>x3]
• [P] — P 為真時取 1，否則取 0
• \mathrm{PC},\ \mathrm{T},\ \mathrm{TC} — 部分正確、終止、總正確
• M',\ M'' — 兩個對照變體

規則與來源

• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• mko_algorithm_correctness_def · cited — 相對初始條件與後置條件，部分正確性表示每個從合法初始狀態到達的停止狀態都滿足後置條件；終止性表示每個合法執行最終到達停止狀態；總正確性是兩者的合取。 · mko-algorithm-correctness
• mko_computational_model_def · cited — 有限抽象模型 (S,Init,Step,Halt)，Init,Halt⊆S、Step⊆S×S；執行從 Init 開始沿 Step 前進，進入 Halt 即結束；無後繼的狀態不因而自動屬於 Halt。 · mko-computational-model
• L_succ · lemma — 在 M 中，每個 s∈S∖Halt 都至少有一個相鄰逆序對，因此至少有一個 Step 後繼。
• L_rank · lemma — 在 M 中，若 (s,s′)∈Step，則 inv(s′)=inv(s)−1。

逐步主鏈

S=\{123,132,213,231,312,321\},\ \mathrm{Init}=\{321\},\ \mathrm{Halt}=\{123\}

\mathrm{Init},\mathrm{Halt}\subseteq S,\ \mathrm{Step}\subseteq S\times S,\ |S|=3!=6

M,\ Q

\mathrm{PC}:\ \text{every halt reached satisfies}\ Q;\quad \mathrm{T}:\ \text{every maximal execution is finite and ends in Halt};\quad \mathrm{TC}=\mathrm{PC}\wedge\mathrm{T}

s\in S\setminus\mathrm{Halt}

x_1>x_2\ \vee\ x_2>x_3,\ \text{so}\ \mathrm{Post}(s)\ne\varnothing

s=(x_1,x_2,x_3)

\mathrm{inv}(s)=[x_1>x_2]+[x_1>x_3]+[x_2>x_3]\ge 0;\ \mathrm{inv}(321)=3,\ \mathrm{inv}(231)=\mathrm{inv}(312)=2,\ \mathrm{inv}(213)=\mathrm{inv}(132)=1,\ \mathrm{inv}(123)=0

(s,s')\in\mathrm{Step}

\mathrm{inv}(s')=\mathrm{inv}(s)-1

(t_k)\ \text{an execution of}\ M,\ t_0\in\mathrm{Init}

\mathrm{inv}(t_0)=\mathrm{inv}(321)=3

\mathrm{inv}(t_k)=3-k,\ (t_k,t_{k+1})\in\mathrm{Step}

\mathrm{inv}(t_{k+1})=(3-k)-1=3-(k+1)

\mathrm{inv}(t_k)=3-k\ge 0

k\le 3:\ \text{every execution has at most 3 steps; no infinite execution}

\text{every execution is finite}

\text{every maximal execution ends in Halt:}\ \mathrm{T}

t_{\mathrm{last}}\in\mathrm{Halt}=\{123\}

Q(123):\ 1<2<3\ \wedge\ \{1,2,3\}=\{1,2,3\}\ \Rightarrow\ \mathrm{PC}

\mathrm{PC},\ \mathrm{T}

\mathrm{TC}=\mathrm{PC}\wedge\mathrm{T}\ \text{holds for}\ M

\text{reachable graph from}\ 321

321\to 231\to 213\to 123,\quad 321\to 312\to 132\to 123

M':\ 321\to 231\to 213\to 123\ \text{exists}

t_{2k}=321,\ t_{2k+1}=231\ \text{is infinite}\ \Rightarrow\ \neg\mathrm{T},\ \neg\mathrm{TC}\ \text{for}\ M'

M'':\ \mathrm{Halt}''=\{s\mid x_1<x_2\}=\{123,132,231\}

321\to 231\in\mathrm{Halt}'',\ \neg Q(231)\ \Rightarrow\ \neg\mathrm{PC},\ \neg\mathrm{TC}\ \text{for}\ M''

局部子步與引理

\neg(x_1>x_2)\ \wedge\ \neg(x_2>x_3)

x_1<x_2<x_3

x_1<x_2<x_3,\ \{x_1,x_2,x_3\}=\{1,2,3\}

(x_1,x_2,x_3)=(1,2,3)\in\mathrm{Halt}

x_1>x_2,\ s'=(x_2,x_1,x_3)

\mathrm{inv}(s')=0+[x_2>x_3]+[x_1>x_3]=\mathrm{inv}(s)-1

x_2>x_3,\ s'=(x_1,x_3,x_2)

\mathrm{inv}(s')=[x_1>x_3]+[x_1>x_2]+0=\mathrm{inv}(s)-1

逐步反向審查

• S14 · premise_audit · G3, G2, quantifier_negation — 否定 PC 只需一個到達的停止狀態不滿足 Q；T 的判定來自兩條極大執行的完整列舉。
• S13 · premise_audit · G3, S02, quantifier_negation — 一條無窮執行就否定全稱的 T。索引分偶數與奇數兩種，涵蓋所有 n≥0；交替的兩條邊 321→231 與 231→321 都是 M′ 的邊。
• S12 · premise_audit · G1, mko_computational_model_def — 可達圖必須從每個可達狀態列出全部後繼才算完整；這裡六個狀態都已處理。
• S11 · sufficient_goal_reduction · S02, S09, S10, and_intro_elim — 目標 TC；依定義足夠且必要的是 PC 與 T，兩者都由前面步驟正向證得，沒有把 TC 當前提。
• S10 · premise_audit · S01, G2, mko_algorithm_correctness_def — PC 只談到達的停止狀態；它不推出 T，T 由 S09 另外證明。
• S09 · premise_audit · S08, S03, contrapositive — T 需要兩件事：沒有無窮執行（S08）且沒有卡住（S03）；缺一不可。
• S08 · premise_audit · S07, S04, order_basics — 需要 inv≥0 與每步恰減 1。只排除無窮執行；是否停在 Halt 由 S09 處理。
• S07 · premise_audit · S06, S05, nat_induction — 歸納步用到 L_rank 對所有邊成立；算術恆等式由 N8 作一次多項式核對。
• S06 · premise_audit · S04, G1, nat_induction — 不變量在初始狀態成立；保持性在 S07。
• S05.2 · premise_audit · S04, def_unfold, add_comm, case_analysis — M 的邊只有這兩種，所以兩個情況窮盡。
• S05.1 · premise_audit · S04, def_unfold, add_comm — 需要條件 x1>x2，這正是 M 允許此交換的條件。
• S05 · premise_audit · L_rank, S04 — 引理依賴「只交換逆序對」；在 M′ 中交換非逆序對會使 inv 增加，引理不適用。
• S04 · premise_audit · def_intro, numeric_evaluation — 此步只定義與計算，不推出執行性質；inv≥0 由定義直接得到。
• S03.2 · premise_audit · S03.1, order_basics — 需要 s 是 1、2、3 的排列（S01）。
• S03.1 · premise_audit · order_basics, contrapositive — 需要三項互異；若允許重複值，「不大於」只能得「小於或等於」。
• S03 · premise_audit · L_succ, G1 — 只對 M 的交換規則成立；在 M″ 中某些非 Halt 狀態的情況需另外檢查。
• S02 · premise_audit · mko_algorithm_correctness_def, G4 — 此步只展開定義。PC 本身不要求任何執行停止，所以單獨的 PC 可能空真成立。
• S01 · premise_audit · G1, mko_computational_model_def, finite_counting_basics — 此步只檢查資料構成模型；「交換保持排列」也就是後置條件中「為輸入的重排」那一半的來源（N1 重算 3!）。

錯誤控制與反例

一條成功路徑不是總正確

MKO 指出的誤解是把一條成功 trace 或「輸出正確但可能不停」當成總正確。M′ 有成功路徑 321→231→213→123，PC 也成立，卻有無窮執行（S13）。非確定性模型的責任針對所有執行（MKO 假設 a2）。

部分正確可以空真成立

PC 只要求「到達的停止狀態」滿足 Q。一個永不停止的模型（例如只有邊 321→321 而 Halt 不可達）沒有任何停止狀態可檢查，PC 空真成立，但 T 不成立。所以 PC 不能冒充 TC（MKO 第二段）。

不變量要對每一步證明

「inv 每步減 1」在 S05 對 M 的兩種邊都證明了。若只在樣本轉移上觀察，例如在 M′ 中看到 321→231 使 inv 由 3 變 2，就會漏掉 231→321 使 inv 由 2 變 3 的邊。初始成立加上逐步保持才是證明（MKO 第一段）。

• M′ 有成功路徑 321→231→213→123，所以 M′ 總正確 → reject — M′ 有無窮執行 321→231→321→231 不斷交替，T 不成立。
• M′ 部分正確，所以 M′ 終止 → reject — PC 不含終止；M′ 的 PC 成立而 T 不成立。
• M″ 的每條執行都停止，所以 M″ 總正確 → reject — M″ 會停在 231，它不是遞增排列，PC 不成立。
• 永不停止的程式不是部分正確的 → reject — 沒有到達任何停止狀態時，PC 空真成立；它不是總正確，但是部分正確。

結論與限制

對 M：每步使逆序數恰減 1，所以每條執行至多 3 步；非 Halt 狀態都有後繼，所以每條極大執行停在 123；123 滿足後置條件。故 M 部分正確、終止、總正確；可達圖恰有兩條極大執行，各 3 步。M′ 部分正確且有成功路徑，但有無窮執行 321↔231，不是總正確；M″ 終止，但停在未排序的 231，不是部分正確。

• Hoare 式規格、一般的排名函數方法、非確定性公平性與實際程式語義的橋接（MKO formal next）未在此建立；本稿只處理一個明示的有限模型。

驗證及來源綁定

8 個本稿宣告算術檢查；只支持所列算式。

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 9ce0cffb4623aaaff23ae8c54c93395ecd56ec9621219ba8168ae49c7873d238
• original source SHA-256: 9ce0cffb4623aaaff23ae8c54c93395ecd56ec9621219ba8168ae49c7873d238
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）