# SECV Paper 04｜合法消除演算：Soundness、Termination 與 Confluence

**English Title:** Legal Elimination Calculus: Soundness, Termination, and Confluence  
**Series:** Symbolic Equivalence-Constrained Variable Method  
**Paper:** 04 / 10  
**Version:** v0.1  
**Author:** Neo.K  
**AI Collaboration:** Aletheia (GPT-5.6 Sol)  
**Status:** Formal Reliability Draft

---

## 摘要

本文建立 SECV（Symbolic Equivalence-Constrained Variable Method）的可信度核心：合法消除演算（Legal Elimination Calculus, LEC）。前述 SECV 已允許符號商化、對偶、自指、殘差化與符號自由度降維，但若缺少嚴格的 soundness、termination 與 confluence 條件，任何「消除」都可能退化為結果導向的符號刪除。

本文因此定義三個核心問題：

$$
\boxed{
\text{Soundness: 消除後是否仍保存原證明義務？}
}
$$

$$
\boxed{
\text{Termination: reduction 是否保證在有限或可控意義下停止？}
}
$$

$$
\boxed{
\text{Confluence: 不同合法消除順序是否得到同一等價 normal form？}
}
$$

本文建立局部與全域 soundness、certificate-carrying reduction、well-founded measure、cycle quotient、local confluence、critical-pair analysis、canonical normal form、rule-versioning、proof invalidation graph 與 fail-closed execution contract。本文進一步提出：SECV 的正式 proof layer 必須將「候選規則發現」與「已證明規則執行」分離，任何未被驗證的 heuristic 都不得直接提交到 canonical proof state。

本文不主張所有 SECV 系統都必然可終止或可合流；本文的目標是提供清楚的形式判準，使任何實作都能明確標示其證明強度與失效邊界。

---

## 關鍵詞

soundness、termination、confluence、rewrite system、critical pair、normal form、certificate、proof invalidation、fail-closed、SECV。

---

# 1. 為什麼「可以消」本身還不夠

若一個系統看到：

$$
x\sim y
$$

就直接執行：

$$
x,y\rightarrow[x],
$$

但沒有回答：

$$
\text{「這個等價關係保存了什麼？」}
$$

則 reduction 可能破壞原命題。

同樣地，若每次消除都合法，但 reduction 可以：

$$
X_0\rightarrow X_1\rightarrow X_2\rightarrow\cdots
$$

永不停止，則演算法可能無法產生可提交結果。

又或者，不同順序得到：

$$
X_0\rightarrow^\ast A,
$$

以及：

$$
X_0\rightarrow^\ast B,
$$

且：

$$
A\not\equiv B,
$$

則系統沒有唯一的 canonical residual。

因此，合法消除演算至少必須處理：

$$
\boxed{
\text{保真}
+
\text{停止}
+
\text{路徑一致性}.
}
$$

---

# 2. Reduction system

定義 SECV reduction system：

$$
\mathfrak R
=
(
\mathcal X_\Gamma,
\rightarrow,
\mathcal Q,
\mathcal I,
\Pi
),
$$

其中：

$$
\mathcal X_\Gamma
$$

為合法狀態域；

$$
\rightarrow
$$

為一步 reduction 關係；

$$
\mathcal Q
$$

為 proof obligations；

$$
\mathcal I
$$

為 invariants；

$$
\Pi
$$

為 certificate/provenance layer。

一步 reduction：

$$
x\rightarrow y
$$

只有在存在 certificate：

$$
\pi(x\rightarrow y)
$$

時，才屬於正式 proof layer。

---

# 3. Local soundness

對單一步驟：

$$
x\rightarrow y,
$$

定義 local soundness：

$$
\boxed{
\mathcal Q(x\mid\Gamma)
\equiv
\mathcal Q(y\mid\Gamma).
}
$$

若 $\mathcal Q$ 是命題集合，則可要求：

$$
\Gamma\models
Q(x)\leftrightarrow Q(y)
$$

對所有：

$$
Q\in\mathcal Q.
$$

若只需要單向保存，例如 reduction 只服務 implication proof，則可定義 directional soundness：

$$
\Gamma\models
Q(y)\Rightarrow Q(x)
$$

或：

$$
\Gamma\models
Q(x)\Rightarrow Q(y).
$$

因此 soundness 必須標記方向。

---

