The expressive power of fixed-point logic with counting

1996 ◽  
Vol 61 (1) ◽  
pp. 147-176 ◽  
Author(s):  
Martin Otto
Keyword(s):  
Fixed Point ◽  
Polynomial Time ◽  
Natural Extension ◽  
Expressive Power ◽  
Generic Model ◽  
Point Counting ◽  
Ordered Structures ◽  
Relational Structures ◽  
Positive Assessment

AbstractWe study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count.To this end an isomorphism preserving (‘generic’) model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation of the relational vs. the arithmetical side of the algorithms involved.In parallel, we study the relations of Fixed-Point+Counting with the infinitary logics and the corresponding pebble games.The main result, however, involves the concept of an arithmetical invariant. By this we mean a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. In particular its values are linearly ordered structures. We establish the existence of a family of arithmetical invariants with the following properties:• The invariants themselves can be evaluated in polynomial time.• A class of finite relational structures is definable in Fixed-Point+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants.• The invariant r classifies all finite relational structures exactly up to equivalence with respect to the logic We also give a characterization of Fixed-Point+Counting in terms of sequences of formulae in the : It corresponds exactly to the polynomial time computable families (φn)n ∈ ω in these logics.Towards a positive assessment of the expressive power of Fixed-Point+Counting, it is shown that the natural extension of fixed-point logic by Lindström quantifiers, which capture all the PTime computable properties of cardinalities of definable predicates, is strictly weaker than what we get here. This implies in particular that every extension of fixed-point logic by means of monadic Lindström quantifiers, which stays within PTime, must be strictly contained in Fixed-Point+Counting.

On fixed-point logic with counting

2000 ◽  
Vol 65 (2) ◽  
pp. 777-787 ◽  
Author(s):  
Jörg Flum ◽  
Martin Grohe
Keyword(s):  
Fixed Point ◽  
Complexity Theory ◽  
Polynomial Time ◽  
Planar Graphs ◽  
Expressive Power ◽  
Descriptive Complexity ◽  
Main Motivation ◽  
First Order ◽  
Finite Structures ◽  
Tree Width

One of the fundamental results of descriptive complexity theory, due to Immerman [13] and Vardi [18], says that a class of ordered finite structures is definable in fixed-point logic if, and only if, it is computable in polynomial time. Much effort has been spent on the problem of capturing polynomial time, that is, describing all polynomial time computable classes of not necessarily ordered finite structures by a logic in a similar way.The most obvious shortcoming of fixed-point logic itself on unordered structures is that it cannot count. Immerman [14] responded to this by adding counting constructs to fixed-point logic. Although it has been proved by Cai, Fürer, and Immerman [1] that the resulting fixed-point logic with counting, denoted by IFP+C, still does not capture all of polynomial time, it does capture polynomial time on several important classes of structures (on trees, planar graphs, structures of bounded tree-width [15, 9, 10]).The main motivation for such capturing results is that they may give a better understanding of polynomial time. But of course this requires that the logical side is well understood. We hope that our analysis of IFP+C-formulas will help to clarify the expressive power of IFP+C; in particular, we derive a normal form. Moreover, we obtain a problem complete for IFP+C under first-order reductions.

scholarly journals Isomorphism, canonization, and definability for graphs of bounded rank width

2021 ◽  
Vol 64 (5) ◽  
pp. 98-105
Author(s):  
Martin Grohe ◽  
Daniel Neuen
Keyword(s):  
Fixed Point ◽  
Complexity Theory ◽  
Polynomial Time ◽  
Graph Isomorphism ◽  
Isomorphism Problem ◽  
Descriptive Complexity ◽  
Graph Isomorphism Problem ◽  
Structural Graph ◽  
Graph Classes ◽  
Bounded Rank

We investigate the interplay between the graph isomorphism problem, logical definability, and structural graph theory on a rich family of dense graph classes: graph classes of bounded rank width. We prove that the combinatorial Weisfeiler-Leman algorithm of dimension (3 k + 4) is a complete isomorphism test for the class of all graphs of rank width at most k. A consequence of our result is the first polynomial time canonization algorithm for graphs of bounded rank width. Our second main result addresses an open problem in descriptive complexity theory: we show that fixed-point logic with counting expresses precisely the polynomial time properties of graphs of bounded rank width.

