# 完整DFA的1011追蹤

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

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

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



## 目標與範圍

指定DFA拒絕1011，並接受空字ε。

完整Q×Σ決定總表與有限word trace，不由幾條trace推language equivalence。





## 已知條件與符號


- calc


- G1 — Q={E,O}，Σ={0,1}，start=E，finals={E}；δ(E,0)=E,δ(E,1)=O,δ(O,0)=O,δ(O,1)=E。word=1011。


- \delta^* — 整字迭代轉移
- i — 已讀符號數





## 規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。


- calc · prerequisite — 假設有限集合、有限字串與索引、逐步函數更新及自然數歸納；ε表示長度0字串。
- mko_definition · cited — 完整核 Q×Σ 每一輸入恰有一個合法輸出；依序追蹤完整有限 word。空字被接受，當且僅當初始狀態屬於接受狀態集合。一組有限 trace 本身不能證明與任意未指定目標語言的等價，也不能證明該未指定目標語言的 regularity。 · mko-finite-automaton





## 逐步主鏈

S01 · implies操作前

Q=\{E,O\},\quad\Sigma=\{0,1\}

操作後

\begin{array}{c|cc}\delta&0&1\\\hline E&E&O\\O&O&E\end{array}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

四個Q×Σ輸入各恰有一個Q內輸出，完整核total與deterministic。



S02 · implies操作前

w=1011,\quad q_0=E

操作後

(q,i)=(E,0)

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

初始化為唯一start，位置0表示尚未讀任何符號。



S03 · implies操作前

(E,0),\quad w_1=1

操作後

(O,1)

條件：無

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

葉節點依據：calc

讀首個1依δ(E,1)=O，位置增加1。



S04 · implies操作前

(O,1),\quad w_2=0

操作後

(O,2)

條件：無

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

葉節點依據：calc

第二符號0使O保持O，仍然確實消耗此符號。



S05 · implies操作前

(O,2),\quad w_3=1

操作後

(E,3)

條件：無

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

葉節點依據：calc

第三個1翻回E，此時尚有一個1未讀。



S06 · implies操作前

(E,3),\quad w_4=1

操作後

(O,4),\quad4=|w|

條件：無

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

葉節點依據：calc

末個1送到O，全部四符號依序消耗完。



S07 · implies操作前

\delta^*(E,1011)=O,\quad F=\{E\}

操作後

O\notin F\Rightarrow1011\text{ rejected}

條件：無

規則：mko_definition · 依賴：G1, S06

葉節點依據：mko_definition

完整決定run的末狀態非final，因此拒絕此word。



S08 · implies操作前

w=\varepsilon,\quad|w|=0

操作後

\delta^*(E,\varepsilon)=E\in F\Rightarrow\varepsilon\text{ accepted}

條件：無

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

葉節點依據：calc

空字不走轉移，start就是末狀態，故接受。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S01, S07 — 沒有添加ε邊；空字語義與ε transition是不同概念。
- S07 · premise_audit · G1, S06 — 這是指定word的完整證書，不是任意目標language的equivalence證明。
- S06 · premise_audit · G1, S01, S05 — 不能在S05的E提前停住而丟棄末字。
- S05 · premise_audit · G1, S01, S04 — 中途到final不代表整個word已接受。
- S04 · premise_audit · G1, S01, S03 — 狀態不變不代表ε move，位置仍從1到2。
- S03 · premise_audit · G1, S01, S02 — 只有一個合法後繼，不能選擇留E。
- S02 · premise_audit · G1, S01 — start雖final仍不能略過非空word後續輸入。
- S01 · premise_audit · G1 — 沒有ε transition，也沒有同格多分支。





## 錯誤控制與反例

總表四個Q×Σ格皆要合法唯一輸出。

讀完輸入接受檢查只在位置等於word長度後執行。


- 中途E出現便接受1011。 → reject — 尚有末個1，完整末態是O。
- 讀0不變狀態表示不消耗輸入。 → reject — DFA每次讀一個符號，位置仍增加。
- ε需要額外ε transition才接受。 → reject — 空字不走任何邊，start E已final。





## 結論與限制

指定DFA拒絕1011，並接受空字ε。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: c631c60e2976f05f20ff82cd04318bc5c870bf60c51efcfb4bf34202ec0524b1
- original source SHA-256: 1b4e2cc34b16b6214d69dfde3f776b2089abe1dec7d7ab3534bf2cf53e8d3aae
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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