Operator-Native RDSS：Literature-Bounded HHP 與 Cause-Sensitive Verification Lattice

Separating Exact Bounded Backtracking Semantics from Runtime Approximation

版本： v0.15 Working Verification Draft
日期： 2026-08-10
作者：Neo.K
機構：EveMissLab／一言諾科技有限公司
定位： bounded HHP 定義校正／Cause-Sensitive CBHHP 實作／Verification Grade 多軸化
前置： ON-RDSS v0.13–v0.14

摘要

v0.14 提出 ON-RDSS Runtime bounded checker：

BHHP_k

並以 recursive rollback-depth 的方式建立：

BHHP_0=HP.

本版重新核對 Fröschle–Hildebrandt 1999 / Hildebrandt dissertation 原始 bounded-backtracking 定義後，進行一個重要命名修正。

文獻中的：

\boxed{ (n)\text{-HHPB} }

是：

將 HHPB 的 backtracking requirement 限制到 run 尾端最近的 $n+1$ transitions。

原文正式條件使用：

last(r,t)\ge |r|-n.

因此：

\boxed{ (0)\text{-HHPB}=HPB. }

而且：

\boxed{ HHPB \subseteq \cdots \subseteq (n+1)\text{-HHPB} \subseteq (n)\text{-HHPB} \subseteq \cdots \subseteq HPB. }

文獻並構造對每個 $n$ 都存在：

(n)\text{-HHPB}

但非：

(n+1)\text{-HHPB}

的有限 nets。

因此本版正式區分：

\boxed{ LitHHP_n }

與：

\boxed{ RBHHP_k. }

前者指文獻 bounded semantics；

後者指 ON-RDSS v0.14 的 recursive runtime verification grade。

除非後續完成形式等價證明，不再混用兩者。

1. 文獻 $(n)$ -HHPB

對 synchronous run：

r

與 backtrack-enabled transition：

t,

文獻 $(n)$ -hereditary condition 要求：

只有當：

\boxed{ last(r,t)\ge |r|-n }

時才強制 backtracking closure。

也就是只允許檢查 run 尾端最近：

\boxed{ n+1 }

個位置的 removable transitions。

2. 文獻 indexing

因此：

\boxed{ LitHHP_0=HP. }

LitHHP_1

比 HP 多一層尾端 backtracking sensitivity。

一般：

\boxed{ LitHHP_{n+1} \subseteq LitHHP_n. }

而：

\boxed{ HHP = \bigcap_{n\ge0} LitHHP_n. }

3. Strict Hierarchy

文獻 Figure 6.2 提供一個參數化 net family：

N_n, N_n'

使：

