Lichter, Moritz (2023)
Continuing the Quest for a Logic Capturing Polynomial Time - Potential, Limitations, and Interplay of Current Approaches.
Technische Universität Darmstadt
doi: 10.26083/tuprints-00024244
Dissertation, Erstveröffentlichung, Verlagsversion

Kurzbeschreibung (Abstract)

The search for a logic capturing PTIME is one central question of finite model theory and descriptive complexity theory: Is there a reasonable logic in which exactly the polynomial-time decidable properties of finite relational structures, e.g., of finite graphs, are definable? This thesis continues the search and investigates all current approaches and candidates for such logics. We examine and compare their expressive power, show limitations, and study the combination and relationship of them. We contribute the following new results:

First, we show that the quantifier depth of 3-variable first-order logic with counting needed to distinguish two n-element structures is in O(n log n). Equivalently, the 2-dimensional Weisfeiler-Leman algorithm stabilizes in O(n log n) iterations. This upper bound matches the known Ω(n) lower bound up to a logarithmic factor. We use representation-theoretic arguments for matrix algebras closely related to the algorithm.

Second, we consider the logic of Choiceless Polynomial Time (CPT). This logic expresses all choice-less polynomial-time computations on relational structures. CPT is a promising candidate for a logic capturing PTIME. Because proving or disproving that CPT captures PTIME is currently out of reach, capturing PTIME with CPT on restricted classes of structures is studied. Capturing PTIME is usually achieved by defining canonization. We show that CPT canonizes structures with bounded color class size for which every color class induces a dihedral automorphism group. The canonization is based on a new normal form, a classification of certain subdirect products of dihedral groups, and the existing canonization for structures with bounded color class size and abelian colors.

Third, we consider the combination of two approaches to capture PTIME. We combine CPT with witnessed symmetric choice (CPT+WSC). This restricted choice-mechanism guarantees that the result of a CPT-computation is independent of the choices made. While defining canonization is the usual way to capture PTIME, it is unknown whether canonization has to be definable. For CPT+WSC, we show that a CPT+WSC-definable isomorphism test for a class of structures implies a CPT+WSC-definable canonization. If isomorphism for this class is actually polynomial-time decidable, capturing PTIME with CPT+WSC is equivalent to defining isomorphism in CPT+WSC.

Fourth, we further investigate witnessed symmetric choice. Showing that witnessed symmetric choice makes CPT more expressive would separate CPT from PTIME, which itself is an open problem. We consider inflationary fixed-point logic with counting (IFPC) as base logic, for which witnessed symmetric choice strictly increases expressiveness. We separate IFPC+WSC from PTIME and show that the further extension with an operator based on logical interpretations (IFPC+WSC+I) is strictly more expressive. Hence, at least for IFPC, witnessed symmetric choice alone is too weak to capture PTIME. We also make a first step to separate IFPC+WSC+I from PTIME.

Last, we consider extensions of IFPC by operators from linear algebra. We separate rank logic, the second promising candidate, from PTIME. Rank logic extends IFPC by an operator to define ranks over finite fields. We show that rank logic fails to define isomorphism for certain structures for which isomorphism is polynomial-time decidable and actually CPT-definable. Hence, rank logic cannot even capture CPT. We also show that the more general linear-algebraic logic fails to define this isomorphism problem. This logic encompasses every extension of IFPC by linear-algebraic operators over finite fields. Consequently, linear algebra over finite fields is too weak to capture PTIME.

Frage zum Eintrag

Redaktionelle Details anzeigen