$O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof

要約

形式言語を生成できる文法の表現力に応じて形式言語を分類することは、計算言語学、したがって計算理論の基本的な問題です。
さらに、この種の分析は、たとえば文章問題によって与えられる対応関係を通じて、グループなどの抽象的な代数構造の分類に対する洞察を与えることができます。
このような分類問題の多くは未解決のままですが、解決された問題もあります。
最近、$n$ バランス型言語 (つまり、その文字列に $a_i$ と $A_i$ という同じ文字が $1\leq i \leq n$ で出現する言語) を複数の文脈自由文法で生成できることが証明されました (
MCFG) は、前述の分類をより正確にするために古典的なチョムスキー階層に追加された文脈自由文法をわずかに拡張したものの 1 つです。
この論文は、計算論的および証明理論的な観点から既存の証明を分析し、各証明が 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$.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google