NFA的existential有限路徑

目標與範圍

指定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

逐步主鏈

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]\}

w=aab,\quad|w|=3

[q_0,0]

[q_0,0]

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

[q_1,0],\quad w_1=a

[q_1,1]

[q_1,1],\quad w_2=a

[q_1,2]

[q_1,2],\quad w_3=b

[q_f,3]

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

aab\text{ accepted}

[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}

[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}

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）