OCMEBilingual mathematics & derivations繁體中文

A parity invariant for arbitrary word length

On this page
  1. Goal and scope
  2. Givens and symbols
  3. Rules and sources
  4. Main derivation
  5. Substeps and lemmas
  6. Reverse audits
  7. Error controls and negative controls
  8. Result and limitations
  9. Verification and source binding

← Guide index · Original MKO

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

Goal and scope

All words over {0,1} with an even number of 1s form a regular language.

A complete DFA and an invariant for every prefix; no regex or NFA machinery.

Givens and symbols

  • calc
  • G1 — Q={E,O}, alphabet={0,1}, start E, finals {E}; transitions E0 to E,E1 to O,O0 to O,O1 to E; L consists of words with an even number of 1s.
  • c(w) — number of 1s in the word
  • I(w) — prefix-parity invariant

Rules and sources

  • calc · prerequisite — Assume finite sets, finite strings and indices, stepwise function updates and induction on natural numbers; epsilon denotes the length-zero word.
  • mko_definition · cited — The DFA certificate must cover every finite word over the declared alphabet. Mod-count and parity languages use a state invariant valid for arbitrary word length; a finite language can use a prefix-trie DFA construction. Finitely many tested words do not prove regularity or language equivalence. · mko-regular-language

Main derivation

S01 · implies

Before

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

After

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

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

All four cells have one valid output, so the DFA can read every finite word.

S02 · implies

Before

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

State the universal target invariant: the state records parity of the count of 1s in the prefix.

S03 · induction_base

Before

w=\varepsilon

After

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

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

Base case: the empty word contains zero 1s, an even count, and with no input consumed the automaton remains in state E.

S04 · induction_step

Before

I(w),\quad w'=w0

After

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

Conditions: the induction hypothesis I(w) holds

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Appending 0 preserves both count and state, covering either prior parity.

S05 · induction_step

Before

I(w),\quad w'=w1

After

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

Conditions: the induction hypothesis I(w) holds

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Appending 1 flips both parity and state, matching both cases.

S06 · implies

Before

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

After

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

Conditions: none

Rule: calc · Uses: G1, S03, S04, S05

Leaf basis: calc

Every finite word is formed from epsilon by appending 0 or 1, so induction proves the whole-language invariant.

S07 · implies

Before

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

After

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

Conditions: none

Rule: mko_definition · Uses: G1, S01, S06

Leaf basis: mko_definition

The complete DFA accepts exactly words with even 1-count, a universal recognition certificate for L.

S08 · implies

Before

w=1011,\quad v=1010

After

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

Conditions: none

Rule: calc · Uses: G1, S06, S07

Leaf basis: calc

Two examples illustrate the proven invariant without replacing the proof.

Substeps and lemmas

No substeps in this guide.

Reverse audits

  • S08 · premise_audit · G1, S06, S07 — Many different languages share finite samples, so samples alone cannot certify equivalence.
  • S07 · premise_audit · G1, S01, S06 — Both directions follow from I(w), not merely inclusion of L in the accepted language.
  • S06 · premise_audit · G1, S03, S04, S05 — Induction covers arbitrary length without a test cutoff.
  • S05 · premise_audit · G1, S01, S02 — O1 to E ensures odd plus one becomes even, covering the reverse direction too.
  • S04 · premise_audit · G1, S01, S02 — Both E and O zero-transitions are checked, not only the even case.
  • S03 · premise_audit · G1, S02 — Epsilon is not a character and contributes no symbol count.
  • S02 · premise_audit · G1, S01 — Naming E 'even' is not proof; induction below is required.
  • S01 · premise_audit · G1 — Model qualification alone is not recognition of the specified L; an invariant is still required.

Error controls and negative controls

Universal invariant

Use induction on length, not a finite test list for L.

Both directions

Final state E iff even must cover both acceptance and nonacceptance.

  • Testing lengths at most 4 proves L regular. → reject — A complete DFA invariant for arbitrary length is required; finite samples do not determine a language.
  • Words with an odd number of 1s lie in L. → reject — The invariant ends at nonfinal O, for example word 1.
  • This certificate proves any two DFAs equivalent. → reject — It certifies this DFA and the specified L only.

Result and limitations

All words over {0,1} with an even number of 1s form a regular language.

    Verification and source binding

    0 declared checks for this guide; only the listed expressions are covered.

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

    Same-source full JSON (formulas, ASTs, controls and revision log)