\boxed{ N_n \sim_{LitHHP_n} N_n' }

但：

\boxed{ N_n \not\sim_{LitHHP_{n+1}} N_n'. }

因此：

\boxed{ LitHHP_n }

hierarchy 對所有有限 $n$ 都是 strict。

4. Strictness 的機制

文獻的 generic counterexample 具有：

a_1,\ldots,a_n,

b_1,\ldots,b_n

等長歷史，

在 critical：

a_{n+1}',b_{n+1}'

處可以選兩種匹配方式。

若選一種，

需要回退所有 $a$ histories 才會暴露：

d

mismatch。

若選另一種，

需要回退所有 $b$ histories 才會暴露：

c

mismatch。

$(n)$ -bounded backtracking 看不到足夠深，

但：

(n+1)

可以。

5. ON-RDSS v0.14 的 RBHHP

v0.14 定義：

\boxed{ RBHHP_0=HP }

並以：

current-level forward matching + 一步 rollback 到前一級 relation

遞迴建立：

RBHHP_{k+1}.

這與「增加可追溯歷史深度」有相同設計直覺，

但目前未證：

\boxed{ RBHHP_k = LitHHP_k. }

6. 為何保留 RBHHP？

RBHHP 有工程優勢：

greatest-fixed-point implementation 直接；
certificate 可以遞迴記錄 level；
incremental cache 容易；
可以與 CauseSensitive mapping 共用 engine。

所以它仍是一個有用 Runtime grade。

但其名稱應保持：

\boxed{ RuntimeBoundedHHP }

而非冒充 literature definition。

7. Literature Grade 與 Runtime Grade

正式分：

\boxed{ VerificationFamily \in \{ LiteratureBounded, RuntimeRecursive, FullHHP \}. }

Certificate 必須說明 family。

8. Cause-Sensitive CBHHP

General CEES runtime state：

\boxed{ \widehat C = (C,\pi,\le_\pi,v). }

concrete causal realization：

\boxed{ \widetilde e=(e,\kappa,v). }

本版完成第一個 Cause-Sensitive bounded checker。

9. Cause-Sensitive Forward Matching

對：

\widehat C_1 \xrightarrow{(e_1,\kappa_1)} \widehat C'_1,

另一邊需：

\widehat C_2 \xrightarrow{(e_2,\kappa_2)} \widehat C'_2

並滿足：

\boxed{ Profile(e_1)=Profile(e_2) }

以及：

\boxed{ f(\kappa_1)=\kappa_2. }

因此不是只有 output/event label matching。

10. Cause-Sensitive Backward Matching

只有 causal-maximal occurrence：

\widetilde e

可直接回退。

若 current realization map：

f_r

已建立，

另一邊必須回退：

\boxed{ f_r(\widetilde e). }

不能重新挑另一個同 surface label occurrence。

11. $CBHHP_0$

定義：

\boxed{ CBHHP_0 }

為 cause-sensitive forward HP-like relation。

它要求：

profile-preserving realization history isomorphism；
chosen witness correspondence；
forward back-and-forth。

12. $CBHHP_{k+1}$

ON-RDSS Runtime recursive版本：

\boxed{ CBHHP_{k+1} }

再加一層沿 realization mapping 的 causal-maximal rollback obligation落入：

CBHHP_k.

13. Surface vs Cause-Sensitive 分離實驗

General CEES：

\varnothing\vdash a,

\varnothing\vdash b,

\{a\}\vdash c,

\{b\}\vdash c.

兩 histories：

\widehat C_A: c\text{ uses }\{a\},

\widehat C_B: c\text{ uses }\{b\}.

兩者 raw surface event set 完全一樣：

\boxed{ C_A=C_B=\{a,b,c\}. }

14. 但 Cause 不同

\boxed{ a<_{\pi_A}c, }

而：

\boxed{ b<_{\pi_B}c. }

所以：

\boxed{ SameSurfaceState=true, }

但：

\boxed{ SameCausalOrder=false. }

15. Governance-Distinct Sources

若：

Profile(a) = (A,source.A),

Profile(b) = (B,source.B),

則 checker：

\boxed{ CBHHP_0(\widehat C_A,\widehat C_B)=false. }

因此：

\boxed{ SurfaceEquality \not\Rightarrow CauseSensitiveEquivalence. }

16. CauseMode 是非冗餘軸

這直接證明：

\boxed{ CauseMode \in \{ Surface, CauseSensitive \} }

不是多餘 metadata。

它真的會改變 equivalence result。

17. Profile-Relative Cause Quotient

如果刻意令：

Profile(a)=Profile(b),

則兩 histories 可以藉由：

a\leftrightarrow b

互換形成 causal isomorphism。

Checker：

\boxed{ SymmetricProfile\ CBHHP_0=true. }

因此：

\boxed{ CauseSensitive }

也仍然 relative to chosen event-profile regime。

18. 三軸 Verification Grade

目前可以寫：

\boxed{ VG = ( HistoryFamily, CauseMode, GovernanceMode ). }

19. HistoryFamily

\boxed{ HistoryFamily \in \{ HP, LitHHP_n, RBHHP_k, FullHHP \}. }

20. CauseMode

\boxed{ CauseMode \in \{ Surface, CauseSensitive \}. }

21. GovernanceMode

\boxed{ GovernanceMode \in \{ BehaviourOnly, Authority, Authority+Residual, FullGoverned \}. }

22. Verification Grade 是 Partial Order

例如：

(RBHHP_2,Surface,FullGoverned)

和：

(RBHHP_1,CauseSensitive,BehaviourOnly)

不能單靠一個整數說誰更強。

因此：

\boxed{ VG }

應視為多軸偏序。

23. Grade Certificate

\boxed{ VQCert = ( Family, Depth, CauseMode, GovernanceMode, Scope, EventVersion, OperatorVersion, CheckerVersion, WitnessHash ). }

24. Forget Cause

若：

Surface(\widehat C_1) = Surface(\widehat C_2)

但：

CauseSensitiveEq=false,

則：

\boxed{ ForgetCause }

不能是 silent operation。

需：

\boxed{ ForgetCauseCert. }

25. Cause-Sensitive Residual

若 Runtime 只做 surface quotient，

但 caller 要求 causal provenance，

可輸出：

\boxed{ Residual[ CauseEquivalenceUnchecked ]. }

若 causal check 直接失敗：

\boxed{ Residual[ CauseHistoriesDiverge ]. }

26. Meta 與 CauseMode

Meta 可能改：

Alt_v(e).

所以舊：

CBHHP_k^v

certificate 在：

v+1

必須 stale。

因為 causal realization space：

Real_v(C)

本身已改變。

27. Maximal Causes 與 Runtime Index

文獻的 bounded-HHP decidability proof 指出：

要維持新增 event 後的 pomset isomorphism，不必永遠保存全部過去；保存可作為新事件 maximal causes 的最近歷史即可。

這對 ON-RDSS 很重要。

可以定義：

\boxed{ CauseFrontier(C) = \text{potential maximal causes}. }

作為快速 index。

28. CauseFrontier 不等於 Full History

\boxed{ CauseFrontier = Index(History). }

它有利於：

incremental type/effect check；
future event matching；
bounded verification。

但 authority source 仍是完整 history / certificate ledger。

29. 與 GCMS / History Compression 類型問題的接口

抽象來說，history memory 可壓成：

M_t

只要對指定 query / verification mode 保持足夠資訊。

對 bounded HHP，

一個自然 query 就是：

哪些 past events 仍可能成為未來 extension 的 maximal causes或 backtracking targets？

因此可研究：

\boxed{ HistoryCompression_{VG} }

相對 verification grade 的最小充分記憶。

30. 文獻 Strict-Hierarchy Fixture Family

下一步不需要再自行猜 $k=2$ fixture。

文獻已給：

\boxed{ Fixture_n^{Lit} }

使：

LitHHP_n=true,

LitHHP_{n+1}=false.

所以應把 Figure 6.2 的參數化 net family正式翻譯成 machine-readable benchmark。

31. Figure 6.2 翻譯工作的限制

目前文字解析已足以確認：

generic $a_i,b_i$ history；
critical $a_{n+1},b_{n+1}$ / alternative matching；
backtrack all $a$ exposes $d$ ；
backtrack all $b$ exposes $c$ ；
strictness theorem。

但圖的精確 place/arc 拓撲仍需可靠讀圖／人工轉錄後再寫 checker。

在完成此步前，不自行捏造 Petri-net arcs。

32. 新的 Verification Backend 分層

Fast Index

current projection；
profile hash；
CauseFrontier；
bounded future summary。

Runtime Strong Check

RBHHP $_k$ ；
CBHHP $_k$ 。

Literature-Compatible Formal Check

LitHHP $_n$ ；
full HHP。

Offline Proof

event-structure / Petri-net theorem prover；
future Lean/Coq formalization。

33. 暫定結論

本版最重要的不是再增加一個 $k$ 。

而是把「bounded history equivalence」拆成兩個不能混淆的東西：

\boxed{ LitHHP_n }

是有明確文獻定義與 strict hierarchy theorem 的 bounded-backtracking semantics。

\boxed{ RBHHP_k }

是 ON-RDSS 為 Runtime 設計的 recursive verification grade。

同時：

\boxed{ CBHHP_k }

證明 CauseMode 是一條真正獨立的 verification axis。

所以 ON-RDSS 的 state-equivalence certificate 現在最合理的形式不是：

Equivalent=true.

而是：

\boxed{ Equivalent[ Family, Depth, CauseMode, GovernanceMode, Scope, Version, Cert ]. }

這讓「同一個 State」從一個含糊判斷，變成一個可追溯的、分域的、分強度的驗證聲明。

ON_RDSS_Literature_Bounded_HHP_CauseSensitive_Lattice_v0.15