paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the Expressive Power of Higher-Order Pushdown Systems

论高阶下推系统的表达能力
LMCS vol.Volume 16, Issue 32020匹配度 2/10 · 该论文研究高阶下推系统与递归方案的可表达性，属于纯形式语言/自动机理论，与用户关注的 LLM/Agent 交叉、静态分析、浮点程序分析或贝叶斯程序分析没有直接关系。虽然高阶下推/递归方案可作为高阶程序验证的理论基础，但本文未涉及 AI/LLM 或实际程序分析工具与落地。引用 2 inbox
Paweł Parys
逻辑与自动机
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：证明二阶确定性可坍缩下推自动机严格强于任意阶无坍缩确定性高阶下推自动机，并给出相应树/递归方案分离。

本文研究高阶下推系统（等价于递归方案）的表达能力边界。作者证明：二阶确定性可坍缩下推自动机可识别某个语言，而任意阶的不含坍缩的确定性高阶下推自动机均不能识别该语言。由此推出，存在由二阶可坍缩下推系统（等价地，二阶递归方案）生成的树，不能由任意阶的确定性高阶下推系统（等价地，任意阶安全递归方案）生成。方法上通过构造分离语言并分析自动机计算能力，同时给出确定性高阶下推自动机的泵引理，可作为后续应用工具。结果厘清了“坍缩”机制与高阶确定性在生成/识别能力上的严格差异。

问题
论文关注带坍缩机制的高阶下推自动机（及等价递归方案）是否比无坍缩的确定性高阶下推系统具有更强表达能力，以及不同阶数与确定性下是否存在严格分离。
方法
通过构造一个二阶确定性可坍缩下推自动机可识别、而任意阶无坍缩确定性高阶下推自动机均不可识别的语言，并分析其计算与生成能力，证明相应树/递归方案的不可生成性；同时建立确定性高阶下推自动机的泵引理。
评估
采用数学证明与反例构造进行评估，给出表达能力分离定理及推论；未涉及实现或实验评估。
原文摘要（Abstract）

We show that deterministic collapsible pushdown automata of second order can recognize a language that is not recognizable by any deterministic higher-order pushdown automaton (without collapse) of any order. This implies that there exists a tree generated by a second order collapsible pushdown system (equivalently, by a recursion scheme of second order) that is not generated by any deterministic higher-order pushdown system (without collapse) of any order (equivalently, by any safe recursion scheme of any order). As a side effect, we present a pumping lemma for deterministic higher-order pushdown automata, which potentially can be useful for other applications.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{abs-2008-00650,
  title = {On the Expressive Power of Higher-Order Pushdown Systems},
  author = {Paweł Parys},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 3},
  year = {2020},
  doi = {10.23638/lmcs-16(3:11)2020}
}