# 4. Strong soundness 與 task soundness

SECV 區分兩種強度。

## 4.1 Strong soundness

要求完整語義等價：

$$
x\equiv_\Gamma y.
$$

此時所有合法 query 都可互換。

## 4.2 Task soundness

只要求：

$$
x\equiv_{\Gamma,\mathcal Q}y.
$$

即對目前 proof obligations 足夠。

因此：

$$
\boxed{
\text{Strong soundness}
\Rightarrow
\text{Task soundness},
}
$$

但反之不成立。

實際 SECV 多數 reduction 屬於 task-sound，而非 absolute semantics-preserving。

---

# 5. Invariant soundness

除了 proof obligation，還可要求 invariants：

$$
\mathcal I
=
\{I_1,\ldots,I_m\}.
$$

若：

$$
x\rightarrow y,
$$

則對 strict invariants：

$$
I_k(x)=I_k(y).
$$

對 monotone invariants：

$$
I_k(y)\preceq I_k(x)
$$

或事先定義的方向。

因此 certificate 需要至少包含：

$$
\boxed{
\pi
=
(
\text{rule},
\text{domain witness},
\text{obligation proof},
\text{invariant proof}
).
}
$$

---

# 6. Global soundness

若：

$$
x_0\rightarrow x_1\rightarrow\cdots\rightarrow x_n,
$$

且每一步 local sound，則由傳遞性得到：

$$
\boxed{
\mathcal Q(x_0)
\equiv
\mathcal Q(x_n).
}
$$

因此 finite reduction chain 的 global soundness 可以由 local soundness 組成。

若存在無限 reduction chain，則不能僅以「每一步都 sound」直接推出極限對象 sound，除非另外證明：

$$
\text{limit existence},
$$

$$
\text{continuity},
$$

以及：

$$
\text{obligation preservation under limit}.
$$

這一點留給 Paper 08 的無限階版本。

---

# 7. Certificate-carrying reduction

正式 SECV 狀態不只保存：

$$
x_n,
$$

還保存：

$$
(x_n,\Pi_n).
$$

其中：

$$
\Pi_n
=
\{\pi_1,\ldots,\pi_n\}.
$$

每一個：

$$
\pi_k
$$

證明：

$$
x_{k-1}\rightarrow x_k.
$$

因此 canonical proof state 應寫為：

$$
\boxed{
\mathsf{State}_n
=
(
x_n,
\Pi_n
).
}
$$

不是只有：

$$
x_n.
$$

---

# 8. Heuristic layer 與 proof layer 分離

SECV 可以允許 AI、搜尋器或 heuristic 提出：

$$
x\overset{?}{\rightarrow}y.
$$

但此時狀態只能是：

$$
\mathsf{candidate}.
$$

只有得到 certificate：

$$
\pi(x\rightarrow y)
$$

後才能：

$$
\mathsf{candidate}
\rightarrow
\mathsf{certified}.
$$

因此流程為：

$$
\boxed{
\text{Propose}
\rightarrow
\text{Check}
\rightarrow
\text{Certify}
\rightarrow
\text{Commit}.
}
$$

而不是：

$$
\text{Propose}
\rightarrow
\text{Commit}.
$$

---

# 9. Fail-closed commitment

若 relation 狀態是：

$$
\mathsf{unknown},
$$

則：

$$
\boxed{
\mathsf{unknown}
\not\Rightarrow
\mathsf{valid}.
}
$$

正式系統採：

$$
\boxed{
\text{Fail Closed}.
}
$$

任何無法證明合法的消除都不進入 canonical state。

這是 SECV 防止符號過擬合的第一道工程防線。

---

# 10. Termination 問題

令：

$$
x_0\rightarrow x_1\rightarrow x_2\rightarrow\cdots.
$$

若不存在無限嚴格 reduction chain，則 relation $\rightarrow$ 稱為 terminating 或 strongly normalizing。

形式上：

$$
\boxed{
\nexists
(x_n)_{n\in\mathbb N}
:
x_0\rightarrow x_1\rightarrow x_2\rightarrow\cdots
}
$$

這是最強版本的 termination。

---

# 11. Well-founded measure

最常見的 termination 證法，是構造：

$$
\mu:
\mathcal X_\Gamma
\rightarrow
W,
$$

其中：

$$
(W,\prec)
$$

為 well-founded order。

