# NFA到DFA的子集合構造

以epsilon-NFA狀態子集合為DFA狀態，start、transition與acceptance按epsilon closure定義即可保持語言。

mko-subset-construction-nfa-to-dfa · theorem · v0.10.0



## 數學敘述

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。





## 代表公式（精確 TeX）

D(S,a)=E(M(S,a))





## 成立條件


- 來源epsilon-NFA使用完整finite states、alphabet與transition relation；null表示不消耗input的epsilon。
- 所有subset canonical排序且每次symbol move之後重新取epsilon closure；trace從epsilon-closed start開始。





## 符號作用域


- D — DFA子集合轉移
- S — NFA狀態子集合
- a — 輸入符號
- E — epsilon closure
- M — symbol move





## 直觀、定義與常見誤解

start subset必須先封閉epsilon reachability。

每個symbol transition採move後epsilon closure。

prefix invariant而非有限accept/reject samples支撐一般language equivalence。

省略epsilon closure、把empty subset刪掉卻不處理dead transition，或由有限測試字串宣稱語言等價。





## 已採用的推導導讀

[epsilon-NFA的完整reachable subset DFA](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-subset-construction-nfa-to-dfa-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [非確定有限自動機](https://ocme.evemisslab.com/zh-Hant/mko/mko-nondeterministic-finite-automaton/) — epsilon-NFA語義。
- [確定有限自動機](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-automaton/) — 目標DFA結構。
- [子集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-subset/) — powerset states與dead empty subset。





## 驗證界線

本輪exact traces核對任意給定word；一般等價依prefix induction，不由測試樣本數量成立。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

加入正規表示式等價與automata minimization。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/subset-construction-nfa-to-dfa.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-subset-construction-nfa-to-dfa/index.md)