# 非確定有限自動機

epsilon-NFA以狀態、input symbol或epsilon對應可能後繼集合，存在一條full-input final path即接受。

mko-nondeterministic-finite-automaton · definition · v0.10.0



## 數學敘述

transition序列固定[from_state,input_symbol_or_null,to_state]；null是epsilon且不消耗input。states因含start而nonempty；alphabet與final-state set都允許empty。relation可empty或multi-valued，不要求deterministic/total。empty word可經finite epsilon path接受；empty final set合法並辨識empty language。一條finite accepting path證membership；bounded search failure不證rejection。epsilon cycle本身不接受，也不要求all branches接受。





## 代表公式（精確 TeX）

N(Q,S)





## 成立條件


- states nonempty；states與alphabet finite、unique且disjoint；alphabet及final states可empty。
- path configuration=[state,input_position]，接受需完整消耗input並位於final state。





## 符號作用域


- N — epsilon-NFA
- Q — 有限狀態集
- S — input alphabet





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

epsilon closure不消耗input。

acceptance是existential finite path。

bounded failure與dead branches不否定其他path；epsilon cycle若不到final仍不接受。

要求all branches accept、讓epsilon consume input，或把epsilon cycle當acceptance。





## 已採用的推導導讀

[NFA的existential有限路徑](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-nondeterministic-finite-automaton-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [確定有限自動機](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-automaton/) — finite control。
- [二元關係與集合投影](https://ocme.evemisslab.com/zh-Hant/mko/mko-relation/) — multi-valued transition relation。
- [子集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-subset/) — successor state subsets。





## 驗證界線

本輪不宣稱DFA equivalence或subset construction theorem。

not_formalized

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





## 下一個義務

加入NFA-to-DFA subset construction。





## 同源結構化資料

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

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/nondeterministic-finite-automaton.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-nondeterministic-finite-automaton/index.md)