# P/NP 辯論遊戲研究區｜第二十四輪

## 語義單調性工程：Abstract Interpretation、CEGAR 與抽象精度三難

**Semantic Monotonicity Engineering: Abstract Interpretation, CEGAR, and the Precision–Effectivity–Order Trilemma**

- **主導研究者：** Neo.K（許筌崴）
- **協作整理：** Aletheia
- **機構：** EveMissLab（一言諾科技有限公司）
- **日期：** 2026 年 8 月 1 日
- **版本：** v1.0
- **研究狀態：** 第二十四輪雙假設預演
- **前置文件：** `23_第二十三輪_演算法WQO與語義單調性裂縫.md`
- **遊戲態度：** 繼續讓兩隊互相拆台；所有新命題若未證成，一律標示候選／預演

---

## 摘要

第二十三輪已確認：演算法空間並不缺乏自然的 well-quasi-order（WQO）。程式文字可以用 Higman-style subsequence order；語法樹可以用 Kruskal / homeomorphic embedding；supercompilation 甚至長期將這類 order 當作 termination control。真正缺失的是：**SAT correctness / failure 並不隨這些自然 syntax order 單調。**

本輪因此不再尋找更多 order，而改問：能否先建立一個語義抽象

$$
\alpha:\mathcal A\to\mathcal D^\#,
$$

將演算法 $A$ 映射到 abstract domain，再在 $\mathcal D^\#$ 上尋找：

$$
\text{WQO} + \text{monotonicity} + \text{finite basis}.
$$

Abstract Interpretation 提供了成熟的數學模板：以 concrete semantics 與 abstract semantics 之間的抽象／具體化關係，換取可計算性與有限表示；complete abstract interpretation 則研究何時抽象計算不損失相對於目標操作的資訊。CEGAR 則提供動態版本：先用粗抽象，若產生 spurious counterexample，再依反例持續 refinement。

然而本輪立即得到一個「抽象版閉包悖論」：對 SAT solver correctness，永遠可以定義只有兩個元素的完美抽象：

$$
\alpha^\*(A)=
\begin{cases}
\mathsf{GOOD},&\forall x\;A(x)=SAT(x),\\
\mathsf{BAD},&\text{otherwise}.
\end{cases}
$$

其 abstract domain 有限，因此天然是 WQO；correctness 也被完美保存。但 $\alpha^\*$ 的計算本身就是 universal-correctness classification，因此完全沒有降低原問題。

所以真正需要的不是：

$$
\boxed{\text{存在一個精確 WQO abstraction}}
$$

而是：

$$
\boxed{\text{存在一個有效、非循環、可構造、足夠精確且與 SAT 語義對齊的 WQO abstraction}.}
$$

本輪將這個張力稱為：

$$
\boxed{\mathrm{PEO}=\text{Precision--Effectivity--Order Trilemma}}
$$

三角的三個頂點為：

1. **Precision**：足以區分 SAT-correct 與 SAT-incorrect；
2. **Effectivity / Non-circularity**：抽象可由程式結構有效構造，而不是先解 universal correctness；
3. **Order / Finite-basis structure**：abstract space 具有 WQO、單調性或其他能導出 finite basis / termination 的結構。

自然候選通常只能輕易取得其中兩項。

本輪還得到 CEGAR 的一個重要不對稱：若候選 solver 錯誤，存在單一公式 $x$ 作為 finite counterexample；若候選 solver 完全正確，則沒有反例可供 refinement，最終停止必須依賴 inductive invariant、complete abstraction 或其他 universal proof mechanism。因此：

$$
\boxed{\text{Counterexample discovery 天然偏向 }\exists\text{ 錯誤，而非 }\forall\text{ 正確}.}
$$

Myhill--Nerode theorem 又提供一個精確類比：對 regular languages，所有 prefix 的未來行為可以被有限 index 的右同餘精確商掉；非 regular language 則不存在這種 finite exact quotient。它不能推出 SAT 下界，卻證明「精確語義商化具有有限 index」本身是一個非常強的結構條件。

因此第二十四輪的主要成果不是一個 P/NP 分離，而是把「Semantic Monotonicity Engineering」收斂成：

