论文标题
惊人的混合多项式封闭及其应用于两变量的一阶逻辑
The amazing mixed polynomial closure and its applications to two-variable first-order logic
论文作者
论文摘要
多项式关闭是一种标准运算符,适用于一类普通语言。在论文中,我们研究了三个称为左(LPOL),右(RPOL)和混合多项式闭合(MPOL)的限制。前两个在MPOL是新的。我们查看每个类别定义的两个决策问题。成员资格将常规语言作为输入,并询问它是否属于C。分离将两种普通语言作为输入,并询问C中是否存在第三种语言,其中包括第一种语言,并且从第二个语言不连接。我们证明,LPOL,RPOL和MPOL保留了在输入类别中轻度假设下会员资格的可决定性,以及在更强的假设下分离的可决定性。我们将这些结果应用于自然层次结构。 首先,我们查看通过将LPOL,RPOL和MPOL递归应用于单个输入类构建的几种语言理论层次结构。我们证明实际上可以使用几乎完全使用MPOL来定义这些层次结构。我们还考虑了两种可变量一阶逻辑的量化器交替层次结构,并证明可以使用MPOL爬上它们。从某种意义上说,结果是通用的,即它具有大多数标准签名选择。我们使用它来证明,对于大多数这些选择,成员资格对于层次结构中的所有级别都是可决定的。最后,我们证明,对于仅配备线性顺序的两变量一阶逻辑的层次结构是可决定的。
Polynomial closure is a standard operator which is applied to a class of regular languages. In the paper, we investigate three restrictions called left (LPol), right (RPol) and mixed polynomial closure (MPol). The first two were known while MPol is new. We look at two decision problems that are defined for every class C. Membership takes a regular language as input and asks if it belongs to C. Separation takes two regular languages as input and asks if there exists a third language in C including the first one and disjoint from the second. We prove that LPol, RPol and MPol preserve the decidability of membership under mild hypotheses on the input class, and the decidability of separation under much stronger hypotheses. We apply these results to natural hierarchies. First, we look at several language theoretic hierarchies that are built by applying LPol, RPol and MPol recursively to a single input class. We prove that these hierarchies can actually be defined using almost exclusively MPol. We also consider quantifier alternation hierarchies for two-variable first-order logic and prove that one can climb them using MPol. The result is generic in the sense that it holds for most standard choices of signatures. We use it to prove that for most of these choices, membership is decidable for all levels in the hierarchy. Finally, we prove that separation is decidable for the hierarchy of two-variable first-order logic equipped with only the linear order.