Partial Fixed-Point Logic on Infinite Structures
Partial Fixed-Point Logic on Infinite Structures
复制标题
无限结构上的部分定点逻辑
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
S. Kreutzer
中科院分区：
文献类型：
--
作者：
S. Kreutzer
我们考虑部分定点逻辑（PFP）的替代语义。为了定义此语义中公式的不动点，需要考虑由公式引发的阶段序列。一旦该序列成为循环，循环的每个阶段中包含的元素集合就被视为不动点。结果表明，在有限结构上，这种定点语义和有限模型理论中考虑的 PFP 标准语义是等效的，尽管可以说属性的形式化甚至可能变得更简单和更直观。与仅在有限结构上定义的标准 PFP 语义相反，新语义可以轻松推广到无限结构和超限归纳。在这种普遍性中，我们在表达能力方面将部分与其他已知的定点逻辑进行比较。论文的主要结果是，在任意结构上，PFP 严格来说比通货膨胀定点逻辑（IFP）更具表现力。在有限结构上分离这些逻辑将证明 PTIME 与 PSPACE 不同。
We consider an alternative semantics for partial fixed-point logic (PFP). To define the fixed point of a formula in this semantics, the sequence of stages induced by the formula is considered. As soon as this sequence becomes cyclic, the set of elements contained in every stage of the cycle is taken as the fixed point. It is shown that on finite structures, this fixed-point semantics and the standard semantics for PFP as considered in finite model theory are equivalent, although arguably the formalisation of properties might even become simpler and more intuitive. Contrary to the standard PFP semantics which is only defined on finite structures the new semantics generalises easily to infinite structures and transfinite inductions. In this generality we compare - in terms of expressive power - partial with other known fixed-point logics. The main result of the paper is that on arbitrary structures, PFP is strictly more expressive than inflationary fixed-point logic (IFP). A separation of these logics on finite structures would prove PTIME different from PSPACE.