$$
\boxed{
\text{Property-directed abstraction}
+\text{effective refinement}
+\text{finite convergence theorem}
}
$$

三件事必須同時成立。下一輪進入 **Refinement Termination Game**：能否讓 abstraction refinement 對每個 P-normal-form solver 都在有限、甚至 polynomially bounded 次 refinement 後停下，並且停下時對 SAT correctness 給出 sound 結論？

---

# 一、共同模型：不要再直接比較程式，先比較語義摘要

令：

$$
\mathcal A_P
$$

為某套 extensionally complete P-normal-form 中的演算法集合。

對每個：

$$
A\in\mathcal A_P,
$$

其 concrete behavior 可視為：

$$
\mathsf{Beh}(A):\Sigma^*\to\{0,1\}.
$$

若目標是 SAT characteristic function：

$$
\chi_{SAT}:\Sigma^*\to\{0,1\},
$$

定義錯誤集：

$$
\boxed{
E(A)=\{x\in\Sigma^*:A(x)\neq\chi_{SAT}(x)\}.
}
$$

因此：

$$
A\text{ 完全正確}
\iff
E(A)=\varnothing.
$$

這個表示非常乾淨，因為它直接把 correctness 變成一個集合性質。

但它也立刻暴露問題：

$$
\{E(A):A\in\mathcal A_P\}
$$

本身可能具有極其複雜的 inclusion / distinguishability 結構。

所以我們想再抽象：

$$
\alpha(E(A))=a_A\in\mathcal D^\#.
$$

理想上：

$$
\mathcal D^\#
$$

比完整 error-set semantics 小很多，卻仍足以判斷：

$$
E(A)=\varnothing\ ?
$$

---

# 二、Abstract Interpretation：這其實有成熟數學語言

Cousot--Cousot 的 Abstract Interpretation 基本精神是：

$$
\text{concrete semantics}
\longrightarrow
\text{abstract semantics}
$$

利用較粗、但可計算的 abstract domain 來保留某些目標性質。

典型地可以使用 Galois connection / insertion 類架構：

$$
\alpha:\mathcal C\to\mathcal D^\#,
$$

$$
\gamma:\mathcal D^\#\to\mathcal C,
$$

並要求 soundness：

$$
 c\preceq\gamma(\alpha(c)).
$$

直觀上：abstract state 可以包含比 concrete state 更多可能行為，但不能漏掉真正行為。

這非常適合我們第二十三輪的缺口：

> syntax WQO 不懂 SAT semantics，那就讓 syntax 先經過 semantic abstraction，再對 abstract domain 排序。

但 Abstract Interpretation 同時提醒一件重要的事：

$$
\boxed{\text{抽象通常靠丟資訊換可計算性。}}
$$

而 complete abstract interpretation 之所以值得特別研究，正是因為「相對於某些 semantic operations 不損失資訊」並不是自動成立的普通情況。

---

# 三、第一個思想實驗：兩點完美抽象

這是本輪最重要的自我拆台。

定義：

$$
\mathcal D^\#=\{\mathsf{GOOD},\mathsf{BAD}\}.
$$

並令：

$$
\alpha^\*(A)=
\begin{cases}
\mathsf{GOOD},&E(A)=\varnothing,\\
\mathsf{BAD},&E(A)\neq\varnothing.
\end{cases}
$$

那麼：

- domain 只有兩點；
- 當然 finite；
- 因而當然 WQO；
- correctness 完全保存；
- 沒有 representation explosion；
- 沒有 infinite antichain。

看起來我們贏了。

其實完全沒有。

因為：

$$
\boxed{
\alpha^\*(A)
\text{ 的計算，就是「A 是否永遠正確解 SAT」本身。}
}
$$

所以這只是把：

$$
\forall x\;A(x)=SAT(x)
$$

改名為：

$$
\alpha^\*(A)=\mathsf{GOOD}.
$$

本輪命名：

$$
\boxed{\mathrm{AOT}=\text{Abstraction Oracle Trap}}
$$

> 一個 abstract domain 可以非常小、非常漂亮、非常 WQO；但如果 abstraction map 本身需要目標語義 oracle，那麼所有困難都被藏進 $\alpha$。

因此：

