Infinitary Logic and Inductive Definability over Finite Structures
Infinitary Logic and Inductive Definability over Finite Structures
复制标题
有限结构上的无限逻辑和归纳可定义性
DOI：
10.1006/inco.1995.1084
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
S. Weinstein
中科院分区：
文献类型：
--
作者：
A. Dawar;S. Lindell;S. Weinstein
已知具有最小不动点算子（FO + LFP）和具有部分不动点算子（FO + PFP）的一阶逻辑的扩展在有限结构上存在序关系的情况下分别捕获复杂性类P和PSPACE。最近，Abiteboul和Vianu（在“Proceedings of the 23rd ACM Symposium on the Theory of Computing，”1991）使用通用计算的机器模型，在没有排序的情况下研究了这两个逻辑的关系。特别是，他们证明了这两种语言具有相等的表达能力，当且仅当P = PSPACE。这些语言也可以被看作是一个无限逻辑的片段，其中每个公式都有一个有限数量的变量，L？∞？，(see例如，Kolaitis和Vardi在“Proceedings of the 5th IEEE Symposium on Logic in Computer Science”，pp. 156-167，1990）。我们研究这种逻辑的有限结构，并提供了一个正常的形式。我们还提出了一个治疗Abiteboul和Vianu？的结果从这个角度来看。特别是，我们表明，我们可以写一个公式FO + LFP定义的顺序的Lk∞？，在所有有限结构上都是一致的。这样做的一个结果是将FO + LFP和P的等价性从有序结构推广到每个元素都可定义的结构类。我们还解决了一个猜想Abiteboul和Vianu提到的FO + LFP是正确的多项式时间可计算的片段L？∞？，这就产生了一个问题：后一个片段是否是一个递归可重命名的类。
The extensions of first-order logic with a least fixed point operator (FO + LFP) and with a partial fixed point operator (FO + PFP) are known to capture the complexity classes P and PSPACE respectively in the presence of an ordering relation over finite structures. Recently, Abiteboul and Vianu (in "Proceedings of the 23rd ACM Symposium on the Theory of Computing," 1991) investigated the relationship of these two logics in the absence of an ordering, using a machine model of generic computation. In particular, they showed that the two languages have equivalent expressive power if and only if P = PSPACE. These languages can also be seen as fragments of an infinitary logic where each formula has a bounded number of variables, L?∞?, (see, for instance, Kolaitis and Vardi, in "Proceedings of the 5th IEEE Symposium on Logic in Computer Science," pp. 156-167, 1990). We investigate this logic on finite structures and provide a normal form for it. We also present a treatment of Abiteboul and Vianu?s results from this point of view. In particular, we show that we can write a formula of FO + LFP that defines an ordering of the Lk∞?, types uniformly over all finite structures. One consequence of this is a generalization of the equivalence of FO + LFP and P from ordered structures to classes of structures where every element is definable. We also settle a conjecture mentioned by Abiteboul and Vianu by showing that FO + LFP is properly contained in the polynomial time computable fragment of L?∞?, raising the question of whether the latter fragment is a recursively enumerable class.