# 二元字串偶數1的scan decider

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

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

derivation-mko-turing-machine-decision-model-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

完整machine、trace、ranking與全input正確性。

single-tape deterministic scan schema，不由一條halt trace證total。





## 已知條件與符號


- work


- G1 — Q={E,O,A,R}，input alphabet{0,1}，tape alphabet{0,1,_}，blank=_，start E，accept A，reject R，head初始0。輸入w長m置cells0≤j<m，其餘blank。
- G2 — 完整非halt轉移：[E,0,E,0,R]、[E,1,O,1,R]、[O,0,O,0,R]、[O,1,E,1,R]、[E,_,A,_,S]、[O,_,R,_,S]；halt states A、R沒有outgoing。tuple末位R指right，不是reject state。


- C=[q,h,T] — state、head、sparse tape
- ρ — 全input下降ranking





## 規則與來源


- mko_definition · cited — machine明示finite states、input alphabet、tape alphabet、blank、start、accept、reject及deterministic transition [state,read,next,write,move]，tape未列cells皆為blank。configuration固定[state,head,sparse nonblank tape]。exact step與finite trace只證指定input。全域decider certificate須提供對所有input成立且每步嚴格下降的ranking或明示step bound，並同時有answer correctness。recognizer可在nonmember上loop；bounded simulation failure不證rejection或nontermination，單一halting trace也不證全域decider。 · mko-turing-machine-decision-model
- work · prerequisite — deterministic TM一步語義、有限word按head順序掃描、prefix parity歸納、非負整數嚴格下降ranking保證termination。





## 逐步主鏈

S01 · implies操作前

\{E,O\}\times\{0,1,\_\}

操作後

6\text{ deterministic transitions; A,R terminal}

條件：無

規則：work · 依賴：G1, G2, work

葉節點依據：work

兩個非halt state各三個read symbol全列且single-valued。



S02 · implies操作前

w=101,\quad C_0=[E,0,\{0:1,1:0,2:1\}]

操作後

C_1=[O,1,\{0:1,1:0,2:1\}]

條件：無

規則：work · 依賴：G1, G2, S01, work

葉節點依據：work

在cell0讀1，切O並向右，tape不改。



S03 · implies操作前

C_1=[O,1,\{0:1,1:0,2:1\}]

操作後

C_2=[O,2,\{0:1,1:0,2:1\}]

條件：無

規則：work · 依賴：G1, G2, S02, work

葉節點依據：work

讀0不改parity，head到2。



S04 · implies操作前

C_2=[O,2,\{0:1,1:0,2:1\}]

操作後

C_3=[E,3,\{0:1,1:0,2:1\}]

條件：無

規則：work · 依賴：G1, G2, S03, work

葉節點依據：work

第二個1把parity切回E，head到第一blank。



S05 · implies操作前

C_3=[E,3,T]

操作後

C_4=[A,3,T]\quad\text{accept}

條件：無

規則：work · 依賴：G1, G2, S04, work

葉節點依據：work

E讀blank時stay並accept，這條trace共4步。



S06 · implies操作前

h\text{ input cells scanned}

操作後

q=E\iff\#\{j<h:w_j=1\}\text{ even};\quad q=O\iff\text{odd}

條件：無

規則：work · 依賴：G1, G2, S05, work

葉節點依據：work

空prefix為E；讀0不變、讀1切換，依h歸納證完整parity invariant。



S07 · implies操作前

\rho=m-h+1\text{ in scan states},\quad\rho=0\text{ in A,R}

操作後

\rho\in\mathbb N_0,\quad\rho\text{ strictly decreases at each step}

條件：無

規則：work · 依賴：G1, G2, S06, work

葉節點依據：work

讀bit令h加一；blank時從1降0，所以任意input最多m+1步halt。



S08 · implies操作前

h=m,\quad q=E\text{ iff total ones even}

操作後

\text{accept iff }w\text{ has even ones; reject otherwise}

條件：無

規則：work · 依賴：G1, G2, S07, work

葉節點依據：work

第一blank時invariant已涵蓋全word，兩blank轉移給正確答案與total termination。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, G2, S07, work — empty word m=0在一步accept；bounded timeout不是reject證書。
- S07 · premise_audit · G1, G2, S06, work — 只能在可達scan態0≤h≤m使用此ranking。
- S06 · premise_audit · G1, G2, S05, work — state只記已掃prefix，不偷看未讀suffix。
- S05 · premise_audit · G1, G2, S04, work — 此trace只證101，尚須全input義務。
- S04 · premise_audit · G1, G2, S03, work — 原input長度3，cell3確實blank。
- S03 · premise_audit · G1, G2, S02, work — 0也是nonblank tape symbol，仍保留於sparse table。
- S02 · premise_audit · G1, G2, S01, work — sparse tape未列cells都blank。
- S01 · premise_audit · G1, G2, work — 無缺transition，也無同pair兩個後繼。





## 錯誤控制與反例

R角色tuple 的第 1、3 個 state slot 中，R 可表示 reject state；第 5 個 move slot 中的 R 只表示向右。

全稱證書parity invariant給答案，ranking給termination，兩者都不可漏。


- 一條101 halt trace就證所有input halt。 → reject — 全input termination另由ranking證明。
- m步未halt就可reject。 → reject — 此正確機器需要m+1步讀末blank。
- empty input不在decider範圍。 → reject — 初始即讀blank，由E在一步accept，零個1為偶數。





## 結論與限制

此機器對所有二元words在m+1步內決定1的個數是否偶數；101於4步accept。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 77d53abdd344aeaf85e19bd50d683bd23ec41515448ac822ac05edcccf7c7a30
- original source SHA-256: 6afbbbf8fb1498115567f484c8776ccf5f2728c23bb439f5feb63e33c9327cd6
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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