scholarly journals Construction and Characterization of Representations of SU(7) for GUT Model Builders

Symmetry ◽  
2021 ◽  
Vol 13 (6) ◽  
pp. 1044
Author(s):  
Daniel Jones ◽  
Jeffery A. Secrest
Keyword(s):  
Gauge Symmetry ◽  
Symmetry Group ◽  
Lie Group ◽  
Cartan Subalgebra ◽  
Natural Extension ◽  
Grand Unification ◽  
Raising And Lowering Operators ◽  
Higher Dimensional ◽  
Lowering Operators

The natural extension to the SU(5) Georgi-Glashow grand unification model is to enlarge the gauge symmetry group. In this work, the SU(7) symmetry group is examined. The Cartan subalgebra is determined along with their commutation relations. The associated roots and weights of the SU(7) algebra are derived and discussed. The raising and lowering operators are explicitly constructed and presented. Higher dimensional representations are developed by graphical as well as tensorial methods. Applications of the SU(7) Lie group to supersymmetric grand unification as well as applications are discussed.

scholarly journals GALOIS THEORY OF THE CANONICAL THETA STRUCTURE

2011 ◽  
Vol 07 (01) ◽  
pp. 173-202
Author(s):  
ROBERT CARLS
Keyword(s):  
Galois Theory ◽  
Theoretical Foundation ◽  
Abelian Varieties ◽  
Geometric Mean ◽  
Null Point ◽  
Point Counting ◽  
Characteristic 2 ◽  
Theoretic Characterization ◽  
Generalized Arithmetic

In this article, we give a Galois-theoretic characterization of the canonical theta structure. The Galois property of the canonical theta structure translates into certain p-adic theta relations which are satisfied by the canonical theta null point of the canonical lift. As an application, we prove some 2-adic theta identities which describe the set of canonical theta null points of the canonical lifts of ordinary abelian varieties in characteristic 2. The latter theta relations are suitable for explicit canonical lifting. Using the theory of canonical theta null points, we are able to give a theoretical foundation to Mestre's point counting algorithm which is based on the computation of the generalized arithmetic geometric mean sequence.

scholarly journals Copyful Streaming String Transducers

2021 ◽  
Vol 178 (1-2) ◽  
pp. 59-76
Author(s):  
Emmanuel Filiot ◽  
Pierre-Alain Reynier
Keyword(s):  
Polynomial Time ◽  
Equivalence Problem ◽  
Expressive Power ◽  
The Other ◽  
Finite State Automata ◽  
Finite State ◽  
Variable Content ◽  
Deterministic Automata ◽  
Intermediate Output ◽  
Linear Manner

Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. Černý in 2010 as a one-way deterministic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a set of variables in which to store intermediate output strings, and those variables can be combined and updated all along the run, in a linear manner, i.e., no variable content can be copied on transitions. It is known that copyless SST capture exactly the class of MSO-definable string-to-string transductions, and are as expressive as deterministic two-way transducers. They enjoy good algorithmic properties. Most notably, they have decidable equivalence problem (in PSpace). On the other hand, HDT0L systems have been introduced for a while, the most prominent result being the decidability of the equivalence problem. In this paper, we propose a semantics of HDT0L systems in terms of transductions, and use it to study the class of deterministic copyful SST. Our contributions are as follows: (i)HDT0L systems and total deterministic copyful SST have the same expressive power, (ii)the equivalence problem for deterministic copyful SST and the equivalence problem for HDT0L systems are inter-reducible, in quadratic time. As a consequence, equivalence of deterministic SST is decidable, (iii)the functionality of non-deterministic copyful SST is decidable, (iv)determining whether a non-deterministic copyful SST can be transformed into an equivalent non-deterministic copyless SST is decidable in polynomial time.

Strong extension axioms and Shelah's zero-one law for choiceless polynomial time

2003 ◽  
Vol 68 (1) ◽  
pp. 65-131 ◽  
Author(s):  
Andreas Blass ◽  
Yuri Gurevich
Keyword(s):  
Fixed Point ◽  
Polynomial Time ◽  
Order Logic ◽  
Complexity Class ◽  
First Order Logic ◽  
Infinitary Logic ◽  
Extensive Discussion ◽  
First Order ◽  
Detailed Proof ◽  
Strong Extension

