演算法 WQO 與語義單調性裂縫:為什麼 Graph-Minor 式有限禁阻集沒有直接搬進 P/NP

第二十二輪留下一個 Graph-Minor 式夢想:替 P-normal-form algorithms 找一個 well-quasi-order,讓 SAT correctness/failure 單調,就能複製有限禁阻集定理。本輪測試六種候選 order 後得到關鍵修正——WQO 本身其實很便宜:對有限 alphabet 的程式文字,Higman lemma 直接給出 subsequence WQO;對程式語法樹,Kruskal tree theorem 給出 homeomorphic-embedding WQO,而且這不是紙上假設,supercompilation、partial evaluation 等程式轉換技術早就拿它當 termination whistle 用。真正卡住的是第二個條件:自然 syntactic WQO 幾乎不會讓 SAT correctness 具有所需單調性——只要在程式裡插入一行 if trigger(x): return 1,語法上仍是 subsequence,語義卻可能整個翻轉;反過來把 order 換成語義等價或語言包含,又立刻在 singleton 語言或不同 Boolean 函數上長出 infinite antichain,失去 WQO。本輪把這個張力正式提煉成 WQO--Semantic Alignment Barrier(WSAB)與更具操作性的 Order Alignment Trilemma:結構 WQO、語義單調性、非循環的資源相關性三個角,自然候選通常只能同時拿到兩項。最重要的正面結果是把 Termination WQO(控制展開軌跡)與 Hardness WQO(讓 correctness 集合有 finite basis)正式分開——supercompilation 用的是前者,不能自動當後者用;而 Bellantoni–Cook/Cobham 類完整 P grammar 的 derivation trees 確實可以套 Kruskal 型 WQO,所以失敗點已經從「沒有 order」精確收斂成「缺乏能讓語義性質 closure 的 order」。