Symmetric Circuits and Model-Theoretic Logics

Abstract

The question of whether there is a logic that characterises polynomial-time is arguably the most important open question in finite model theory. The study of extensions of fixed-point logic are of central importance to this question. It was shown by Anderson and Dawar that fixed-point logic with counting (FPC) has the same expressive power as uniform families of symmetric circuits over a basis with threshold functions. In this thesis we prove a far-reaching generalisation of their result and establish an analogous circuit characterisation for each from a broad range of extensions of fixed-point logic. In order to do so we fist develop a very general framework for defining and studying extensions of fixed-point logics, which we call generalised operators. These operators generalise Lindström quantifiers as well as the counting and rank operators used to define FPC and fixed-point logic with rank (FPR). We also show that in order to define a symmetric circuit model that goes beyond FPC we need to consider circuits with gates that are allowed to compute non-symmetric functions. In order to do so we develop a far more general framework for studying circuits. We also show that key notions, such as the notion of a symmetric circuit, can be analogously defined in this more general framework. The characterisation of FPC in terms of symmetric circuits, and the treatment of circuits generally, relies heavily on the assumption that the gates in the circuit compute symmetric functions. We develop a broad range of new techniques and approaches in order to study these more general symmetric circuit models. As a corollary of our main result we establish a circuit characterisation of FPR. We also show that the question of whether there is a logic that characterises polynomial-time can be understood as a question about the symmetry property of circuits. We lastly propose a number of new approaches that might exploit this new-found connection between circuit complexity and descriptive complexity.

Type

Related