CSL–LBA 等价定理

形式陈述 ​

固定空字的同一约定。对语言 $L\subseteq {\mathrm{\Sigma }}^{\ast }$，下列条件等价：

1. $L$ 由某个非收缩文法生成，即 $L$ 是上下文有关语言理路上下文有关语言Context-sensitive language · CSL可由非收缩文法生成、允许产生式读取局部上下文的形式语言类。；
2. $L$ 被某台非确定性线性有界自动机理路线性有界自动机Linear-bounded automaton · LBA工作带可访问区域被输入长度的常数倍限制的非确定性图灵机。接受。

若语言包含 $\epsilon$，文法侧允许受控规则 $S\to \epsilon$ 且 $S$ 不出现在任何右侧；机器侧单独规定空输入的接受。对非空字，两种模型都不需要这一例外。

证明纲要 ​

下面保留双向构造的关键编码与正确性理由，但不逐条列出机器到文法方向的全部局部产生式，因此是证明纲要而非完整形式构造。

文法到机器的构造如下。对长度为 $n$ 的输入 $w$，LBA 在其线性带区中从 $S$ 开始，非确定地选择产生式和出现位置，维护当前 sentential form，并拒绝任何长度超过 $n$ 的分支。因为文法不收缩，一条最终得到 $w$ 的推导中，所有中间串长度都不超过 $n$。机器接受当且仅当某个分支恰好生成 $w$。

机器到文法方向先采用 LBA 条目中的固定轨道压缩，把常数倍工作区放进恰好 $n$ 个复合格；不能把 $cn+c_0$ 个文法符号在最后直接缩成 $n$ 个终结符。文法先猜出一个非空输入及同样长的初始配置，每个复合格同时保存原输入符号、工作轨道内容和必要的头位置或端点标志。生成阶段只增长字符串，进入模拟阶段后不再增加格。

有限的局部产生式模拟每个合法读写与移动，且保持复合格数不变。阶段标记隔离生成、模拟与清理；只有模拟到接受配置后，清理扫描才把每个复合格逐一改写为它保存的原输入终结符，仍是一格换一符号，不发生收缩。故能够完整清理得到的字恰好是某条合法接受运行的原输入。具体局部规则与阶段控制还需在完整构造中列出，这里保留的是长度约束和正确性接口。