要求每一步：

$$
x\rightarrow y
$$

都有：

$$
\boxed{
\mu(y)\prec\mu(x).
}
$$

因為 well-founded order 不允許無限下降鏈，所以 reduction 必停。

---

# 12. Natural-number measure

最簡單情況：

$$
\mu(x)\in\mathbb N.
$$

若：

$$
\mu(y)<\mu(x)
$$

每一步都成立，則 termination 立即成立。

可選：

$$
\mu(X)
=
a\,\operatorname{srank}(X)
+
b\,\operatorname{exprsize}(X)
+
c\,\operatorname{dep}(X),
$$

其中：

$$
a,b,c>0.
$$

但 weighted sum 只有在每一步都真正嚴格下降時才有效。

---

# 13. Lexicographic measure

若某一步可能 rank 不變但 residual complexity 下降，可使用：

$$
\mu(X)
=
(
r(X),
d(X),
s(X)
)
$$

並採 lexicographic order：

$$
(r_1,d_1,s_1)
\prec
(r_2,d_2,s_2)
$$

若第一個不同分量更小。

例如：

$$
\boxed{
\mu(X)
=
(
\operatorname{srank},
\operatorname{residualDepth},
\operatorname{exprsize}
).
}
$$

這允許 rank-neutral residual lifting，只要後續 measure 嚴格下降。

---

# 14. Multiset order

若系統同時存在多個 residual：

$$
R=\{r_1,\ldots,r_k\},
$$

可為每個 residual 賦予 complexity：

$$
c(r_i).
$$

整體 measure 使用 multiset extension：

$$
\mu(R)
=
\{\!\{
c(r_1),\ldots,c(r_k)
\}\!\}.
$$

只要每次將一個 residual 換成若干更小 residual，便可使用 well-founded multiset order 證 termination。

---

# 15. 不一定要求完整 termination

某些系統本質上允許無限展開，但任意特定查詢只需要有限部分。

此時可以放寬為 query-relative termination：

$$
\boxed{
\forall Q\in\mathcal Q,
\quad
\exists N_Q<\infty
}
$$

使第：

$$
N_Q
$$

步後已足以決定 $Q$。

因此：

$$
\text{global nontermination}
$$

不必然等於：

$$
\text{task nontermination}.
$$

Paper 08 將處理這一類 infinite-order closure。

---

# 16. Cycle detection

若 reduction 出現：

$$
x_i\rightarrow x_{i+1}\rightarrow\cdots\rightarrow x_j
$$

且：

$$
x_j\cong x_i,
$$

則形成 cycle。

此時不能繼續重跑相同 cycle。

最簡單處理：

$$
\boxed{
\text{detect}
\rightarrow
\text{freeze}
\rightarrow
\text{quotient as orbit}.
}
$$

若 cycle 本身具有 invariant：

$$
I(x_i)=I(x_{i+1})=\cdots=I(x_j),
$$

則可以壓縮成：

$$
[x_i,\ldots,x_j]_I.
$$

---

# 17. Normal form

若：

$$
x
$$

沒有任何合法 outgoing reduction：

$$
\nexists y:
x\rightarrow y,
$$

則稱 $x$ 為 normal form。

記為：

$$
\boxed{
\operatorname{NF}(x).
}
$$

如果 reduction terminating，則每條 reduction path 都會到某個 normal form。

但這個 normal form 未必唯一。

---

# 18. Confluence

relation $\rightarrow$ 稱為 confluent，若：

$$
x\rightarrow^\ast y_1,
$$

且：

$$
x\rightarrow^\ast y_2,
$$

則存在：

$$
z
$$

使：

$$
y_1\rightarrow^\ast z,
$$

且：

$$
y_2\rightarrow^\ast z.
$$

形式上：

$$
\boxed{
x\rightarrow^\ast y_1
\land
x\rightarrow^\ast y_2
\Rightarrow
\exists z:
y_1\rightarrow^\ast z
\land
y_2\rightarrow^\ast z.
}
$$

若 terminating 且 confluent，則 normal form 唯一到等價意義。

---

# 19. Local confluence

local confluence 只要求一步分叉：

$$
x\rightarrow y_1,
$$

$$
x\rightarrow y_2
$$

可以重新 join：

$$
\exists z:
y_1\rightarrow^\ast z,
$$

$$
y_2\rightarrow^\ast z.
$$

