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

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-algorithm-correctness/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-algorithm-correctness-01 · production-20261019-adopted-96



## 目標與範圍

在有限狀態模型 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。





## 逐步主鏈

S01 · definition操作前

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

條件：無

規則：def_intro · 依賴：G1

葉節點依據：def_intro + subset_def + cartesian_product_def + finite_counting_basics

確認 M 是 MKO 意義下的有限模型。321 與 123 都在 S 中。交換一個排列的兩項，所得仍是 1、2、3 的排列，所以每條邊的兩端都在 S 中，Step⊆S×S。S 恰有 3!=6 個元素。123 沒有相鄰逆序對，所以本來就沒有外出邊，與「Halt 為終點」一致。



S02 · definition操作前

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}

條件：無

規則：def_unfold · 依賴：G2, G4, mko_algorithm_correctness_def

葉節點依據：def_unfold + mko_algorithm_correctness_def

依 MKO 的部分正確／總正確區分寫出責任，並把終止性精確量化於極大執行。PC：從 Init 出發、到達 Halt 的每條執行，其末狀態滿足 Q。T：從 Init 出發的每條極大執行都有限且末狀態屬於 Halt，等價於沒有無窮執行，也沒有停在非 Halt 狀態的有限極大執行。有限非極大前綴不要求已到 Halt。TC 是 PC 與 T 的合取，所有非確定選擇都必須涵蓋（G4）。



S03 · theorem_application操作前

s\in S\setminus\mathrm{Halt}

操作後

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

條件：無

規則：L_succ · 依賴：G1

葉節點依據：contrapositive + order_basics

套用引理 L_succ（在 S03.1、S03.2 證明）：不在 Halt 的狀態一定有相鄰逆序對，因此有後繼，不會卡住。這是終止性論證中排除「卡住」的部分。



S04 · definition操作前

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

條件：無

規則：def_intro · 依賴：G1

葉節點依據：def_intro + numeric_evaluation

定義排名函數 inv(s)：位置對 (i,j)、i<j 中 x_i>x_j 的個數。它是三個 0 或 1 的和，所以是 0 到 3 的自然數。逐一計算六個狀態的值（N2 到 N7 可重算）。



S05 · theorem_application操作前

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

操作後

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

條件：無

規則：L_rank · 依賴：S04, G1

葉節點依據：def_unfold + add_comm + numeric_evaluation

套用引理 L_rank（在 S05.1、S05.2 對兩種交換分別證明）：每一步都使逆序數恰好減 1。這是對每一種邊的證明，不是只在幾個樣本狀態上觀察。



S06 · induction_base操作前

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

操作後

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

條件：無

規則：nat_induction · 依賴：S04, G1

葉節點依據：nat_induction + numeric_evaluation

考慮任意一條執行 (t_k)。t0∈Init={321}，所以 inv(t0)=3。這是不變量 inv(t_k)=3−k 的歸納基底（k=0）。



S07 · induction_step操作前

\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)

條件：無

規則：nat_induction · 依賴：S06, S05

葉節點依據：nat_induction + eq_replace + add_assoc

設 inv(t_k)=3−k，且執行還有下一步 t_{k+1}。依 L_rank，inv(t_{k+1})=inv(t_k)−1=(3−k)−1=3−(k+1)。所以對執行中的每個索引 k，都有 inv(t_k)=3−k。不變量對每一步都證明了保持，不論在非確定的分岔中選了哪一條邊。



S08 · implies操作前

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

操作後

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

條件：無

規則：order_basics · 依賴：S07, S04

葉節點依據：order_basics + nat_induction

inv 的值不小於 0，所以執行中任何索引 k 都滿足 3−k≥0，即 k≤3。因此每條執行至多有 4 個狀態、3 步，不存在無窮執行。這是排名函數論證：一個非負整數值每步嚴格下降，不能無限下降。



S09 · implies操作前

\text{every execution is finite}

操作後

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

條件：無

規則：contrapositive · 依賴：S08, S03

葉節點依據：contrapositive + mko_computational_model_def

由 S08，每條執行有限；只要末狀態還有後繼就可以延長，延長至多到 3 步，所以每條執行都可延伸成極大執行，其末狀態沒有後繼。依 L_succ 的逆否（S03），沒有後繼的狀態必在 Halt。所以每條從 Init 出發的極大執行都有限並以 Halt 結束；每條有限前綴亦可延伸到這樣的停止執行。依 S02，終止性 T 成立。



S10 · implies操作前

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

操作後

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

條件：無

規則：mko_algorithm_correctness_def · 依賴：S01, G1, G2

