$O_2$是一种多上下文无关文法：一份便于实现与形式化的证明
$O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof
AI总结：
针对现有$n$平衡语言的MCFG生成证明无法衍生经验证解析算法的问题，本文提出了$n\leq2$情形下全新的基础短证明，为实现$O_2$的经验证解析算法迈出实质一步。
摘要：
根据能生成形式语言的文法的表达能力对其进行分类，是计算语言学中的一个基础问题，因此也是计算理论中的基础问题。此外，这类分析还能为群等抽象代数结构的分类提供洞见，例如通过字问题给出的对应关系。尽管许多此类分类问题仍悬而未决，但也有部分问题已经得到解决。近期有研究证明，$n$平衡语言（即其字符串中字母$a_i$和$A_i$的出现次数相同，其中$1\leq i \leq n$）可由多上下文无关文法（multiple context-free grammars, MCFGs）生成；MCFG是对经典乔姆斯基层级中上下文无关文法的若干轻微扩展之一，用于让上述分类更精确。本文从计算视角和证明论视角分析了现有证明，系统研究了每一种证明能否衍生出一种经验证的（即由证明助手检查的）、通过MCFG解析平衡语言的算法。我们得出结论：现有证明无一能切实适配这一实际目标，随后针对关键的$n \leq 2$情形给出了一种全新的、基础的且极短的证明。最后，本文将所提证明与现有证明进行了对比分析，论证了为何该证明是朝着具体获得$O_2$的经验证解析算法迈出的实质性一步。
英文摘要：
Classifying formal languages according to the expressiveness of grammars able to generate them is a fundamental problem in computational linguistics and, therefore, in the theory of computation. Furthermore, such kind of analysis can give insight into the classification of abstract algebraic structure such as groups, for example through the correspondence given by the word problem. While many such classification problems remain open, others have been settled. Recently, it was proved that $n$-balanced languages (i.e., whose strings contain the same occurrences of letters $a_i$ and $A_i$ with $1\leq i \leq n$) can be generated by multiple context-free grammars (MCFGs), which are one of the several slight extensions of context free grammars added to the classical Chomsky hierarchy to make the mentioned classification more precise. This paper analyses the existing proofs from the computational and the proof-theoretical point of views, systematically studying whether each proof can lead to a verified (i.e., checked by a proof assistant) algorithm parsing balanced languages via MCFGs. We conclude that none of the existing proofs is realistically suitable against this practical goal, and proceed to provide a radically new, elementary, extremely short proof for the crucial case $n \leq 2$. A comparative analysis with respect to the existing proofs is finally performed to justify why the proposed proof is a substantial step towards concretely obtaining a verified parsing algorithm for $O_2$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
