epsilon-NFA的完整reachable subset DFA

目標與範圍

完整列轉移並以prefix induction證語言等價。

只保留reachable subsets，明確包含empty dead state。

已知條件與符號

• work

• G1 — Q={0,1,2}，Σ={a,b}，start=0，finals={2}。完整NFA表：(0,ε)={1}，(1,a)={1}，(1,b)={2}；其餘所有(q,s)∈Q×{ε,a,b}轉移為空。

• S,A,F,D — 四個reachable subsets
• R_N(w) — NFA讀w後封閉可達集

規則與來源

• mko_definition · cited — DFA start state是epsilon-closure({q0})。對subset S與symbol a，delta_D(S,a)=epsilon-closure(move(S,a))；accepting subset恰與NFA final-state set有非空交集。empty subset是合法dead state，可只保留reachable subsets但須明示。任意word invariant是DFA讀完每個prefix的subset恰等於NFA所有epsilon-closed reachable states；有限words測試不足以證language equivalence。 · mko-subset-construction-nfa-to-dfa
• work · prerequisite — epsilon-closure包含零次與有限次epsilon步；move合併全部active states的symbol後繼；word長度歸納與DFA/NFA接受定義。

逐步主鏈

\operatorname{cl}_\varepsilon(\{0\})

S=\{0,1\}\text{ is the DFA start}

\delta_D(S,s)=\operatorname{cl}_\varepsilon(\operatorname{move}(S,s))

\delta_D(S,a)=A=\{1\},\quad\delta_D(S,b)=F=\{2\}

A=\{1\}

\delta_D(A,a)=A,\quad\delta_D(A,b)=F

F=\{2\}

\delta_D(F,a)=D=\varnothing,\quad\delta_D(F,b)=D

D=\varnothing

\delta_D(D,a)=D,\quad\delta_D(D,b)=D

S\xrightarrow{a}A,\ S\xrightarrow{b}F,\ S\xrightarrow{ba}D

Q_D=\{S,A,F,D\},\quad F_D=\{F\}

w=\varepsilon

\delta_D^*(S,\varepsilon)=S=\operatorname{cl}_\varepsilon(\{0\})=R_N(\varepsilon)

\delta_D^*(S,w)=R_N(w),\quad s\in\Sigma

\delta_D^*(S,ws)=\operatorname{cl}_\varepsilon(\operatorname{move}(R_N(w),s))=R_N(ws)

\delta_D^*(S,w)\cap\{2\}\ne\varnothing\iff R_N(w)\cap\{2\}\ne\varnothing

L(D)=L(N)

局部子步與引理

本稿無局部子步。

逐步反向審查

• S09 · premise_audit · G1, S08, work — 沒有以幾個測試words替代歸納證明。
• S08 · premise_audit · G1, S07, work — w任意、s兩種皆涵蓋，因此是全word induction。
• S07 · premise_audit · G1, S06, work — R_N表示讀完prefix後所有epsilon-closed可達states。
• S06 · premise_audit · G1, S05, work — 接受條件是與{2}交集非空，不是subset等於全部finals的一般規則。
• S05 · premise_audit · G1, S04, work — 刪empty state又不處理incoming dead transitions會不完整。
• S04 · premise_audit · G1, S03, work — 接受subset也必須有完整DFA轉移。
• S03 · premise_audit · G1, S02, work — 沒有epsilon邊離開1，封閉仍是單點。
• S02 · premise_audit · G1, S01, work — NFA原表所有states均納入move，不只任選一路。
• S01 · premise_audit · G1, work — 只從{0}起步會漏a與b的路徑。

錯誤控制與反例

closure次序

起始先closure，每次move後再closure。

完整八轉移

四reachable states各有a、b兩轉移。

• DFA start={0}。 → reject — 0可epsilon到1，故應{0,1}。
• empty subset不是合法state。 → reject — 它表示所有NFA分支都消失，且是total DFA所需dead state。
• 測過a、b就證完整等價。 → reject — 完整等價由任意prefix induction，不由有限tests。

結論與限制

reachable DFA共有四state、八轉移，與原epsilon-NFA對所有words等價。

驗證及來源綁定

2 個本稿宣告算術檢查；只支持所列算式。

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 66fd6e76217271463939e2074eb9e586f0571bdfa596621064cb082086e08ad0
• original source SHA-256: 66fd6e76217271463939e2074eb9e586f0571bdfa596621064cb082086e08ad0
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

同源完整 JSON（含公式、AST、反控制與修訂記錄）