對 terminating rewrite system，Newman 類型的標準結構告訴我們：

$$
\boxed{
\text{Termination}
+
\text{Local Confluence}
\Rightarrow
\text{Confluence}.
}
$$

SECV 可直接採此 proof pattern，但必須確保 reduction relation 的條件符合所使用的定理框架。

---

# 20. Critical pair

若兩條規則：

$$
R_1,
R_2
$$

都能作用在同一符號區域：

$$
x,
$$

得到：

$$
x\overset{R_1}{\rightarrow}y_1,
$$

$$
x\overset{R_2}{\rightarrow}y_2,
$$

則：

$$
(y_1,y_2)
$$

形成 critical pair。

SECV 必須檢查：

$$
\boxed{
y_1
\downarrow
y_2
}
$$

也就是兩者是否可 join 到共同 residual。

---

# 21. Critical-pair matrix

若規則集：

$$
\mathcal T
=
\{R_1,\ldots,R_m\},
$$

可建立：

$$
C_{ij}
=
\operatorname{Conflict}(R_i,R_j).
$$

若：

$$
C_{ij}=0,
$$

表示兩規則無重疊或可交換。

若：

$$
C_{ij}=1,
$$

則需要 explicit joinability proof。

這使 confluence analysis 可以演算法化。

---

# 22. Commuting reductions

若：

$$
R_i(R_j(x))
\cong
R_j(R_i(x)),
$$

則兩規則 commute。

此時：

$$
x
\overset{R_i}{\rightarrow}
y_i
$$

與：

$$
x
\overset{R_j}{\rightarrow}
y_j
$$

的分叉天然可 join。

因此證明 operator pair commutation 是降低 critical-pair 成本的重要策略。

---

# 23. Canonical representative

即使等價類唯一，其 representative 仍可能不唯一。

例如：

$$
[a,b]
$$

與：

$$
[b,a]
$$

屬於同一 class。

因此需要 canonicalization function：

$$
\kappa:
[x]\mapsto x_{\mathrm{can}}.
$$

並要求：

$$
x\equiv y
\Rightarrow
\kappa(x)=\kappa(y).
$$

此時 normal form 可以變成 machine-stable canonical form。

---

# 24. Canonical residual domain

若 reduction system terminating、confluent，且 canonicalization deterministic，則可以定義：

$$
\boxed{
\operatorname{CRD}(X)
=
\kappa(
\operatorname{NF}(X)
).
}
$$

此物件就是 canonical residual domain。

這使：

$$
X_1\equiv X_2
$$

可被檢查為：

$$
\operatorname{CRD}(X_1)
=
\operatorname{CRD}(X_2)
$$

在規則完備的前提下。

---

# 25. Confluence 不一定必須是 syntactic

兩條路徑可能得到：

$$
A\neq B
$$

但：

$$
A\equiv_{\Gamma,\mathcal Q}B.
$$

因此 SECV 通常追求：

$$
\boxed{
\text{semantic confluence}
}
$$

而非 strict syntactic confluence。

定義：

$$
A
\Downarrow_{\Gamma,\mathcal Q}
B
$$

若：

$$
A\equiv_{\Gamma,\mathcal Q}B.
$$

此時不同 normal forms 仍可被視為同一 proof-equivalent residual class。

---

# 26. Weak confluence mode

若系統無法證明完整 confluence，可降級為：

$$
\boxed{
\text{path-labeled residual mode}.
}
$$

輸出：

$$
(\Sigma_\star,\mathcal P)
$$

其中：

$$
\mathcal P
$$

明確保存 reduction path。

此時不能宣稱：

$$
\Sigma_\star
$$

為唯一 normal form。

只能說：

$$
\boxed{
\text{這是某條合法路徑所得 residual。}
}
$$

---

# 27. Rule freeze

正式推演前：

$$
\mathcal T_0
$$

必須凍結。

若：

$$
\mathcal T_t\neq\mathcal T_0
$$

則原 proof state 不能直接視為同一 proof version。

因此每次 canonical proof 都必須攜帶：

$$
\boxed{
\operatorname{RuleSetHash}(\mathcal T_0).
}
$$

或等價的版本識別。

---

# 28. Rule versioning

定義：

$$
\mathcal T^{(0)},
\mathcal T^{(1)},
\mathcal T^{(2)},\ldots
$$

