论文标题
通过一阶逻辑分离的通用多项式时间方法，而无需量词交替
A generic polynomial time approach to separation by first-order logic without quantifier alternation
论文作者
论文摘要
我们查看与一阶LogicBς1的片段相关的语言类别，该语言不允许量词交替。每个类是通过选择可以使用的位置上的谓词集来定义的。这样的两个关键片段是配备了线性排序以及可能的继任关系的片段。众所周知，这两个变体具有可决定的成员资格：“输入常规语言属于该类？”。我们依靠操作员BPOL对Bς1的表征：给定C类C，它输出了BPOL类（C）的类别，该类别与配备了与C相关的特殊谓词的变体对应于C。我们将这些结果扩展到两个正交方向。首先，我们使用两种输入：类语言的类G类（即，由DFA识别，其中每个字母诱导了状态的置换）及其扩展名，书面的G+。 BPOL（g）和BPOL（G+）类捕获了许多使用谓词的Bpol（G+）类，例如线性排序，后继，模块化谓词或字母模块化模块化谓词。 其次，我们探讨了更通用的分离问题，而不是会员资格：决定是否可以通过所研究的班级将两种普通语言分开。我们表明，当G的情况下，对于BPOL（G）和BPOL（G+）是可决定的。这是BPOL（G）和两个特定类Bpol（G+）的闻名。然而，算法是间接的，并依赖于涉及的框架，产生了较差的上部复杂性界限。我们的方法是直接的。我们使用基本概念（主要是有限自动机）。我们的主要贡献包括从BPOL（G）和BPOL（G+） - 分离到G-分开分离的多项式时间Turing减少。这产生了Bς1的关键变体的多项式算法，包括配备了线性订购的算法以及可能的后继和/或模块化谓词。
We look at classes of languages associated to the fragment of first-order logic BΣ1 which disallows quantifier alternations. Each class is defined by choosing the set of predicates on positions that may be used. Two key such fragments are those equipped with the linear ordering and possibly the successor relation. It is known that these two variants have decidable membership: "does an input regular language belong to the class ?". We rely on a characterization of BΣ1 by the operator BPol: given an input class C, it outputs a class BPol(C) that corresponds to a variant of BΣ1 equipped with special predicates associated to C. We extend these results in two orthogonal directions. First, we use two kinds of inputs: classes G of group languages (i.e., recognized by a DFA in which each letter induces a permutation of the states) and extensions thereof, written G+. The classes BPol(G) and BPol(G+) capture many variants of BΣ1 which use predicates such as the linear ordering, the successor, the modular predicates or the alphabetic modular predicates. Second, instead of membership, we explore the more general separation problem: decide if two regular languages can be separated by a language from the class under study. We show it is decidable for BPol(G) and BPol(G+) when this is the case for G. This was known for BPol(G) and for two particular classes BPol(G+). Yet, the algorithms were indirect and relied on involved frameworks, yielding poor upper complexity bounds. Our approach is direct. We work with elementary concepts (mainly, finite automata). Our main contribution consists in polynomial time Turing reductions from both BPol(G)- and BPol(G+)-separation to G-separation. This yields polynomial algorithms for key variants of BΣ1, including those equipped with the linear ordering and possibly the successor and/or the modular predicates.