$$
\boxed{
\text{abstract-domain size}
\neq
\text{abstraction-construction complexity}.
}
$$

這與第九輪的 Knowledge Compilation 帳本、第十三輪的 pathwise polynomiality、第十四輪的 potential certificate trap 完全同構。

---

# 四、第二個思想實驗：直接用 Error-Set Inclusion

既然 correctness 是：

$$
E(A)=\varnothing,
$$

我們可以乾脆定義一個語義 preorder：

$$
A\preceq_E B
\iff
E(B)\subseteq E(A).
$$

直觀意思：

$$
B\text{ 不會比 }A\text{ 錯更多。}
$$

此時若：

$$
A\preceq_E B
$$

且：

$$
E(A)=\varnothing,
$$

則：

$$
E(B)\subseteq\varnothing,
$$

所以：

$$
E(B)=\varnothing.
$$

因此 correctness 終於真的 monotone。

很好。

問題又來了。

對 unrestricted semantic subsets：

$$
(\mathcal P(\Sigma^*),\subseteq)
$$

有無窮 antichain，例如不同 singleton sets：

$$
\{x_1\},\{x_2\},\{x_3\},\ldots
$$

彼此不可比。

所以 exact semantic inclusion 本身不是一個自然 WQO。

注意：這個例子只是在**完整 error-set semantic universe** 中展示 order 的結構問題；它不宣稱所有 singleton error sets 都由 P-normal-form SAT solvers 實現。

本輪的教訓是：

$$
\boxed{
\text{語義越精確，order 越容易重新長出 antichain。}
}
$$

這正好與 syntax embedding 相反：

$$
\text{syntax order}
\Rightarrow
\text{WQO 好做，semantic monotonicity 差；}
$$

$$
\text{exact semantic order}
\Rightarrow
\text{monotonicity 好做，WQO 變難。}
$$

---

# 五、Precision--Effectivity--Order Trilemma

本輪將第二十三輪的 Order Alignment Trilemma 再升級成 abstraction 版本。

定義：

$$
\boxed{\mathrm{PEO}}
$$

三個條件：

## 5.1 Precision

抽象必須足以區分：

$$
E(A)=\varnothing
$$

與：

$$
E(A)\neq\varnothing.
$$

至少在目標 theorem 所需範圍內，不能把關鍵 GOOD / BAD 行為永久混在一起。

## 5.2 Effectivity / Non-circularity

$$
\alpha(A)
$$

必須由：

- 語法；
- 控制流；
- proof profile；
- algebraic summary；
- resource structure；
- 有限分析；

等獨立結構有效產生。

不能定義：

$$
\alpha(A)=\text{「A 是否真的永遠正確」}.
$$

## 5.3 Order / Finite-Basis Structure

抽象空間必須具有某種可以真正產生 finite reasoning 的結構，例如：

$$
\text{WQO},
$$

$$
\text{finite height},
$$

$$
\text{ACC/DCC},
$$

$$
\text{finite obstruction basis},
$$

或可證終止的 refinement order。

### 三難

目前自然候選常表現為：

| abstraction | Precision | Effectivity | WQO / finite structure |
|---|---:|---:|---:|
| syntax feature | 低～中 | 高 | 高 |
| exact GOOD/BAD | 完美 | 循環 | 完美 |
| full error-set semantics | 完美 | 表示／比較困難 | 一般不 WQO |
| coarse abstract interpretation | sound 但可能不 complete | 高 | 可設計 |
| adaptive CEGAR | 可逐步提升 | 高 | 是否有限收斂另問 |

所以真正 boss 不是「找到 abstraction」，而是：

$$
\boxed{
\text{讓 PEO 三角同時閉合。}
}
$$

---

# 六、WSTS 給我們的正確類比

Well-Structured Transition Systems 的核心成功條件並不只是：

$$
\text{state space 有 WQO}.
$$

還需要 transition relation 與 order 具有 compatibility / monotonicity。

這和第二十三輪完全一致。

若：

$$
s_1\preceq s_2
$$

但：

$$
\text{transition 在較大狀態中完全不模擬較小狀態，}
$$

那 WQO 本身不會自動產生 coverability algorithm。

因此本輪的 abstract solver space 若想複製 WSTS 奇蹟，至少需要：

