# NFA的existential有限路徑

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-nondeterministic-finite-automaton/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-nondeterministic-finite-automaton-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

指定NFA接受aab，即使另一分支dead；epsilon loop本身不接受。

完整finite relation，null不耗輸入；不推DFA等價或subset theorem。





## 已知條件與符號


- calc


- G1 — Q={q0,q1,qf,qd}，Σ={a,b}，start q0，finals{qf}；全部edges為[q0,null,q1],[q0,null,q0],[q0,a,qd],[q1,a,q1],[q1,b,qf],[qd,a,qd],[qd,b,qd]；word aab。


- q_d — 非final dead state
- F — 接受狀態集合
- null — epsilon transition標記





## 規則與來源


- calc · prerequisite — 假設有限集合、有限字串與索引、逐步函數更新及自然數歸納；ε表示長度0字串。
- mko_definition · cited — 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接受。 · mko-nondeterministic-finite-automaton





## 逐步主鏈

S01 · implies操作前

Q\ne\varnothing,\quad Q\cap\Sigma=\varnothing

操作後

\{[q_0,\text{null},q_1],[q_0,\text{null},q_0],[q_0,a,q_d],[q_1,a,q_1],[q_1,b,q_f],[q_d,a,q_d],[q_d,b,q_d]\}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

明列全部七條合法relation；可有epsilon、多分支與缺邊，不要求DFA總決定表。



S02 · implies操作前

w=aab,\quad|w|=3

操作後

[q_0,0]

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

初始化state與已讀位置，尚未消耗a。



S03 · implies操作前

[q_0,0]

操作後

[q_1,0]\text{ via }[q_0,\text{null},q_1]

條件：無

規則：calc · 依賴：G1, S01, S02

葉節點依據：calc

epsilon選擇進入q1，位置不變。



S04 · implies操作前

[q_1,0],\quad w_1=a

操作後

[q_1,1]

條件：無

規則：calc · 依賴：G1, S01, S03

葉節點依據：calc

用a-loop消耗首a，state留q1。



S05 · implies操作前

[q_1,1],\quad w_2=a

操作後

[q_1,2]

條件：無

規則：calc · 依賴：G1, S01, S04

葉節點依據：calc

同一合法loop讀第二a。



S06 · implies操作前

[q_1,2],\quad w_3=b

操作後

[q_f,3]

條件：無

規則：calc · 依賴：G1, S01, S05

葉節點依據：calc

b-edge消耗末字到final，位置等word長度。



S07 · implies操作前

[q_f,3],\quad q_f\in F,\quad3=|w|

操作後

aab\text{ accepted}

條件：無

規則：mko_definition · 依賴：G1, S02, S03, S04, S05, S06

葉節點依據：mko_definition

存在這條有限讀完路徑就夠，不要求所有分支接受。



S08 · implies操作前

[q_0,0]\xrightarrow{a}[q_d,1]\xrightarrow{a}[q_d,2]\xrightarrow{b}[q_d,3]

操作後

q_d\notin F\text{ on this branch, but the accepting branch still exists}

條件：無

規則：calc · 依賴：G1, S01, S07

葉節點依據：calc

另一條完整分支到dead非final qd，不會否證先前existential接受witness。



S09 · implies操作前

[q_0,0]\xrightarrow{\varepsilon}[q_0,0];\quad F'=\varnothing

操作後

\text{epsilon cycle alone does not accept};\quad F'=\varnothing\text{ is a valid empty-language NFA}

條件：無

規則：calc · 依賴：G1, S01, S07, S08

葉節點依據：calc

loop本身未到final且未讀input；空final集合仍是合法模型，只是不可能滿足末態final。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S09 · premise_audit · G1, S01, S07, S08 — empty alphabet也可合法，例如只含start與final同一state、無edges的NFA接受ε。
- S08 · premise_audit · G1, S01, S07 — 將NFA誤當all-branches接受會錯拒這個word。
- S07 · premise_audit · G1, S02, S03, S04, S05, S06 — 起點、每條邊與終點均已列，不用有界搜尋未命中的推斷。
- S06 · premise_audit · G1, S01, S05 — qf雖沒有輸出邊，接受只需已完成的有限路徑。
- S05 · premise_audit · G1, S01, S04 — 不可直接跳到position3，b仍未讀。
- S04 · premise_audit · G1, S01, S03 — 同state不代表epsilon，這步確實消耗一字。
- S03 · premise_audit · G1, S01, S02 — 不能把epsilon當成讀第一個a。
- S02 · premise_audit · G1, S01 — position0是初始值，不是接受條件。
- S01 · premise_audit · G1 — qf沒有輸出邊仍合法；start必在非空Q。





## 錯誤控制與反例

存在量詞一條完整接受路徑就證membership，dead branches不推拒絕。

epsilon位置null邊位置保持，符號邊才增加1。


- 有一條dead分支就必拒絕aab。 → reject — 已列另一條完整accepting path。
- epsilon cycle本身即接受。 → reject — 仍須有限路徑讀完input並到final。
- NFA必有非空alphabet與final set。 → reject — 本模型容許兩者empty；只要求start使states非空。





## 結論與限制

指定NFA接受aab，即使另一分支dead；epsilon loop本身不接受。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 2f202837026e2fb8c1a908dc18766c8e59c70be3d98e1011ca235aa4e3cd7172
- original source SHA-256: 2f202837026e2fb8c1a908dc18766c8e59c70be3d98e1011ca235aa4e3cd7172
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-nondeterministic-finite-automaton-01.json)