# 完整有限reduction與方向保持 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-many-one-reduction/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-many-one-reduction-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 逐x核iff、組合及decider transfer。 有限完整truth tables；不宣稱無限domain算法。 ## 已知條件與符號 - work - G1 — source S={0,1,2,3}，A={1,3}；target T={a,b,c}，B={b}；f=(a,b,c,b)。U={u,v}，C={v}；g(a)=u、g(b)=v、g(c)=u。 - f,g,h — total reductions及composition - D_B — target decider ## 規則與來源 - mko_definition · cited — 有限題族明示source carrier、target carrier、decision predicates與完整total mapping table，逐x雙向驗x∈A iff f(x)∈B；只驗yes instances不足。composition須保留方向：A≤mB且B≤mC推出A≤mC。若A≤mB且B decidable，先算f再跑B decider可得A decider；反向transfer不成立。partial map、倒轉方向與Turing reduction混同均須拒絕。有限mapping table只證指定finite domain；無限domain仍需完整可計算算法及termination certificate。 · mko-many-one-reduction - work · prerequisite — many-one reduction是total computable map保持x∈A iff f(x)∈B；有限完整table可計算且halt；函數合成與iff傳遞。 ## 逐步主鏈 S01 · implies操作前 f=(a,b,c,b),\quad g=(u,v,u) 操作後 f:S\to T,\quad g:T\to U\text{ are total} 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 每個source entry都有合法target像；g也完整定義。 S02 · implies操作前 x=0,2 操作後 x\notin A,\quad f(0)=a\notin B,\quad f(2)=c\notin B 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work 全部no instances逐一保持no。 S03 · implies操作前 x=1,3 操作後 x\in A,\quad f(1)=f(3)=b\in B 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 全部yes instances也保持yes。 S04 · implies操作前 \forall x\in S:\ x\in A\iff f(x)\in B 操作後 A\le_m B\quad\text{on the declared carriers} 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 四source元素全部完成雙向membership equivalence。 S05 · implies操作前 a,c\notin B,\quad b\in B 操作後 g(a)=g(c)=u\notin C,\quad g(b)=v\in C 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work 完整三target元素給B≤mC。 S06 · implies操作前 h=g\circ f 操作後 h=(u,v,u,v),\quad x\in A\iff h(x)\in C 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 逐表合成保持方向A到C，四entry完整。 S07 · implies操作前 D_B(a)=0,D_B(b)=1,D_B(c)=0 操作後 D_A(x)=D_B(f(x))=(0,1,0,1)_x 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work 先算f再查B decider，得到完整A truth table且有限查表halt。 S08 · implies操作前 A\le_mB\text{ and }B\text{ decidable} 操作後 A\text{ decidable; no reverse implication supplied} 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work 演算法composition解釋正向transfer；對一般問題不能由A可決推B可決。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S07, work — 有限carriers本來皆可查表，不能用它們偽造無限不可決反例。 - S07 · premise_audit · G1, S06, work — decider transfer是從target B到source A。 - S06 · premise_audit · G1, S05, work — 不能用f∘g，型別和方向都不匹配。 - S05 · premise_audit · G1, S04, work — g定義域是整個T，而不只B。 - S04 · premise_audit · G1, S03, work — 這個有限結論不延伸未列的整數。 - S03 · premise_audit · G1, S02, work — x=1、3不同但可同像，reduction不要求injective。 - S02 · premise_audit · G1, S01, work — 只核yes會漏掉這兩個責任。 - S01 · premise_audit · G1, work — partial table不能先稱many-one reduction。 ## 錯誤控制與反例 no cases0、2的membership否定也逐一核。 transfer方向沿f計算方向走，使用target decider來解source。 - 只要f在1、3送b即可，0也可送b。 → reject — 0非A但b屬B會破壞iff反向。 - f必須injective。 → reject — 1與3同像b仍完整保持iff。 - composition應是f∘g。 → reject — g輸出U但f輸入S，不合型別；正確g∘f。 ## 結論與限制 f證A≤mB，g證B≤mC，g∘f證A≤mC；先f後DB決定A。 ## 驗證及來源綁定 2 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 1a1c76bdcb2cbe175d47046cb14542bfd1c9bd765be098a093d56ec92f7bd817 - original source SHA-256: 64cb4efb6449a3a14fcb1d7a0a1135fd167442065877da4e143010419d64892f - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-many-one-reduction-01.json)