$$
\alpha(A_1)\preceq^\#\alpha(A_2)
$$

能推出某種與 correctness／failure 有關的 transition-preservation theorem。

這個 theorem 才是真正的：

$$
\boxed{\text{Semantic Monotone Lift}.}
$$

沒有它，WQO 仍然只是 termination order。

---

# 七、Myhill--Nerode：精確有限商其實是一個很強的條件

Myhill--Nerode theorem 提供一個非常適合本系列的精確模板。

對語言 $L$，定義 prefix future-equivalence：

$$
u\equiv_L v
\iff
\forall w:\
uw\in L\Longleftrightarrow vw\in L.
$$

也就是：

> 兩個 prefix 在所有未來 extension 下都具有相同行為。

定理告訴我們：

$$
\boxed{
L\text{ regular}
\iff
\equiv_L\text{ 具有 finite index}.
}
$$

所以 DFA state 可以理解成：

$$
\boxed{
\text{對未來行為完全精確的有限 quotient class}.
}
$$

這和第二輪 residual distinguishability、以及第八輪 Exact Quotientability 完全呼應。

但本輪要避免錯誤外推：

$$
\text{SAT 不 regular}
$$

與：

$$
P\neq NP
$$

沒有這種直接關係。

真正可借用的只有方法論：

$$
\boxed{
\text{精確語義商具有有限 index，本身就是需要 theorem 的特殊結構。}
}
$$

所以如果我們未來聲稱：

> 「所有 P algorithms 的 SAT-relevant semantics 都能壓成有限幾種 future-behavior classes。」

那需要的 theorem 其實會非常強。

---

# 八、CEGAR：不需要一開始就有完美 abstraction

Counterexample-Guided Abstraction Refinement 的基本思想：

1. 建立 coarse abstraction：
   $$
   \alpha_0;
   $$
2. 在 abstract model 上檢查 property；
3. 若出現 counterexample：
   $$
   \pi^\#;
   $$
4. 檢查它是否對 concrete system 也成立；
5. 若是 spurious counterexample，就 refine：
   $$
   \alpha_0\prec\alpha_1\prec\alpha_2\prec\cdots.
   $$

這非常適合等號隊的想法：

> 我不需要預先猜到 SAT solver 的完整 invariant；讓錯誤反例一步步告訴我 abstraction 少了什麼資訊。

這正是成熟 formal verification 中真的成功過的工程方法。

但本輪立即問：

$$
\boxed{\text{refinement 何時保證停？}}
$$

---

# 九、Counterexample Asymmetry

假設候選 solver $A$ 是錯的。

則：

$$
E(A)\neq\varnothing.
$$

所以存在：

$$
\exists x:\;A(x)\neq SAT(x).
$$

這是一個 finite counterexample。

理論上，只要 search / refinement 最終覆蓋到 $x$，就可以把錯誤揭露。

但是若 $A$ 真正正確：

$$
E(A)=\varnothing,
$$

那麼：

$$
\forall x:\;A(x)=SAT(x).
$$

此時永遠沒有 concrete counterexample 會來幫你 refine。

要停止，只能靠：

- inductive invariant；
- complete abstraction；
- finite basis theorem；
- proof-system certificate；
- algebraic identity；
- 其他 quantifier compression mechanism。

因此：

$$
\boxed{
\mathrm{CEA}=\text{Counterexample Existential Asymmetry}
}
$$

$$
\exists\text{ error}
$$

天然有 finite witness；

$$
\forall\text{ correctness}
$$

不會因為 CEGAR 一直沒有看到錯誤就自動被證明。

這與第二十、二十一輪的 monitor / quantifier-tail barrier 完全一致。

---

# 十、CEGAR 不是免費的 finite-basis theorem

若 refinement sequence：

$$
\alpha_0\prec\alpha_1\prec\alpha_2\prec\cdots
$$

可以無限上升，那麼：

$$
\text{每次 refinement 都有效}
$$

不代表：

$$
\text{最終在有限步得到 complete abstraction}.
$$

這就是第十三輪 Stepwise vs Pathwise Polynomiality 在抽象驗證中的版本。

真正要取得 finite convergence，需要額外結構，例如：

