# Turing機判定模型

固定deterministic single-tape Turing機語義；decider必須對每個合法輸入停機並給正確accept/reject答案。

mko-turing-machine-decision-model · definition · v0.10.0



## 數學敘述

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。





## 代表公式（精確 TeX）

T(M,w)=h





## 成立條件


- move convention固定為L/R/S，accept與reject states無outgoing transitions。
- 全域正向family固定scan-decider schema，其ranking為尚未掃描的input cells加一。





## 符號作用域


- T — Turing執行紀錄
- M — 確定性單帶機
- w — 輸入字
- h — 停機結果





## 直觀、定義與常見誤解

signature qualification與執行語義分開。

有限trace是input-local evidence。

decider需要termination與answer correctness的全域證書。

從一個halt trace或有限step未halt便斷言整台機是decider或reject。





## 已採用的推導導讀

[二元字串偶數1的scan decider](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-turing-machine-decision-model-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [抽象計算模型](https://ocme.evemisslab.com/zh-Hant/mko/mko-computational-model/) — 有限控制與step semantics。
- [決定問題](https://ocme.evemisslab.com/zh-Hant/mko/mko-decision-problem/) — yes/no語義。
- [確定有限自動機](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-automaton/) — 有限狀態控制背景。
- [算法正確性](https://ocme.evemisslab.com/zh-Hant/mko/mko-algorithm-correctness/) — decider total correctness。





## 驗證界線

本輪不宣稱Church–Turing thesis的形式證明、複雜度上界或多帶等價。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

加入many-one reduction、undecidability與complexity。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/turing-machine-decision-model.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-turing-machine-decision-model/index.md)