论文标题
通过字符串的理论形式语言
Formal Languages via Theories over Strings
论文作者
论文摘要
我们研究了以公式为单词方程式的无量化理论，长度约束的算术理论以及对常规，明显下降和确定性无上下文无上下文的语言的类别的谓词来研究形式语言的属性。总的来说，我们考虑了20种不同的理论和可决定性问题，例如空虚和正式语言的普遍性等问题。首先，我们讨论他们的相对表现力，并根据是否存在单词方程式观察两个层次结构。其次，我们考虑了几个重要决策问题的可确定性状态，例如空虚和普遍性。请注意，空虚问题等效于相应理论的满足性问题。第三，我们考虑了一个理论中的一种语言在另一种理论中是否可以表达并显示出该问题不可决定的几个负面结果的问题。这些结果在正常形式的背景下在弦弦解决的实际和理论方面尤其重要。
We investigate the properties of formal languages expressible in terms of formulas over quantifier-free theories of word equations, arithmetic over length constraints, and language membership predicates for the classes of regular, visibly pushdown, and deterministic context-free languages. In total, we consider 20 distinct theories and decidability questions for problems such as emptiness and universality for formal languages over them. First, we discuss their relative expressive power and observe a rough division into two hierarchies based on whether or not word equations are present. Second, we consider the decidability status of several important decision problems, such as emptiness and universality. Note that the emptiness problem is equivalent to the satisfiability problem over the corresponding theory. Third, we consider the problem of whether a language in one theory is expressible in another and show several negative results in which this problem is undecidable. These results are particularly relevant in the context of normal forms in both practical and theoretical aspects of string solving.
