# 下推自動機

nondeterministic PDA以有限控制、input與stack transitions運算，本輪固定讀完input且到final state接受。

mko-pushdown-automaton · definition · v0.10.0



## 數學敘述

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。





## 代表公式（精確 TeX）

P(Q,Z)





## 成立條件


- states/input/stack alphabets finite、unique且pairwise disjoint。
- configuration=[state,input_position,stack]；stack bottom-first/top-last，null transition不增加input_position，bottom transition必須保留bottom。





## 符號作用域


- P — 下推自動機
- Q — 有限狀態集
- Z — stack底標記





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

acceptance convention固定為full input plus final state。

transition tuple、input consumption與bottom-to-top replacement逐欄核對。

finite run證acceptance；未讀完input即final仍不接受，bounded failure不證nonmembership。

讓epsilon消耗input、pop掉bottom、混用empty stack與final state，或將搜尋深度不足當reject proof。





## 已採用的推導導讀

[bottom-first PDA的aabb接受run](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-pushdown-automaton-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [抽象計算模型](https://ocme.evemisslab.com/zh-Hant/mko/mko-computational-model/) — finite transition model。
- [確定有限自動機](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-automaton/) — finite control。
- [數列](https://ocme.evemisslab.com/zh-Hant/mko/mko-sequence/) — finite input/stack/run。
- [上下文無關文法](https://ocme.evemisslab.com/zh-Hant/mko/mko-context-free-grammar/) — language context without equivalence claim。





## 驗證界線

本輪不宣稱一般CFG↔PDA轉換、determinism或language nonmembership。

not_formalized

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





## 下一個義務

加入CFG-PDA equivalence與pumping lemma。





## 同源結構化資料

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

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