# 決定問題

決定問題由輸入集合 X 與 yes-instance 子集合 Y⊆X 指定；decider 必須對每個合法輸入終止並回傳正確布林答案。

mko-decision-problem · definition · v0.10.0



## 數學敘述

決定問題可表示為輸入集合 X 與 yes-instance 集合 Y⊆X，等價於命題規格 P:X→Prop。相對一個明示計算模型，decider D 必須對每個 x∈X 終止，且 D(x)=true 當且僅當 x∈Y。





## 代表公式（精確 TeX）

D:X\to B





## 成立條件


- 輸入集合 X 與 yes-instance 集合 Y 已固定，Y⊆X。
- 談可判定性時必須另指定有效輸入表示與計算模型；有限查表只證該有限 X。





## 符號作用域


- D — 候選決定程序
- X — 合法輸入集合
- B — 布林答案集合





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

問題規格與實作分開：Y 或 P 描述正確答案，D 是候選程序。只在所有輸入上與規格一致且終止，才是 decider。

對明示有限 X，完整表格可以窮舉驗證候選 D；抽樣一致不足以證明整個論域。域外輸入不參與目前問題。

一般無限輸入域還需要有效編碼與計算模型。這一輪不由有限表格外推可計算性或不可判定性。

把只接受 yes-instance 的半決定程序當成總 decider，或以有限測試通過宣稱無限問題已可判定。





## 已採用的推導導讀

[決定問題：在明示有限輸入集上證明試除程序是 decider](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-decision-problem-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-set/) — 輸入域與 yes-instance 以集合表示。
- [命題](https://ocme.evemisslab.com/zh-Hant/mko/mko-proposition/) — 規格 P(x) 是依輸入而定的命題。
- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 總 decider 對每個合法輸入產生唯一布林輸出。





## 驗證界線

有限輸入表可完整核對規格與輸出；未指定計算模型時不宣稱一般可判定性。

not_formalized

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





## 下一個義務

建立 Prop 規格、Bool decider、有效表示與抽象計算模型之間的明示語義橋。





## 同源結構化資料

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

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