每次新增、修改或刪除規則，都產生新版本。

proof object：

$$
\Pi
$$

必須綁定：

$$
\operatorname{Version}(\Pi)
=
\mathcal T^{(k)}.
$$

因此不能用：

$$
\mathcal T^{(k+1)}
$$

事後替：

$$
\mathcal T^{(k)}
$$

下的舊步驟補證明，除非重新驗證。

---

# 29. Proof dependency graph

建立 proof dependency graph：

$$
G_P=(V_P,E_P).
$$

節點包括：

$$
\text{rule},
\text{lemma},
\text{certificate},
\text{reduction step},
\text{result}.
$$

若節點 $a$ 被節點 $b$ 使用：

$$
a\rightarrow b.
$$

當某條 rule 被修改，只需要 invalidate：

$$
\operatorname{Descendants}(R).
$$

而不必重新驗證所有無關 proof nodes。

---

# 30. Selective invalidation

若：

$$
R_i
$$

被替換為：

$$
R_i',
$$

則：

$$
\boxed{
\mathcal V_{\mathrm{invalid}}
=
\operatorname{Reach}^+_{G_P}(R_i).
}
$$

只將可達後繼標為 invalid。

這是 SECV 在大型 proof runtime 中的重要工程性質。

---

# 31. Proof state machine

正式狀態可定義：

$$
\mathsf{Status}
\in
\{
\mathsf{proposed},
\mathsf{checked},
\mathsf{certified},
\mathsf{committed},
\mathsf{invalidated},
\mathsf{rejected}
\}.
$$

允許：

$$
\mathsf{proposed}
\rightarrow
\mathsf{checked}
\rightarrow
\mathsf{certified}
\rightarrow
\mathsf{committed}.
$$

若上游規則失效：

$$
\mathsf{committed}
\rightarrow
\mathsf{invalidated}.
$$

這避免「曾經通過」被誤解為永久有效。

---

# 32. Soundness under rule composition

若：

$$
R_1:x\rightarrow y
$$

sound，且：

$$
R_2:y\rightarrow z
$$

sound，則 composition：

$$
R_2\circ R_1:x\rightarrow z
$$

同樣 task-sound。

形式上：

$$
Q(x)\equiv Q(y),
$$

$$
Q(y)\equiv Q(z),
$$

所以：

$$
\boxed{
Q(x)\equiv Q(z).
}
$$

因此大型 reduction 可由小型 certified rules 組裝。

---

# 33. Contextual soundness

某規則可能只在 context $C[-]$ 中合法。

若：

$$
x\rightarrow y
$$

不代表：

$$
C[x]\rightarrow C[y]
$$

永遠合法。

因此需要 context closure theorem：

$$
\boxed{
x\equiv_{\Gamma,\mathcal Q}y
\Rightarrow
C[x]\equiv_{\Gamma,\mathcal Q}C[y]
}
$$

對允許 context class：

$$
\mathcal C.
$$

若無法證明，rule 必須標記為 context-sensitive。

---

# 34. Domain-sensitive soundness

若 rule：

$$
R
$$

只在：

$$
D_R
\subseteq
\mathcal X_\Gamma
$$

上 sound，則 certificate 必須包含：

$$
x\in D_R.
$$

禁止從：

$$
R\text{ 在某些測試成功}
$$

推出：

$$
R\text{ 全域 sound}.
$$

因此：

$$
\boxed{
\text{Every rule carries an admissible domain.}
}
$$

---

# 35. Counterexample protocol

對每條 proposed rule：

$$
R,
$$

都應主動搜尋：

$$
x\in D_R
$$

使：

$$
Q(x)\not\equiv Q(R(x)).
$$

若找到：

$$
x^\ast,
$$

則：

$$
R
$$

不能以目前 domain 被 certify。

可以：

1. reject；
2. narrow domain；
3. weaken claim；
4. introduce guard condition。

因此：

$$
\boxed{
\text{falsification is part of certification}.
}
$$

---

# 36. Guarded rule

若 rule 只在 guard：

$$
G(x)
$$

成立時 sound，則寫成：

$$
\boxed{
G(x)
\Rightarrow
x\rightarrow_R y.
}
$$

certificate 必須同時證：

$$
G(x)
$$

與：

$$
Q(x)\equiv Q(y).
$$

