任意字長的parity invariant

目標與範圍

Σ={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

逐步主鏈

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

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

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

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

w=\varepsilon

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

I(w),\quad w'=w0

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

I(w),\quad w'=w1

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

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

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

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

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

w=1011,\quad v=1010

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

局部子步與引理

本稿無局部子步。

逐步反向審查

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