Descriptive complexity of linear algebra
Seminar Room 1, Newton Institute
An important question that has motivated much work in finite model theory is that of finding a logical characterisation of polynomial-time computability. That is to say, to find a logic in which a class of finite structures is expressible if, and only if, membership in the class is decidable in deterministic polynomial time (PTIME).
Much of the research in this area has focused on the extension of inflationary fixed-point logic by counting terms (FPC). This logic has been shown to capture polynomial time on many natural classes of structures, including all classes of graphs with excluded minors. At the same time, it is also known that FPC is not expressive enough to capture polynomial time on the class of all finite graphs. Noting that the various examples of properties in PTIME that are not definable in FPC can be reduced to testing the solvability of systems of linear equations, Dawar et al. (2009) introduced the extension of fixed-point logic with operators for expressing matrix rank over finite fields (FPR). Fixed-point rank logic strictly extends the expressive power of FPC while still being contained in PTIME and it remains an open question whether there are polynomial-time properties that are not definable in this logic.
In this talk I give an overview of the main results in the logical study of linear algebra and present new developments in this area. After reviewing the background to this study, I define logics with rank operators and discuss some of the properties that can be expressed with such logics. In order to delimit the expressive power of FPR, I present variations of Ehrenfeucht-Fraïssé games that are suitable for proving non-definability in finite-variable rank logics. Using the rank games, I show that if we restrict to rank operators of arity two, then there are graph properties that can be defined by first-order logic with rank over GF(p) that are not expressible by any sentence of fixed-point logic with rank over GF(q), for all distinct primes p and q. Finally, I discuss how we can suitably restrict these rank games to get an algebraic game equivalence that can be decided in polynomial time on all classes of finite structures. As an application, this gives a family of polynomial-time approximations of graph isomorphism that is strictly stronger than the well-known Weisfeiler-Lehman method.