guard 不得在 reduction 後才被補上。

---

# 37. Termination with guards

guarded rule 可能改變 termination 性質。

因此 measure 必須對所有可執行 rule 都下降：

$$
G_i(x)
\land
x\rightarrow_{R_i}y
\Rightarrow
\mu(y)\prec\mu(x).
$$

不能只證明「大多數 rule」下降。

---

# 38. Confluence under guards

critical pair 分析也必須考慮：

$$
G_i(x)\land G_j(x).
$$

只有兩個 guard 同時成立時，才構成真實 overlap。

因此：

$$
\operatorname{Crit}(R_i,R_j)
$$

應記為：

$$
\boxed{
\{x:
G_i(x)\land G_j(x)\land
R_i,R_j\text{ overlap at }x
\}.
}
$$

---

# 39. Non-confluent but sound systems

一個系統可以：

$$
\text{sound}
$$

但：

$$
\text{non-confluent}.
$$

這表示所有 reduction 都保真，但最後 representation 依賴路徑。

此時可以採：

$$
\boxed{
\text{equivalence-class output}
}
$$

而不是單一 representative。

只要：

$$
A\equiv_{\Gamma,\mathcal Q}B,
$$

兩條路徑仍可視為 proof-equivalent。

---

# 40. Confluent but unsound systems

相反地，一個系統可以所有路徑都到同一 normal form，但該 normal form 根本不保存原命題。

因此：

$$
\boxed{
\text{Confluence}
\not\Rightarrow
\text{Soundness}.
}
$$

也：

$$
\boxed{
\text{Termination}
\not\Rightarrow
\text{Soundness}.
}
$$

三者必須分開驗證。

---

# 41. Reliability vector

對一個 SECV system，可定義：

$$
\boxed{
\mathbf R
=
(
S,
T,
C,
K
)
}
$$

其中：

$$
S\in\{0,1,\mathsf{unknown}\}
$$

代表 soundness；

$$
T
$$

代表 termination status；

$$
C
$$

代表 confluence status；

$$
K
$$

代表 canonicalization status。

例如：

$$
\mathbf R
=
(
1,1,0,0
)
$$

表示 sound 且 terminating，但 non-confluent 且無 canonical normal form。

---

# 42. Proof strength labels

本文建議實作標記：

$$
\mathsf{L0}=\text{heuristic only},
$$

$$
\mathsf{L1}=\text{locally sound},
$$

$$
\mathsf{L2}=\text{globally sound finite chain},
$$

$$
\mathsf{L3}=\text{sound + terminating},
$$

$$
\mathsf{L4}=\text{sound + terminating + confluent},
$$

$$
\mathsf{L5}=\text{canonical certified normal form}.
$$

這使不同 SECV 結果可以直接比較可信度。

---

# 43. Canonical commit

只有在：

$$
S=1
$$

且所有必要 certificates 通過時，結果才可以 commit 到 canonical source。

若 task 另外要求 termination/confluence，則必須達到相應 level。

因此：

$$
\boxed{
\text{validate first, commit second}.
}
$$

---

# 44. Formal commit condition

定義：

$$
\operatorname{Commit}(X)
$$

成立若：

$$
\operatorname{Sound}(X)=1,
$$

$$
\operatorname{CertComplete}(X)=1,
$$

以及任務指定的：

$$
\operatorname{TermReq}(X),
$$

$$
\operatorname{ConfReq}(X)
$$

皆滿足。

因此 commit 本身也是形式判定，而不是人工感覺。

---

# 45. Replayability

完整 proof trace：

$$
\Pi
=
(
x_0,
R_1,\pi_1,
x_1,
R_2,\pi_2,
\ldots,
x_n
)
$$

必須可 replay。

Replay 時重新檢查：

$$
\pi_k
$$

與 rule version。

若 replay 失敗：

$$
\Pi
$$

不得再被視為 certified canonical proof。

---

# 46. Deterministic replay

為提高可重現性，可將：

$$
\text{rule ordering},
$$

$$
\text{canonical representative selection},
$$

$$
\text{tie-breaking}
$$

全部固定。

此時即使底層搜尋可平行，commit 階段仍可產生 deterministic trace。

---

# 47. Parallel execution 與 serial commit

多個候選 reduction：

$$
R_1,\ldots,R_k
$$

可以平行 check。

