一句话:提出混合多项式闭包 MPol,证明其保持成员与分离可判定性,并用于 FO2 量词交替层级。
本文研究正则语言类上的多项式闭包算子,引入左、右、混合三种限制,其中混合多项式闭包 MPol 为新定义。针对成员问题(给定正则语言是否属于某类)与分离问题(是否存在该类中同时包含第一个语言且与第二个语言不相交的语言),作者证明 LPol、RPol 与 MPol 在较弱假设下保持成员可判定性,在更强假设下保持分离可判定性。随后将其应用于语言理论层级与二变量一阶逻辑 FO2 的量词交替层级:这些层级可几乎完全用 MPol 定义,且可用 MPol 逐级攀升,结果对多数标准签名具有一般性。由此证明多数签名下 FO2 各级成员可判定,并证明仅含线性序的 FO2(<) 的分离问题可判定。
Polynomial closure is a standard operator which is applied to a class of regular languages. In this 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 . Membership takes a regular language as input and asks if it belongs to . Separation takes two regular languages as input and asks if there exists a third language in 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 (FO2) 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 (FO2(<)).