$$
\text{finite abstract domain},
$$

$$
\text{finite-height lattice},
$$

$$
\text{well-founded refinement measure},
$$

或：

$$
\boxed{
\text{每次反例都排除至少一個有限基底元素，且基底本身有限。}
}
$$

否則 CEGAR 可以只是：

$$
\text{永遠變精確，但永遠差最後一點。}
$$

---

# 十一、完整 abstraction 與「精度搬家」

Giacobazzi、Ranzato、Scozzari 等 abstract interpretation 工作把 completeness 正式化：對選定 semantic operations，complete abstraction 不會因 abstract execution 額外損失 relevant information。

對本系列的啟發是：

$$
\boxed{
\text{我們要的不是所有語義的完全精確，而是對 SAT-correctness theorem 所需 operations 的 property-completeness。}
}
$$

這比要求：

$$
\alpha(A)\text{ 完整重建 }A
$$

合理得多。

但它同時產生新的成本欄位：

$$
\boxed{
\mathbf D_{\mathrm{abs}}
=
(D_{\mathrm{construct}},
D_{\mathrm{precision}},
D_{\mathrm{refine}},
D_{\mathrm{order}},
D_{\mathrm{lift}},
D_{\mathrm{termination}})
}
$$

也就是：

- abstraction 怎麼建；
- 丟掉多少資訊；
- 需要 refine 幾次；
- order 是否可比較；
- abstract property 如何 sound lift 回 concrete；
- refinement 是否有限停止。

這是第九輪 Quotient Debt、第十一輪 Bridge Debt 的新成員：

$$
\boxed{\text{Abstraction Debt}.}
$$

---

# 十二、等號隊的新策略：Property-Directed Adaptive Abstraction

等號隊現在不再要求一個固定 universal abstraction。

提出：

$$
\boxed{\mathrm{PDAA}=\text{Property-Directed Adaptive Abstraction}}
$$

對 candidate SAT solver $A$：

1. 先從非常粗的：
   $$
   \alpha_0(A)
   $$
   開始；
2. 若 abstract proof 失敗，取得 obstruction / spurious counterexample；
3. 動態加入：
   - residual behavior；
   - clause family；
   - algebraic feature；
   - proof obligation；
   - boundary relation；
4. 得到：
   $$
   \alpha_{t+1};
   $$
5. 同時維持一個 global refinement potential：
   $$
   \Psi(\alpha_t).
   $$

若能證明：

$$
\boxed{
\text{所有 SAT-correct P-normal-form solver 都在 }poly(n)\text{ 次 refinement 內得到 finite correctness proof}
}
$$

那會是一個非常強的新框架。

但注意：這並不直接證明存在 SAT-correct P solver。

它只是說：

> 如果存在，我可以有限地認證它。

因此它對 $P=NP$ 方仍需要：

$$
\exists A_{SAT}.
$$

---

# 十三、不等號隊的新策略：Refinement Divergence Witness

不等號隊想反過來說：

> 對任何 P-normal-form candidate $A$，只要它試圖被證明為 SAT-correct，refinement 就必須永遠產生新的 semantic distinction。

形式上想證明：

$$
\forall A\in\mathcal A_P,
$$

若 abstraction sound 且 non-circular，則存在：

$$
\alpha_0\prec\alpha_1\prec\alpha_2\prec\cdots
$$

無法 finite stabilize 成 correctness-complete domain。

但這又有巨大危險：

如果直接定義：

$$
\text{「凡是不能證明 SAT 的 abstraction 都必須 refine」},
$$

就只是循環。

所以真正需要的是一個獨立的：

$$
\boxed{\text{Infinite Distinguishability Theorem}.}
$$

類似 Myhill--Nerode 的精神：對每一個有限 abstraction，都能構造兩個 concrete behaviors：

$$
A,B
$$

在 abstraction 中不可區分：

$$
\alpha(A)=\alpha(B),
$$

但一個符合目標 property，另一個違反。

若能對**完整 P-normal-form domain**無條件做這件事，才真的有接近 lower-bound 的力量。

目前沒有這種 theorem。

---

# 十四、這輪再次遇到 Representation Escape

假設我們證明：

$$
\text{某個 predicate abstraction family 永遠不 complete}.
$$