葉節點依據：mko_algorithm_correctness_def + order_basics

任何到達 Halt 的執行，末狀態都是 123。123 遞增，而且其項目是輸入 321 的項目的重排（S01：每個狀態都是 1、2、3 的排列，交換不改變項目）。所以 Q 在每個可到達的停止狀態成立，部分正確性 PC 成立。



S11 · implies操作前

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

操作後

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

條件：無

規則：and_intro_elim · 依賴：S09, S10, S02

葉節點依據：and_intro_elim + mko_algorithm_correctness_def

合取 S10 的 PC 與 S09 的 T，依 S02 的定義得總正確性：從 321 出發的每條極大執行都終止，且終止時輸出遞增的重排 123。



S12 · implies操作前

\text{reachable graph from}\ 321

操作後

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

條件：無

規則：mko_computational_model_def · 依賴：G1, S11

葉節點依據：mko_computational_model_def + case_analysis

有限模型可用完整可達圖交叉核對。321 有兩個後繼：交換前兩項得 231，交換後兩項得 312。231 只有後兩項逆序，得 213；312 只有前兩項逆序，得 132；213 得 123；132 得 123。所以恰有兩條極大執行，各 3 步，等於 inv(321)，都停在 123。這與 S07 到 S11 一致；但一般性證明來自 S05 到 S10，不依賴這張圖。



S13 · implies操作前

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'

條件：無

規則：quantifier_negation · 依賴：G3, S02

葉節點依據：quantifier_negation + case_analysis + mko_algorithm_correctness_def

在 M′ 中，成功路徑 321→231→213→123 仍存在，而且 Halt 仍是 {123}，所以 PC 照樣成立。但 M′ 允許交換非逆序對：321 交換前兩項得 231，231 交換前兩項又回到 321，兩者都不在 Halt。序列 t_{2k}=321、t_{2k+1}=231 是合法的無窮執行，T 不成立，TC 不成立。一條成功路徑與 PC 都不足以得到總正確（MKO 誤解）。



S14 · implies操作前

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''

條件：無

規則：quantifier_negation · 依賴：G3, G2, S02

葉節點依據：quantifier_negation + mko_algorithm_correctness_def

在 M″ 中，從 321 出發的極大執行只有兩條：321→231（231 的 2<3，屬於 Halt″，停止）與 321→312→132（132 屬於 Halt″，停止）。兩條都停止，所以 T 成立；但停止狀態 231 不遞增（3>1），Q(231) 為假，PC 不成立，TC 也不成立。終止本身不保證正確。







## 局部子步與引理

S03.1 · implies操作前

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

操作後

x_1<x_2<x_3

條件：x_1,x_2,x_3\ \text{distinct}

規則：order_basics · 依賴：order_basics, contrapositive

葉節點依據：order_basics + contrapositive

改證逆否命題：若沒有相鄰逆序對，則 s∈Halt。排列的三項互不相同，依三分律「不是 x1>x2」且 x1≠x2 給出 x1<x2；同理 x2<x3。所以 x1<x2<x3。



S03.2 · implies操作前

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}

條件：無

規則：order_basics · 依賴：S03.1, order_basics

葉節點依據：order_basics + contrapositive

x1 小於另外兩項（x1<x2，且依傳遞 x1<x3），所以 x1 是 {1,2,3} 的最小元 1；x3 大於另外兩項，所以 x3=3；剩下 x2=2。因此 s=123∈Halt。S03.1 與 S03.2 合起來，以逆否方式證得 L_succ。



S05.1 · implies操作前

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_1>x_2

規則：def_unfold · 依賴：S04, G1

葉節點依據：def_unfold + add_comm + order_basics

交換前兩項：inv(s′)=[x2>x1]+[x2>x3]+[x1>x3]。因 x1>x2，[x2>x1]=0。而 inv(s)=[x1>x2]+[x1>x3]+[x2>x3]=1+[x1>x3]+[x2>x3]。其餘兩項只是交換了位置（加法交換律），所以 inv(s′)=inv(s)−1。



S05.2 · implies操作前

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

條件：x_2>x_3

規則：def_unfold · 依賴：S04, G1

葉節點依據：def_unfold + add_comm + order_basics + case_analysis

交換後兩項：inv(s′)=[x1>x3]+[x1>x2]+[x3>x2]。因 x2>x3，[x3>x2]=0，而 inv(s)=[x1>x2]+[x1>x3]+1。所以 inv(s′)=inv(s)−1。S05.1 與 S05.2 涵蓋 M 的兩種邊，證得 L_rank。







## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-algorithm-correctness-01.json)