AbstractThis paper developed from Shelah's proof of a zero-one law for the complexity class “choiceless polynomial time,” defined by Shelah and the authors. We present a detailed proof of Shelah's result for graphs, and describe the extent of its generalizability to other sorts of structures. The extension axioms, which form the basis for earlier zero-one laws (for first-order logic, fixed-point logic, and finite-variable infinitary logic) are inadequate in the case of choiceless polynomial time; they must be replaced by what we call the strong extension axioms. We present an extensive discussion of these axioms and their role both in the zero-one law and in general.

Microstructural and Chemical Characterization of Ordered Structure in Yttrium Doped Ceria

2013 ◽  
Vol 19 (1) ◽  
pp. 102-110 ◽  
Author(s):  
Pengfei Yan ◽  
Toshiyuki Mori ◽  
Yuanyuan Wu ◽  
Zhimin Li ◽  
Graeme John Auchterlonie ◽  
...  
Keyword(s):  
Chemical Characterization ◽  
Electron Microscopic Observation ◽  
Doped Ceria ◽  
Electron Microscopic ◽  
Ordered Structures ◽  
Transmission Electron ◽  
Vacancy Ordering ◽  
Crystal Model ◽  
Electron Energy Loss

AbstractThe ordered structures in different doping levels (x = 0.1, 0.15, 0.2, 0.25, 0.3) of yttrium doped ceria (YDC, Ce(1−x)YxO2−δ) electrolytes were investigated by electron diffraction, high-resolution transmission electron microscopy (TEM), scanning TEM, and electron energy loss spectroscopy. Oxygen vacancy ordering was experimentally confirmed within the ordered structures. With increasing the doping level, the concentration of trivalent Ce cations was increased in YDC samples and such trivalent Ce cations were supposed to mainly exist in the ordered structures. Based on our electron microscopic observation and microanalysis, a crystal model for the ordered structures is proposed.

scholarly journals Symmetric Circuits for Rank Logic

2022 ◽  
Vol 23 (1) ◽  
pp. 1-35
Author(s):  
Anuj Dawar ◽  
Gregory Wilsenach
Keyword(s):  
Fixed Point ◽  
Expressive Power ◽  
Broad Framework ◽  
The Individual ◽  
Rank Of A Matrix

Fixed-point logic with rank (FPR) is an extension of fixed-point logic with counting (FPC) with operators for computing the rank of a matrix over a finit field. The expressive power of FPR properly extends that of FPC and is contained in P, but it is not known if that containment is proper. We give a circuit characterization for FPR in terms of families of symmetric circuits with rank gates, along the lines of that for FPC given by Anderson and Dawar in 2017. This requires the development of a broad framework of circuits in which the individual gates compute functions that are not symmetric (i.e., invariant under all permutations of their inputs). This framework also necessitates the development of novel techniques to prove the equivalence of circuits and logic. Both the framework and the techniques are of greater generality than the main result.

scholarly journals Face-Width of Pfaffian Braces and Polyhex Graphs on Surfaces

10.37236/3540 ◽  
2014 ◽  
Vol 21 (4) ◽  
Author(s):  
Dong Ye ◽  
Heping Zhang
Keyword(s):  
Bipartite Graph ◽  
Polynomial Time ◽  
Perfect Matching ◽  
Cartesian Product ◽  
Perfect Matchings ◽  
Face Width ◽  
Graphs On Surfaces ◽  
Positive Genus ◽  
Pfaffian Graph

A graph $G$ with a perfect matching is Pfaffian if it admits an orientation $D$ such that every central cycle $C$ (i.e. $C$ is of even size and $G-V(C)$ has a perfect matching) has an odd number of edges oriented in either direction of the cycle. It is known that the number of perfect matchings of a Pfaffian graph can be computed in polynomial time. In this paper, we show that every embedding of a Pfaffian brace (i.e. 2-extendable bipartite graph)  on a surface with a positive genus has face-width at most 3.  Further, we study Pfaffian cubic braces and obtain a characterization of Pfaffian polyhex graphs: a polyhex graph is Pfaffian if and only if it is either non-bipartite or isomorphic to the cube, or the Heawood graph, or the Cartesian product $C_k\times K_2$ for even integers $k\ge 6$.

Sign in / Sign up

Export Citation Format

Share Document