Inductive Definability with Counting on Finite Structures
Inductive Definability with Counting on Finite Structures
复制标题
有限结构的归纳可定义性
DOI：
10.1007/3-540-56992-8_15
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
M. Otto
中科院分区：
文献类型：
--
作者：
E. Grädel;M. Otto
我们研究逻辑语言的属性和表达能力，包括归纳定义的机制和计数的能力。这些语言中最重要的是带有计数项的定点逻辑，表示为 (FP+ C)。为了激发对这些逻辑的研究，我们回顾一下一阶逻辑（FO）的表达能力受到两个主要原因的限制：它缺乏表达任何需要递归的能力（最显着的例子是传递闭包查询）并且它不能计数（这里最著名的例子是没有一阶公式在偶数基数的结构上精确地成立）：有几种经过充分研究的逻辑和数据库查询语言以某种方式向 FO 添加了递归（或其一部分），特别是各种形式的定点逻辑、查询语言 Datalog 及其扩展。在有序有限结构上，其中一些语言精确地表达了 PTIME 或 PSPACE 中可计算的查询。然而，在任意有限结构上，它们不会，并且几乎所有已知的例子都表明这一点都涉及计数。虽然在存在排序的情况下，计数能力是固有的，例如在定点逻辑中，但在没有排序的情况下几乎不会保留任何计数能力。因此，Immerman [15] 提议在定点逻辑中添加计数量词，并询问这是否足以捕获 PTIME。 Cai、Fiirer 和 Immerman [5] 对此问题的回答是否定的；事实上 (FP+ C) 甚至不能表达所有 LoGSPACE 可计算的查询。尽管如此，我们认为带有计数的定点逻辑是一种值得更多关注的重要语言。我们将证明，在存在计数项（或计数量词）的情况下，任意有限结构上的归纳可定义性具有良好的性质，它保留了这些性质，而无需仅在有序结构的情况下进行计数。论文的组织总结如下：
We study the properties and the expressive power of logical languages that include both a mechanism for inductive definitions and the ability to count. The most important of these languages is fixpoint logic with counting terms, denoted (FP+ C). To motivate the study of these logics, we recall that the expressive power of firstorder logic (FO) is limited by two main reasons: It lacks the power to express anything that requires recursion (the most notable example is the transitive closure query) and it cannot count (the best-known example here is that no first-order formula is true precisely on the structures with even cardinality): There are several well-studied logics and database query languages that add recursion in one way or another to FO (or part of it), notably the various forms of fixpoint logics, the query language Datalog and its extensions.On ordered finite structures, some of these languages express precisely the queries that are computable in PTIME or PSPACE. However, on arbitrary finite structures they do not, and almost all known examples showing this involve counting. While in the presence of an ordering, the ability to count is inherent eg in fixpoint logic, hardly any of it is retained in its absence. Thus, Immerman [15] proposed to add counting quantifiers to fixpoint logic and asked whether this would suffice to capture PTIME. Cai, Fiirer and Immerman [5] answered this question negatively; in fact (FP+ C) does not even express all LoGSPACE-computable queries. Nevertheless we argue that fixpoint logic with counting is an important language that deserves more attention. We will show that in the presence of counting terms (or counting quantifiers) inductive definability on arbitrary finite structures has nice properties that it retains without counting only in the case of ordered structures. The organization of the paper is summed up in the following: