Circuits, Logic and Symmetry

The P vs NP conjecture is arguably one of the deepest
problems both in computer science and in science more generally. The conjecture
concerns the very act of problem solving itself, asking if the problems we think
are hard to solve are in fact hard, or if they admit some clever, efficiently
computable, solution. Put more technically, can we separate NP, a class
containing problems believed to be hard, from P, the class of efficiently
solvable problems. In order to make progress we need some understanding of what
it is about a problem that makes it efficiently solvable. In other words, we
need a `nice' characterization of P. This is a challenge because complexity
classes are defined using low-level machine models. These models are hard to
analyse and offer us little insight into the nature of the class. One approach
has been to develop alternative characterizations of complexity classes using
logics, which we think of as abstract high-level languages, rather than
low-level machine models. These logics work over abstract representations of
data, rather than binary strings and, crucially, respect the symmetries inherent
in that representation. These logical characterizations offer great insight into
what pieces of `abstract machinery' (e.g. recursion, counting operations, etc.)
are required to solve exactly those problems in a complexity class. We can now
frame our previous question more concretely: Is there a logic that characterizes
P?

This question is not only closeely related to the P vs NP conjecture, but
is itself a deep question about the nature of abstraction. In order to make
progress we would like to understand what differentiates the computational power
of high-level, abstract languages from that of low-level machines. Recent work
has shown that high-level programs define algorithms with a strong symmetry
property. In contrast, algorithms given by machine models are characterized by a
very weak symmetry condition. It follows that the relationship between these
models, and hence the central question of this field, can be reduced to a
question about the significance of the symmetry condition. In fact, recent
results have enabled us to ask fine-grained questions about the role of
symmetry, allowing us to use progressive weakenings of the symmetry requirement
in order to interpolate between the high-level languages and low-level
models.

The proposed work connects three fundamental approaches in complexity
theory, by exploring how symmetry plays a role in analysing complexity
in each case. They are circuit complexity, descriptive complexity and
proof complexity.

Software engineers working today deploy a vast range of skills
acquired through their training. Most of those skills have their
origins in work that was cutting-edge research not very long ago. One
such key skill, taught in undergraduate computer science curricula is
to recognize a computatinally intractable problem when it arises in a
practical application. A resourceful engineer working on such
problems will be equipped with the knowledge of what problems are
algorithmically tractable and which ones are not. For the latter, they
will know not to attempt brute-force search methods but be able to
deploy suitable approximation or heuristic methods. The knowledge and
skills that enable them to do that emerged from research in
theoretical computer science that has matured and found its way into
computer science curricula that are taught to aspiring engineers
around the world. These then go on to make incalculable contributions
to the efficiency and reliability of the systems that life in the age
of algorithms depends on.

The research proposed here seeks to develop new conceptual tools that
will enable a better understanding of the role of symmetry and
abstraction in the development of algorithms, their efficiency and
complexity. The central pathway to impact for such work leads from
academic research to the teaching of the conceptual tools to students,
to making them part of the future engineers' armoury, greatly
enhancing their productivity. The impact activities identified in the
proposal are aimed at moving the research through the first steps of
this path.