# 任意字長的parity invariant

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

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

derivation-mko-regular-language-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

Σ={0,1}上含偶數個1的全部word構成正規語言。

完整DFA與對任意prefix的歸納不變量；不引入regex或NFA。





## 已知條件與符號


- calc


- G1 — Q={E,O}，Σ={0,1}，start E，finals{E}；轉移E0→E,E1→O,O0→O,O1→E；L={w:1出現偶數次}。


- c(w) — word中1的數量
- I(w) — prefix parity不變量





## 規則與來源


- calc · prerequisite — 假設有限集合、有限字串與索引、逐步函數更新及自然數歸納；ε表示長度0字串。
- mko_definition · cited — DFA certificate須涵蓋宣告alphabet上的任意有限word。mod-count/parity語言以state invariant對任意字長證明；有限語言可用prefix-trie DFA構造。有限測試字不足以證regularity或language equivalence。 · mko-regular-language





## 逐步主鏈

S01 · implies操作前

Q\times\Sigma\text{ has four pairs}

操作後

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

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

完整四格每格一個合法輸出，所以此DFA可讀任意有限word。



S02 · implies操作前

c(w)=\#\{i:w_i=1\}

操作後

I(w):\ \delta^*(E,w)=E\iff c(w)\equiv0\pmod2

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

明示全稱目標不變量：狀態記錄prefix中1數的奇偶。



S03 · induction_base操作前

w=\varepsilon

操作後

c(\varepsilon)=0,\quad\delta^*(E,\varepsilon)=E\Rightarrow I(\varepsilon)

條件：無

規則：calc · 依賴：G1, S02

葉節點依據：calc

歸納基礎：零個1為偶數且未讀字留E。



S04 · induction_step操作前

I(w),\quad w'=w0

操作後

c(w0)=c(w),\quad\delta(E,0)=E,\ \delta(O,0)=O\Rightarrow I(w0)

條件：the induction hypothesis I(w) holds

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

葉節點依據：calc

加0保持計數與狀態，所以兩種原奇偶均保留不變量。



S05 · induction_step操作前

I(w),\quad w'=w1

操作後

c(w1)=c(w)+1,\quad E\xrightarrow{1}O,\ O\xrightarrow{1}E\Rightarrow I(w1)

條件：the induction hypothesis I(w) holds

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

葉節點依據：calc

加1同時翻轉奇偶與狀態，兩種分支均匹配。



S06 · implies操作前

I(\varepsilon),\quad I(w)\Rightarrow I(w0),I(w1)

操作後

\forall w\in\{0,1\}^*:\ I(w)

條件：無

規則：calc · 依賴：G1, S03, S04, S05

葉節點依據：calc

每個有限word由空字逐次加0或1形成，字長歸納完成全語言不變量。



S07 · implies操作前

F=\{E\},\quad\forall w:\ I(w)

操作後

w\text{ accepted}\iff w\in L\Rightarrow L\text{ regular}

條件：無

規則：mko_definition · 依賴：G1, S01, S06

葉節點依據：mko_definition

完整DFA接受恰當偶數1，所以它是L的全稱recognition證書。



S08 · implies操作前

w=1011,\quad v=1010

操作後

c(w)=3\Rightarrow w\notin L;\quad c(v)=2\Rightarrow v\in L

條件：無

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

葉節點依據：calc

兩個例子說明既證不變量，並不代替證明。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S06, S07 — 有限樣本可由很多不同language共享，因此不能單靠樣本宣稱equivalence。
- S07 · premise_audit · G1, S01, S06 — 兩方向都來自I(w)，不僅L包含在接受language。
- S06 · premise_audit · G1, S03, S04, S05 — 任意字長由歸納覆蓋，不依測試長度上限。
- S05 · premise_audit · G1, S01, S02 — 轉移O1→E確保奇數再加1變偶數，不漏反方向。
- S04 · premise_audit · G1, S01, S02 — E與O的0轉移都核到，不能只核even分支。
- S03 · premise_audit · G1, S02 — ε不是字元，所以不計一個1或0。
- S02 · premise_audit · G1, S01 — 只說E代表even是命名，必用下面歸納證。
- S01 · premise_audit · G1 — 此資格只保證模型有效，還需不變量才能認證指定L。





## 錯誤控制與反例

全稱不變量以字長歸納，不以有限測試清單證L。

兩方向末態E iff even，須含接受與不接受兩邊。


- 測完長度≤4便證L正規。 → reject — 需任意字長的完整DFA不變量，有限樣本不決定整個language。
- 含奇數個1也在L。 → reject — 不變量送到非final O，例如word1。
- 此證書自動證兩個任意DFA等價。 → reject — 只認證這一台DFA與明示L。





## 結論與限制

Σ={0,1}上含偶數個1的全部word構成正規語言。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 8b3f94b7386f3cfa6772b2ab39314f3cdfe8dbb931e9468ee42f746ee7293ecb
- original source SHA-256: 1805ff983292495019f5c1345bf8dfe377b3ed25ba222aa28cd86de46fed3f90
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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