# bottom-first PDA的aabb接受run [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-pushdown-automaton/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-pushdown-automaton-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 指定PDA有讀完aabb到final f的有限run，末stack仍為[Z]。 完整transition relation與bottom-first/top-last堆疊；final-state acceptance，不混空stack。 ## 已知條件與符號 - calc - G1 — Q={q,p,f}，Σ={a,b}，Γ={Z,A}三者不交；start q,bottom Z,finals{f}。transitions按[from,input或null,top,to,replacement bottom-to-top]為[q,a,Z,q,[Z,A]],[q,a,A,q,[A,A]],[q,b,A,p,[]],[p,b,A,p,[]],[p,null,Z,f,[Z]],[q,null,Z,f,[Z]]。word aabb。 - Z — 不可underflow的bottom - null — 不耗input的epsilon - i — 已讀input長度 ## 規則與來源 - calc · prerequisite — 假設有限集合、有限字串與索引、逐步函數更新及自然數歸納；ε表示長度0字串。 - mko_definition · cited — PDA tuple含finite Q、input alphabet、stack alphabet、start q0、bottom Z、final states與transition relation。transition序列固定為[from_state,input_symbol_or_null,required_stack_top,to_state,replacement_stack_bottom_to_top]；null表示epsilon且不消耗input。stack序列bottom-first/top-last，bottom不可underflow。接受witness為有限run且讀完input到final state。不混用empty-stack acceptance；bounded search failure不證rejection，也不自動宣稱CFG equivalence或determinism。 · mko-pushdown-automaton ## 逐步主鏈 S01 · implies操作前 Q=\{q,p,f\},\quad\Sigma=\{a,b\},\quad\Gamma=\{Z,A\} 操作後 \begin{array}{c|c|c|c|c}q&a&Z&q&[Z,A]\\q&a&A&q&[A,A]\\q&b&A&p&[]\\p&b&A&p&[]\\p&\text{null}&Z&f&[Z]\\q&\text{null}&Z&f&[Z]\end{array} 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 完整六條relation皆合法；底Z只被換成以Z為底的[Z,A]或[Z]，不能underflow。 S02 · implies操作前 w=aabb,\quad |w|=4 操作後 [q,0,[Z]] 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 初態位置0，stack底到頂只有Z。 S03 · implies操作前 [q,0,[Z]] 操作後 [q,1,[Z,A]] 條件：無 規則：calc · 依賴：G1, S01, S02 葉節點依據：calc 讀第一a，以[q,a,Z,q,[Z,A]]替換top Z，保留底並push A。 S04 · implies操作前 [q,1,[Z,A]] 操作後 [q,2,[Z,A,A]] 條件：無 規則：calc · 依賴：G1, S01, S03 葉節點依據：calc 讀第二a，原top A被[A,A]取代，原下方Z保留。 S05 · implies操作前 [q,2,[Z,A,A]] 操作後 [p,3,[Z,A]] 條件：無 規則：calc · 依賴：G1, S01, S04 葉節點依據：calc 讀第一b，以[q,b,A,p,[]]pop最右A並換state p。 S06 · implies操作前 [p,3,[Z,A]] 操作後 [p,4,[Z]] 條件：無 規則：calc · 依賴：G1, S01, S05 葉節點依據：calc 讀末個b，以[p,b,A,p,[]]消去最後A，位置等於4。 S07 · implies操作前 [p,4,[Z]] 操作後 [f,4,[Z]] 條件：無 規則：calc · 依賴：G1, S01, S06 葉節點依據：calc 以[p,null,Z,f,[Z]]做epsilon，位置維持4，底仍存在。 S08 · implies操作前 [f,4,[Z]],\quad f\in F,\quad4=|w| 操作後 aabb\text{ accepted by this finite run} 條件：無 規則：mko_definition · 依賴：G1, S02, S03, S04, S05, S06, S07 葉節點依據：mko_definition 全部輸入已讀且末態final，符合本稿接受慣例，非空stack不妨礙接受。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S02, S03, S04, S05, S06, S07 — 若在初態用q的epsilon先到f，位置仍0而非4，不能接受aabb。 - S07 · premise_audit · G1, S01, S06 — null不消耗輸入，也不能把Z換[]。 - S06 · premise_audit · G1, S01, S05 — input已讀完但p非final，仍須合法epsilon到final。 - S05 · premise_audit · G1, S01, S04 — 只pop一個top，不清空整條stack。 - S04 · premise_audit · G1, S01, S03 — stack右端是top，因此這步淨增一個A而非兩個。 - S03 · premise_audit · G1, S01, S02 — replacement含原Z，若只寫[A]會丟失bottom。 - S02 · premise_audit · G1, S01 — configuration是[state,position,stack]，不可把位置當下一字元本身。 - S01 · premise_audit · G1 — relation不要求total，replacement列bottom-to-top，[]只在top A時pop。 ## 錯誤控制與反例 堆疊方向stack bottom-first/top-last，pop與替換都針對右端。 兩接受門檻同時要求讀完input與final state，不以empty-stack取代。 - 末stack需空才接受。 → reject — 本慣例full input加final f；本run末[Z]仍接受。 - null把位置4變5。 → reject — epsilon不消耗輸入。 - 初態epsilon到f即可接受aabb。 → reject — 尚未讀四個symbols，位置0不等長度4。 ## 結論與限制 指定PDA有讀完aabb到final f的有限run，末stack仍為[Z]。 ## 驗證及來源綁定 0 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 4b91e5f3268836475349aa0a7814487dd2f540fb36c66fb88a2f29701b97f326 - original source SHA-256: 4b91e5f3268836475349aa0a7814487dd2f540fb36c66fb88a2f29701b97f326 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-pushdown-automaton-01.json)