derivation-mko-computational-model-01 · production-20261019-adopted-96
給定有限模型 (S,Init,Step,Halt)：S={s0,s1,s2,s3,s4,s5,s6}，Init={s0}，Halt={s3}，原始邊資料 {(s0,s1),(s0,s2),(s1,s3),(s1,s5),(s2,s4),(s4,s2),(s3,s6)}。依 MKO 規則截斷停止狀態的外出邊，以不動點迭代算出可達集，找出停止狀態、卡住狀態與可達循環，給出合法的停止、卡住與無窮執行，排除三條不合法的 trace，並說明為何尚未窮盡可達圖的有限深度探索，不能僅憑未見反例就斷言所有極大執行終止。
在 MKO 範圍內工作：S 是明示有限狀態集，Step 是可具非確定性的有向關係（假設 a1）；到達 Halt 即停止，分析前截斷其外出邊（假設 a2）。不處理有效編碼、公平性或確定性與非確定性模型的分層，不改動 canonical MKO 或英文 edition。
set_operations_defcartesian_product_defsubset_defnat_inductionfinite_counting_basicsG1 — S={s0,s1,s2,s3,s4,s5,s6}，Init={s0}，Halt={s3}（MKO 假設 a1：S 明示有限）。G2 — 原始邊資料 E_raw={(s0,s1),(s0,s2),(s1,s3),(s1,s5),(s2,s4),(s4,s2),(s3,s6)}。G3 — 執行約定（MKO 假設 a2 與第二段）：分析前刪去所有從 Halt 狀態出發的邊，得到 Step。執行是以 ℕ 的一個起始段（有限或全部 ℕ）為索引的狀態序列 (t_i)，t_0∈Init，相鄰兩項 (t_i,t_{i+1})∈Step；進入 Halt 即結束。有限執行若末狀態沒有 Step 後繼則稱為極大；有限極大執行的末狀態在 Halt 中稱為停止，不在 Halt 中稱為卡住；無窮執行也視為極大。可延伸的有限前綴仍是合法執行，但不能因尚未到 Halt 就當成全域終止性的反例；全域終止性以下量化從 Init 出發的極大執行。S — 狀態集 {s0,s1,s2,s3,s4,s5,s6}\mathrm{Init},\ \mathrm{Halt} — 初始狀態集與停止狀態集E_{\mathrm{raw}} — 原始邊資料\mathrm{Step} — 截斷後的轉移關係\mathrm{Post}(s) — s 的後繼集 Step[{s}]R_k — 第 k 輪可達集（至多 k 步）\mathrm{Reach} — 從 Init 可達的狀態集set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。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 — 明確整數或有理數算式的精確求值；可以獨立重算。set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。mko_computational_model_def · cited — 本條目的有限抽象模型為 (S,Init,Step,Halt)，其中 Init,Halt⊆S、Step⊆S×S。執行從 Init 中狀態開始並沿 Step 前進；無後繼的 stuck 狀態不因而自動屬於 Halt。 · mko-computational-modelmko_relation_def · cited — 從 A 到 B 的二元關係 R 是 A×B 的子集合；關係像 R[C]={y∈B:存在 x∈C，使 (x,y)∈R}。 · mko-relationreach_def · prerequisite — 可達性：狀態 s 從 Init 可達，若存在 k≥0 與狀態 u_0,u_1 到 u_k 的有限路徑，u_0∈Init、u_k=s，且每對相鄰狀態都在 Step 中（k=0 表示零步，即 s∈Init）。Reach 是所有可達狀態的集合。L_fix · lemma — 令 R_0=Init，R_{k+1}=R_k∪Step[R_k]。則 (i) 對每個 k，R_k 恰是至多 k 步可達的狀態集；(ii) 若某個 m 使 R_{m+1}=R_m，則 Reach=R_m。操作前
\mathrm{Init}=\{s_0\},\ \mathrm{Halt}=\{s_3\},\ E_{\mathrm{raw}}操作後
\mathrm{Init},\mathrm{Halt}\subseteq S,\ E_{\mathrm{raw}}\subseteq S\times S條件：無
規則：subset_def · 依賴：G1, G2
葉節點依據：subset_def + cartesian_product_def + mko_computational_model_def
先檢查資料是否構成 MKO 的模型：s0 與 s3 都在 S 中，所以 Init、Halt⊆S；E_raw 的七個有序對，兩個分量都在 S 中，所以 E_raw⊆S×S。有序對保留方向，例如 (s2,s4) 與 (s4,s2) 是兩條不同的邊。
操作前
E_{\mathrm{raw}}操作後
\mathrm{Step}=E_{\mathrm{raw}}\setminus\{(s_3,s_6)\}=\{(s_0,s_1),(s_0,s_2),(s_1,s_3),(s_1,s_5),(s_2,s_4),(s_4,s_2)\}條件：\mathrm{Halt}=\{s_3\}
規則：set_operations_def · 依賴：S01, G3
葉節點依據：set_operations_def + numeric_evaluation
依 MKO 假設 a2，刪去所有從 Halt 狀態出發的邊。七條邊中只有 (s3,s6) 的起點 s3∈Halt，刪去後剩 6 條。資料中雖有 (s3,s6)，但模型規定到達 s3 即停止，這條邊不屬於執行語義。
操作前
\mathrm{Post}(s)=\mathrm{Step}[\{s\}]操作後
\mathrm{Post}:\ s_0\mapsto\{s_1,s_2\},\ s_1\mapsto\{s_3,s_5\},\ s_2\mapsto\{s_4\},\ s_4\mapsto\{s_2\},\ s_3,s_5,s_6\mapsto\varnothing條件：無
規則：mko_relation_def · 依賴：S02, mko_relation_def
葉節點依據：mko_relation_def + set_builder
對每個狀態收集 Step 中以它為起點的邊的終點。s0 與 s1 各有兩個後繼，所以模型是非確定性的；s3、s5、s6 沒有後繼。後繼表是之後所有計算的基礎。
操作前
R_0=\mathrm{Init},\ R_{k+1}=R_k\cup\mathrm{Step}[R_k]操作後
R_{m+1}=R_m\ \Rightarrow\ \mathrm{Reach}=R_m條件：S\ \text{finite}
規則：L_fix · 依賴：S03, reach_def
葉節點依據：nat_induction + set_operations_def + reach_def
可達性是從 Init 出發沿 Step 的零步或多步閉包（MKO 第一段）。套用引理 L_fix（在 S04.1、S04.2 證明）：逐輪加入後繼，一旦某輪不再增加，當下的集合就是 Reach。因為 R_k 遞增且都在有限的 S 中，至多 |S|=7 輪後必定停止增加。
操作前
R_0=\{s_0\}操作後
R_1=\{s_0,s_1,s_2\},\ R_2=\{s_0,s_1,s_2,s_3,s_4,s_5\},\ R_3=R_2\ \Rightarrow\ \mathrm{Reach}=R_2條件：無
規則：L_fix · 依賴：S03, S04
葉節點依據：set_operations_def + mko_relation_def + numeric_evaluation
R_1=R_0∪Post(s0)={s0,s1,s2}。R_2=R_1∪Post(s0)∪Post(s1)∪Post(s2)={s0,s1,s2}∪{s1,s2}∪{s3,s5}∪{s4}={s0,s1,s2,s3,s4,s5}。R_3 再加入 Post(s3)=∅、Post(s4)={s2}、Post(s5)=∅，沒有新狀態，R_3=R_2。依 L_fix，Reach=R_2，共 6 個狀態；s6 不可達。
操作前
E_{\mathrm{raw}}[R_2]操作後
s_6\in E_{\mathrm{raw}}[R_2]\ \text{but}\ s_6\notin\mathrm{Reach}條件：無
規則：set_operations_def · 依賴：G2, S05
葉節點依據：set_operations_def + mko_relation_def
對照：若忘記截斷而直接用 E_raw，第 3 輪會因 (s3,s6) 加入 s6，得出「全部 7 個狀態可達」，並把 s3 當成還能繼續走的狀態。這與 MKO 假設 a2 衝突。正確分析中 s6 不可達，s3 是執行的終點。
操作前
\mathrm{Reach}=\{s_0,s_1,s_2,s_3,s_4,s_5\}操作後
\mathrm{Reach}\cap\mathrm{Halt}=\{s_3\},\ \{s\in\mathrm{Reach}\setminus\mathrm{Halt}\mid\mathrm{Post}(s)=\varnothing\}=\{s_5\}條件：無
規則：set_builder · 依賴：S03, S05, G1
葉節點依據：set_builder + mko_computational_model_def
可達狀態中，在 Halt 裡的只有 s3。不在 Halt 中又沒有後繼的只有 s5：它是卡住狀態。s3 也沒有後繼，但它在 Halt 中，所以是停止，不是卡住；反過來，s5 沒有後繼並不使它成為停止狀態（MKO 敘述）。s0、s1、s2、s4 都有後繼。
操作前
(s_0,s_1,s_3)
操作後
\text{legal execution that halts at}\ s_3條件：無
規則：mko_computational_model_def · 依賴：G3, S02
葉節點依據：mko_computational_model_def + exists_intro
檢查 trace (s0,s1,s3)：首狀態 s0∈Init；(s0,s1)、(s1,s3)∈Step；末狀態 s3∈Halt，執行在此結束。這是一條合法的停止執行。
操作前
(s_0,s_1,s_5)
操作後
\text{legal maximal execution, stuck at}\ s_5\notin\mathrm{Halt}條件：無
規則：mko_computational_model_def · 依賴：G3, S02, S07
葉節點依據：mko_computational_model_def + exists_intro
(s0,s1,s5)：s0∈Init，(s0,s1)、(s1,s5)∈Step，所以合法；Post(s5)=∅，無法繼續，所以是極大執行；s5∉Halt，所以它卡住而沒有停止。
操作前
t_0=s_0,\ t_{2k+1}=s_2,\ t_{2k+2}=s_4\ (k\ge 0)操作後
\forall n\ge 0,\ (t_n,t_{n+1})\in\mathrm{Step},\ t_n\notin\mathrm{Halt}條件：無
規則：case_analysis · 依賴：G3, S02, G1
葉節點依據：case_analysis + nat_induction + mko_computational_model_def
定義以全部 ℕ 為索引的序列：t0=s0，奇數位 t_{2k+1}=s2，正偶數位 t_{2k+2}=s4。對每個 n 分三種情況檢查相鄰對：n=0 時 (s0,s2)∈Step；n=2k+1 時 (t_n,t_{n+1})=(s2,s4)∈Step；n=2k+2 時 n+1=2(k+1)+1，所以 t_{n+1}=s2，(s4,s2)∈Step。三種情況涵蓋所有 n≥0。序列的狀態都在 {s0,s2,s4} 中，與 Halt 不相交，所以執行永不結束：這是一條合法的無窮執行，來自可達的非停止循環 s2→s4→s2。
操作前
(s_0,s_3),\ (s_1,s_3),\ (s_0,s_1,s_3,s_6)
操作後
\text{none is a legal execution}條件：無
規則：mko_computational_model_def · 依賴：G3, S02, G1
葉節點依據：mko_computational_model_def + quantifier_negation
三條不合法的 trace，各違反一個條件：(s0,s3) 中 (s0,s3)∉Step；(s1,s3) 的首狀態 s1∉Init；(s0,s1,s3,s6) 在進入 s3∈Halt 後還繼續，而 (s3,s6) 已被截斷，不在 Step 中（MKO 第二段：進入 Halt 就結束）。
操作前
\text{stuck execution (S09)},\ \text{infinite execution (S10)}操作後
\neg(\text{every maximal execution from Init halts})條件：無
規則：quantifier_negation · 依賴：S09, S10
葉節點依據：quantifier_negation + exists_intro
「每條從 Init 出發的極大執行都停止」是全稱命題。S09 給出一條卡住的有限極大執行，S10 給出一條無窮極大執行；任一個都足以否定它。因此本模型不具全域終止性，儘管 S08 有一條停止執行。可延伸的有限前綴本身不算此全稱命題的反例。
操作前
\text{prefixes of depth}\ 1:\ (s_0,s_1),\ (s_0,s_2)操作後
\text{no cycle or stuck state visible at depth 1, yet termination fails}條件：無
規則：quantifier_negation · 依賴：S03, S12
葉節點依據：quantifier_negation + mko_computational_model_def
只探索深度 1 時，看到的前綴只有 (s0,s1) 與 (s0,s2)，其中尚未顯示循環或卡住狀態。若僅據此斷言「所有極大執行都終止」就錯了：S12 已給出反例。這裡否定的是尚未窮盡可達圖的觀察所作的推論，不是所有有限探索證書；完整探索有限可達圖並檢查循環與非 Halt 的死端，可以支持相應判定。本模型的完整可達圖（S05、S07、S10）揭示了兩種風險。
操作前
R_k
操作後
R_k=\{s\mid s\ \text{reachable in at most}\ k\ \text{steps}\}條件：無
規則：nat_induction · 依賴：reach_def, nat_induction, set_operations_def
葉節點依據：nat_induction + set_operations_def + reach_def + mko_relation_def
對 k 歸納。k=0：零步可達恰是 Init=R_0。設對 k 成立。若 s 至多 k+1 步可達，則要嘛至多 k 步可達（在 R_k），要嘛路徑最後一步從某個至多 k 步可達的 u 走到 s，即 s∈Step[R_k]。反之 R_k 的元素至多 k 步可達，Step[R_k] 的元素由某個 u∈R_k 再走一步，至多 k+1 步可達。所以 R_{k+1} 恰是至多 k+1 步可達的集合，證得 (i)。
操作前
R_{m+1}=R_m操作後
\forall k\ge m,\ R_k=R_m;\ \mathrm{Reach}=\textstyle\bigcup_k R_k=R_m條件：無
規則：nat_induction · 依賴：S04.1, nat_induction
葉節點依據：nat_induction + set_extensionality + set_operations_def
若 R_{m+1}=R_m，則 R_{m+2}=R_{m+1}∪Step[R_{m+1}]=R_m∪Step[R_m]=R_{m+1}=R_m，依歸納對所有 k≥m 都有 R_k=R_m。每個可達狀態都有某個長度 k 的路徑，由 (i) 它在 R_k 中；R_k 遞增，所以它在 R_{max(k,m)}=R_m 中。反之 R_m 的元素都可達。故 Reach=R_m，證得 (ii)。
S13 · premise_audit · S03, S12 — 此步只指出尚未窮盡可達圖的深度受限觀察，不能僅憑未見反例推出所有極大執行終止；不否定完整有限圖證書，也不宣稱一般程式有終止判定法。S12 · premise_audit · S09, S10, quantifier_negation — 否定全稱只需一個反例；這裡有兩種不同性質的反例，分別對應 MKO 第三段的兩種終止性風險。S11 · premise_audit · G3, S02, G1 — 每條 trace 只需指出一個違反的條件即可排除。S10 · premise_audit · G3, S02, case_analysis — 情況劃分必須涵蓋所有 n：0、正奇數、正偶數，三者互斥且窮盡。索引恆等式 (2k+2)+1=2(k+1)+1 由 N5 作一次多項式恆等式核對。S09 · premise_audit · G3, S02, S07 — 卡住的判定需要兩件事：沒有後繼，且不在 Halt。S08 · premise_audit · G3, S02 — 合法性的三個條件逐一檢查。一條停止執行不表示所有執行都停止（非確定性）。S07 · premise_audit · S03, S05, G1, mko_computational_model_def — 分類只用 Halt 的給定列表與後繼表，不由「沒有後繼」推出屬於 Halt。S06 · premise_audit · G2, S02, S05 — 此步只顯示截斷前後結果不同，用來說明 S02 的必要性；不把 E_raw 的結果當作模型的結論。S05 · premise_audit · S03, L_fix — 每輪都使用完整的後繼表；停止判定是集合等式 R_3=R_2（N3、N4 重算大小）。S04.2 · premise_audit · S04.1, nat_induction, set_extensionality — 論證需要 R_k 遞增（由定義 R_{k+1}⊇R_k）與 (i)。S04.1 · premise_audit · reach_def, nat_induction, set_operations_def, mko_relation_def — 兩個包含方向都在歸納步中證明；基底用到零步路徑。S04 · premise_audit · L_fix, reach_def — 停止條件必須是 R_{m+1}=R_m 這個集合等式，不是「某輪沒有看到新的循環」之類的觀察。S03 · premise_audit · S02, mko_relation_def — 六條邊恰好各被歸到其起點一次，2+2+1+1=6 與邊數一致（N2）。S02 · premise_audit · G3, set_operations_def — 需要逐條檢查起點是否在 Halt；N1 重算邊數 7−1=6。S01 · premise_audit · G1, G2, subset_def, cartesian_product_def — 每個元素與每條邊都逐一檢查；此步不推出任何執行性質。MKO 指出的誤解是把無外出邊自動叫做 halt。s5 沒有後繼，但不在 Halt 中，所以 (s0,s1,s5) 是卡住，不是停止（S07、S09）。是否停止只由 Halt 的給定列表決定。
深度 1 的探索未顯示循環 s2→s4→s2 或卡住的 s5，但不終止的極大執行確實存在（S12、S13）。尚未窮盡可達圖時，沒有看到反例不等於終止證明。完整有限可達圖可用循環與非 Halt 死端檢查判定；一般程式仍需要適當證明方法。
原始資料含 (s3,s6)。若不截斷，s6 會被誤算為可達，(s0,s1,s3,s6) 會被誤認為合法（S06、S11）。MKO 假設 a2 要求在分析前刪去這些邊。
reject — Halt={s3}；s5 是卡住狀態，不是停止狀態。reject — 進入 s3∈Halt 時執行即結束，(s3,s6) 已被截斷。reject — 從 s0 出發後在 s2 與 s4 之間無窮交替的序列是無窮執行，(s0,s1,s5) 是卡住執行。reject — 截斷後沒有任何進入 s6 的邊，Reach={s0,s1,s2,s3,s4,s5}。截斷後 Step 有 6 條邊；Reach={s0,s1,s2,s3,s4,s5}，s6 不可達。s3 是唯一可達的停止狀態，s5 是卡住狀態（沒有後繼但不在 Halt），{s2,s4} 是可達的非停止循環。(s0,s1,s3) 停止，(s0,s1,s5) 卡住，s0 之後在 s2、s4 間無窮交替的序列是無窮執行；(s0,s3)、(s1,s3)、(s0,s1,s3,s6) 都不合法。所以並非所有從 Init 出發的極大執行都停止，深度 1 的探索看不出這一點。
5 個本稿宣告算術檢查；只支持所列算式。
b28a5edbd46279b1db2a3f3f48bb3f447e18899f4e735eff3b7dce6a70f861ddcd8dc409e5a688e22cfd99ecfa7115e5ad0c3ebce947537df405a61ccf81d4f1a305ce5e409796bc956b63e5b8517923dab8e201NOT_MEASURED