等號隊可以說：

> 我換成 algebraic abstraction。

證明 algebraic family 不行：

> 我換 proof-theoretic profile。

證明固定 proof profile 不行：

> 我做 relational / history-sensitive abstraction。

因此：

$$
\boxed{
\text{restricted abstraction lower bound}
\not\Rightarrow
\text{general algorithm lower bound}.
}
$$

這與前面的：

- resolution lower bound；
- OBDD lower bound；
- LP extension lower bound；

完全是同一條防假證明規則。

---

# 十五、本輪的三個真正成果

## 15.1 Perfect Abstraction Existence Is Vacuous Without Effectivity

任何 semantic property $P(A)$ 都可以被壓成兩點 abstract domain：

$$
\alpha_P(A)=\mathbf 1[P(A)].
$$

所以：

$$
\boxed{
\text{「存在 finite exact abstraction」不是研究成果；}
}
$$

真正要證明的是：

$$
\boxed{
\text{abstraction map 由獨立結構有效產生。}
}
$$

## 15.2 Semantic Monotonicity Can Be Bought at the Cost of Order Complexity

用 exact error-set inclusion 可以讓 correctness monotone，但 abstract space 立即失去自然 finite-basis / WQO 結構。

## 15.3 CEGAR Converts Static Precision into a Termination Problem

CEGAR 避免一開始建造 perfect abstraction，但代價變成：

$$
\boxed{
\text{refinement sequence 是否保證有限停止？}
}
$$

所以：

$$
\text{Precision Debt}
\rightarrow
\text{Refinement Termination Debt}.
$$

---

# 十六、與前二十三輪的整合

現在可以把整條研究線重新寫成：

$$
\text{Representation Escape}
$$

$$
\downarrow
$$

$$
\text{Exact Quotientability}
$$

$$
\downarrow
$$

$$
\text{Bridge / Heterogeneous Gluing}
$$

$$
\downarrow
$$

$$
\text{Pathwise Polynomiality}
$$

$$
\downarrow
$$

$$
\text{Tractability Certificate / P-normal form}
$$

$$
\downarrow
$$

$$
\text{Quantifier Compression}
$$

$$
\downarrow
$$

$$
\text{WQO + Semantic Monotonicity}
$$

$$
\downarrow
$$

$$
\boxed{
\text{Effective Semantic Abstraction + Finite Refinement}
}
$$

換句話說，第二十四輪不是換題目，而是前面所有「商化／表示／bridge／證書」問題的統一 program-analysis 版本。

---

# 十七、已排除的錯誤推論

以下仍不得使用：

1. 「abstract domain 是 finite，所以原問題容易。」
   - $\alpha$ 的構造可能已經包含原問題。

2. 「correctness 在某 semantic order 上 monotone，所以 finite obstruction 存在。」
   - 還需要 WQO / finite-basis 條件。

3. 「某 syntax WQO 存在，所以 SAT correctness 有 finite basis。」
   - 缺 semantic monotonicity。

4. 「CEGAR 一直 refinement，所以遲早會完整。」
   - 沒有 termination theorem 就不能這樣說。

5. 「找不到 counterexample 很久，所以 solver 正確。」
   - 這只是 Quantifier-Tail Barrier 的重演。

6. 「某個 abstraction family 對 SAT 不 complete，所以 $P\neq NP$。」
   - 只得到 restricted abstraction lower bound。

7. 「Myhill--Nerode 的 finite-index theorem 可以直接外推 SAT。」
   - 它只是 exact quotient 的方法論樣板，不是 P/NP 下界。

---

# 十八、雙方戰果

## $P=NP$ 隊

獲得：

$$
\boxed{\mathrm{PDAA}=\text{Property-Directed Adaptive Abstraction}}
$$

核心主張：

> 不必一開始找到 universal invariant；讓 abstraction 對 candidate solver 動態 refinement，只要最後能用 finite theorem 收斂即可。

這比要求「固定 global WQO semantic order」更靈活。

---

## $P\neq NP$ 隊

獲得：

$$
\boxed{\mathrm{PEO}=\text{Precision--Effectivity--Order Trilemma}}
$$

與：