但若彼此修改重疊符號域，正式 commit 需要 conflict resolution。

因此推薦：

$$
\boxed{
\text{Parallel Propose/Check}
+
\text{Serial Certified Commit}.
}
$$

或使用可證明 commutative 的批次 transaction。

---

# 48. Transactional reduction

可將一批互不衝突的 reduction：

$$
B
=
\{R_{i_1},\ldots,R_{i_m}\}
$$

組成 atomic batch。

若所有 rules pairwise commute 且 certificates 完整，則：

$$
X
\overset{B}{\longrightarrow}
Y
$$

可一次 commit。

任何一個 certificate 失敗則：

$$
\boxed{
\text{abort whole batch}.
}
$$

---

# 49. Proof ledger

每次 commit 記錄：

$$
L_k
=
(
\text{state hash},
\text{rule-set hash},
\text{certificate hash},
\text{parent hash}
).
$$

形成：

$$
L_0\rightarrow L_1\rightarrow\cdots\rightarrow L_n.
$$

這可作為形式 proof ledger。

其目的不是區塊鏈，而是確保 provenance 不被後續編輯偷偷改寫。

---

# 50. Minimal trusted core

實作時不應讓所有 heuristic code 都進入 trusted computing base。

理想架構：

$$
\boxed{
\text{large untrusted proposer}
+
\text{small trusted verifier}.
}
$$

proposer 可以是：

$$
\text{AI},
\text{search},
\text{CAS},
\text{heuristic engine}.
$$

verifier 只檢查 certificate。

這是 SECV 最適合計算機化的架構之一。

---

# 51. Proof-carrying elimination

每個 reduction 不是輸出：

$$
y
$$

而是輸出：

$$
\boxed{
(y,\pi).
}
$$

其中：

$$
\pi
$$

證明：

$$
x\rightarrow y
$$

合法。

因此 SECV runtime 可以被理解為：

$$
\boxed{
\text{proof-carrying symbolic reduction}.
}
$$

---

# 52. 反例：soundness 失敗

假設：

$$
x+y=10.
$$

若錯誤地認為：

$$
x\sim y
$$

然後 quotient：

$$
x,y\rightarrow z,
$$

得到：

$$
2z=10.
$$

這只代表特殊子域：

$$
x=y,
$$

而不是原問題。

若 $\Gamma$ 沒有：

$$
x=y,
$$

這個 reduction 就不 sound。

---

# 53. 反例：termination 失敗

令：

$$
R_1:x\rightarrow 1-x,
$$

$$
R_2:x\rightarrow 1-x.
$$

則：

$$
x
\rightarrow
1-x
\rightarrow
x
\rightarrow
1-x
\rightarrow\cdots
$$

若系統沒有 cycle detection，將永不停止。

正確處理應 quotient orbit：

$$
\{x,1-x\}.
$$

---

# 54. 反例：confluence 失敗

若：

$$
R_1:x\rightarrow a,
$$

$$
R_2:x\rightarrow b,
$$

且：

$$
a
$$

與：

$$
b
$$

都已 irreducible，而且：

$$
a\not\equiv b,
$$

則系統 non-confluent。

此時：

$$
x
$$

沒有唯一 residual semantics。

除非限制 rule priority 或修正 rule set。

---

# 55. Rule priority 不等於 confluence

可以規定：

$$
R_1\succ R_2
$$

總是先用 $R_1$。

這會讓執行 deterministic。

但：

$$
\boxed{
\text{deterministic}
\neq
\text{confluent}.
}
$$

它只是選定其中一條路。

如果另一條合法路徑產生不同語義，soundness 問題仍存在。

---

# 56. Strategy-dependent normal form

若系統 non-confluent，但固定策略：

$$
\sigma
$$

可得到唯一輸出：

$$
\operatorname{NF}_\sigma(x).
$$

此時必須標記：

$$
\boxed{
\text{strategy-relative normal form}.
}
$$

不能稱 universal canonical form。

---

# 57. Soundness theorem schema

對特定 SECV 系統，可以建立：

$$
\boxed{
\forall x,y\in\mathcal X_\Gamma,
\quad
x\rightarrow y
\Rightarrow
x\equiv_{\Gamma,\mathcal Q}y.
}
$$

一旦成立，任何有限 reduction chain 都自動 global sound。

這應該是每個領域化 SECV runtime 的第一個主定理。

