形式语言与自动机之语言识别机器——下推自动机

下推自动机（Pushdown Automaton，PDA）是一种形式语言与自动机之间的关系，可以用于识别上下文无关文法所生成的语言。它是由有限状态自动机和一个栈组成的，可以通过读取输入符号并在栈顶上推、弹出或不变化栈中的符号来进行状态转移。

在PDA中，初始状态为q0，读入输入串后，如果当前状态为q，栈顶符号为a，输入符号为b，则PDA可以选择进行以下三种操作之一：

1. 推入一个符号x到栈顶，进入状态p
2. 弹出栈顶的符号a，进入状态p
3. 不改变栈顶符号，进入状态p

其中，p和x的选择取决于当前状态、栈顶符号和输入符号，是预先定义好的PDA的转移函数。

当PDA读入整个输入串后，如果当前状态为终止状态qf，且栈为空，则认为该输入串被PDA接受，否则被拒绝。

与有限状态自动机不同的是，PDA在进行状态转移时可以通过栈来记录输入串中的某些信息，因此可以处理一些上下文相关的语言，如{a^n b^n | n >= 1}。但是，PDA也无法处理所有的上下文相关的语言，如{a^n b^n c^n | n >= 1}就无法被PDA识别。

总之，PDA是一种非常重要的自动机模型，可以用于识别上下文无关文法所生成的语言，是计算理论中的基础知识之一。