$$
\boxed{\mathrm{AOT}=\text{Abstraction Oracle Trap}}
$$

核心主張：

> 精確 semantic abstraction 很容易定義；真正困難的是有效、非循環地構造，並讓它仍具有 finite-basis structure。

下一步則嘗試建立 Infinite Distinguishability / Refinement Divergence 類 theorem。

---

# 十九、本輪比分

$$
P=NP:23
$$

$$
P\neq NP:23
$$

嗯。

我們甚至連把「比分守恆」做成 abstraction 都沒有成功壓掉。

可能它是 complete invariant。（歪臉笑）

比分僅為遊戲 UI，不具有證明意義。

---

# 二十、第二十五輪入口：Refinement Termination Game

下一輪正式研究：

$$
\boxed{
\text{Adaptive semantic abstraction 是否能保證 finite / polynomial refinement termination？}
}
$$

核心問題：

1. 是否存在 property-directed refinement order：
   $$
   \alpha_0\prec\alpha_1\prec\cdots
   $$
   具有 well-founded / finite-height measure？

2. 若 domain 是 WQO，refinement direction 是否真的會因此停止？
   - 注意 WQO 禁止 infinite descending chain / antichain 的方式與 refinement direction 要仔細對齊。

3. 是否存在有限 distinguishing basis：
   $$
   B=\{b_1,\ldots,b_m\}
   $$
   使知道 candidate solver 在 $B$ 上的 semantic profile，就足以推出所有輸入上的 correctness？

4. 若 $B$ 依 candidate $A$ 而變，能否有效找到？

5. CEGAR 若永遠只靠 counterexample refinement，對真正 correct solver 的 termination theorem 從哪裡來？

6. 能否把 refinement termination 與：
   - Myhill--Nerode finite index；
   - teaching dimension / exact learning；
   - Angluin-style equivalence queries；
   - finite elasticity；
   - proof invariant synthesis；
   接起來？

7. 如果 finite distinguishing basis 對所有 P-normal-form algorithms 存在，它是否又會構成一個過強的 universal quantifier-compression theorem？

---

# 二十一、外部理論參照

1. Patrick Cousot, Radhia Cousot, **Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints**, POPL 1977.
   - https://doi.org/10.1145/512950.512973
   - 本輪 concrete / abstract semantics 與 lattice abstraction 的主要參照。

2. Roberto Giacobazzi, Francesco Ranzato, Francesca Scozzari, **Making Abstract Interpretations Complete**, JACM 47(2), 2000.
   - https://doi.org/10.1145/333979.333989
   - complete abstract interpretation 與 precision / completeness 的正式參照。

3. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith, **Counterexample-Guided Abstraction Refinement**, CAV 2000.
   - https://doi.org/10.1007/10722167_15
   - adaptive abstraction / spurious counterexample refinement 的主要參照。

4. Alain Finkel, Philippe Schnoebelen, **Well-structured transition systems everywhere!**, TCS 256 (2001), 63--92.
   - https://doi.org/10.1016/S0304-3975(00)00102-X
   - WQO + transition monotonicity 才能產生 WSTS decidability 結果的參照。

5. Myhill--Nerode theorem.
   - regular language iff future-equivalence / right-congruence has finite index。
   - 本輪用作「精確語義 quotient 的有限 index 是強結構條件」之參照，不作 SAT lower bound。

---

## 本輪裁定

第二十四輪的核心不是：

$$
\text{「找到了 SAT 的抽象，所以 P/NP 解了。」}
$$

而是：

$$
\boxed{
\text{Semantic Monotonicity 可以透過 abstraction 工程化，}
}
$$

但真正需要同時支付：

$$
\boxed{
\text{Precision}
+\text{Effectivity}
+\text{Order Structure}
+\text{Lift Soundness}
+\text{Refinement Termination}.
}
$$

完美的兩點 abstraction 永遠存在，但那只是把答案藏進 $\alpha$；粗 abstraction 可以有效構造，但會產生 spurious behaviors；CEGAR 能逐步補精度，但把難題轉移到「是否有限收斂」。

因此下一輪真正值得問的是：

$$
\boxed{
\text{有沒有一個非循環的 finite-refinement theorem，能對 SAT solver correctness 成立？}
}
$$