基于一阶文法的DPDA语言等价性判定性证明
A Short Decidability Proof for DPDA Language Equivalence via First-Order Grammars
摘要：
本文的主要目的是给出确定下推自动机的语言等价可判定性的一个简短的完备证明，这是G。Senizergues，C. Stirling推导出一个原始的递归复杂度上界。这里的证明是在一阶文法的框架中给出的，这似乎特别适合于这个目的。一个附录提出了一个修改斯特林的方法，产生一个复杂性界的形式tetr（2，g（n）），其中tetr是（非初等）运营商的迭代幂（tetration）和g是一个初等函数的输入大小。
英文摘要：
The main aim of the paper is to give a short self-contained proof of the decidability of language equivalence for deterministic pushdown automata, which is the famous problem solved by G. Senizergues, for which C. Stirling has derived a primitive recursive complexity upper bound. The proof here is given in the framework of first-order grammars, which seems to be particularly apt for the aim. An appendix presents a modification of Stirling's approach, yielding a complexity bound of the form tetr(2,g(n)) where tetr is the (nonelementary) operator of iterated exponentiation (tetration) and g is an elementary function of the input size.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