---

# 58. Termination theorem schema

若存在 well-founded：

$$
(W,\prec)
$$

與：

$$
\mu:\mathcal X_\Gamma\rightarrow W
$$

使：

$$
x\rightarrow y
\Rightarrow
\mu(y)\prec\mu(x),
$$

則：

$$
\boxed{
\rightarrow
\text{ terminates}.
}
$$

這是第二個主定理模板。

---

# 59. Confluence theorem schema

若已證 termination，再證所有 critical pairs joinable：

$$
\forall (y_1,y_2)\in\operatorname{Crit},
\quad
y_1\downarrow y_2,
$$

則可推得：

$$
\boxed{
\text{confluence}
}
$$

在符合相應 rewrite-theoretic條件時成立。

這是第三個主定理模板。

---

# 60. Canonical normal-form theorem schema

若：

$$
\text{sound}
+
\text{terminating}
+
\text{confluent}
+
\text{deterministic canonicalization},
$$

則：

$$
\boxed{
\forall x,
\quad
\operatorname{CNF}(x)
\text{ 唯一到語義等價}.
}
$$

此時：

$$
\operatorname{CNF}
$$

才有資格成為後續 generative seed extraction 的穩定輸入。

---

# 61. 與生成種子的接口

Paper 05 將從：

$$
\operatorname{CNF}(x)
$$

或：

$$
\Sigma_\star
$$

開始問：

$$
\boxed{
\text{這個 residual 是否保留足夠生成能力？}
}
$$

若 reduction sound 但資訊刪除過度，residual 可能只能回答 $\mathcal Q$，卻無法重新展開原問題域。

因此：

$$
\boxed{
\text{proof sufficiency}
\neq
\text{generative sufficiency}.
}
$$

這正是下一篇的核心。

---

# 62. 非主張

本文不主張：

1. 所有 SECV rule system 都 terminating；
2. 所有 terminating system 都 confluent；
3. 所有 confluent system 都 sound；
4. 所有 sound reduction 都能產生 canonical normal form；
5. heuristic discovery 本身等於 proof；
6. rule priority 可以取代 confluence proof；
7. finite local tests 可以取代全域 soundness；
8. 無限 reduction chain 可直接以極限符號閉合。

本文主張的是：

$$
\boxed{
\text{SECV 的每一個正式 reduction 都必須被放入一個可審計的可靠性框架。}
}
$$

---

# 63. 核心原則

本文將合法消除演算濃縮為六條規則：

$$
\boxed{
\textbf{R1: No certificate, no commit.}
}
$$

$$
\boxed{
\textbf{R2: Unknown means non-eliminable.}
}
$$

$$
\boxed{
\textbf{R3: Every rule has a domain.}
}
$$

$$
\boxed{
\textbf{R4: Every proof binds to a frozen rule version.}
}
$$

$$
\boxed{
\textbf{R5: Termination and confluence are separate from soundness.}
}
$$

$$
\boxed{
\textbf{R6: Canonical output requires validated normal-form conditions.}
}
$$

---

# 結論

SECV 若只有「符號可以被消掉」這個直覺，仍不足以構成可靠證明方法。

真正可接受的 symbolic elimination 必須回答：

$$
\boxed{
\begin{aligned}
&\text{為什麼這一步不改變證明義務？}\\
&\text{為什麼 reduction 不會永遠循環？}\\
&\text{如果換一個順序，最後會不會變成另一個答案？}\\
&\text{規則修改後，哪些舊證明需要失效？}\\
&\text{誰負責提出候選，誰負責驗證？}
\end{aligned}
}
$$

因此，SECV 的正式 proof layer 應採：

$$
\boxed{
\text{Propose}
\rightarrow
\text{Certify}
\rightarrow
\text{Commit}
\rightarrow
\text{Replay}
}
$$

並以：

$$
\boxed{
\text{Soundness}
+
\text{Termination}
+
\text{Confluence}
}
$$

作為三個互相獨立、不能混同的可靠性維度。

只有當這些條件被明確證明或明確標記尚未證明時，符號消除才從「技巧」升格為真正可審計、可重播、可計算機執行的合法演算。

下一篇將進入系列的第二個重大轉折：當 reduction 已經得到穩定 residual 後，如何判斷它不只是「剩下來的東西」，而是真正能重新展開整個問題域的生成種子。