Symmetric Circuits for Rank Logic
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 finite 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 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.
fixed-point logic with rank
circuits
symmetric circuits
uniform families of circuits
circuit characterization
circuit framework
finite model theory
descriptive complexity
Theory of computation~Circuit complexity
Theory of computation~Finite Model Theory
Theory of computation~Complexity theory and logic
20:1-20:16
Regular Paper
https://arxiv.org/abs/1804.02939
Anuj
Dawar
Anuj Dawar
Department of Computer Science and Technology, University of Cambridge, UK
https://orcid.org/0000-0003-4014-8248
Gregory
Wilsenach
Gregory Wilsenach
Department of Computer Science and Technology, University of Cambridge, UK
Funding provided by the Gates Cambridge Scholarship.
10.4230/LIPIcs.CSL.2018.20
M. Anderson and A. Dawar. On symmetric circuits and fixed-point logics. Theory of Computing Systems, 60(3):521-551, 2017.
A. Dawar. The nature and power of fixed-point logic with counting. ACM SIGLOG News, 2(1):8-21, 2015.
A. Dawar. On symmetric and choiceless computation. In Mohammad Taghi Hajiaghayi and Mohammad Reza Mousavi, editors, Topics in Theoretical Computer Science, pages 23-29, Cham, 2016. Springer International Publishing.
A. Dawar, E. Grädel, B. Holm, E. Kopczynski, and W. Pakusa. Definability of linear equation systems over groups and rings. Logical Methods in Computer Science, 9(4), 2013.
A. Dawar, M. Grohe, B. Holm, and B. Laubner. Logics with rank operators. In 2009 24th Annual IEEE Symposium on Logic In Computer Science (LICS), pages 113-122, 2009.
A. Dawar and B. Holm. Pebble games with algebraic rules. In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming, pages 251-262, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
A. Dawar and G. Wilsenach. Symmetric circuits for rank logic. arXiv, 2018. URL: http://arxiv.org/abs/1804.02939.
http://arxiv.org/abs/1804.02939
L. Denenberg, Y. Gurevich, and S. Shelah. Definability by constant-depth polynomial-size circuits. Information and Control, 70(2):216-240, 1986.
E. Grädel and W. Pakusa. Rank logic is dead, long live rank logic! In 2015 24th Annual Conference on Computer Science Logic, (CSL), pages 390-404, 2015.
M. Grohe. Descriptive Complexity, Canonisation, and Definable Graph Structure Theory. Lecture Notes in Logic. Cambridge University Press, 2017. URL: https://books.google.co.uk/books?id=RLYrDwAAQBAJ.
https://books.google.co.uk/books?id=RLYrDwAAQBAJ
L. Hella. Logical hierarchies in ptime. Information and Computation, 129(1):1-19, 1996.
N. Immerman. Relational queries computable in polynomial time. Information and Control, 68(1-3):86-104, 1986.
N. Immerman. Descriptive Complexity. Graduate texts in computer science. Springer New York, 1999.
L. Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin Heidelberg, 2004.
M. Otto. The logic of explicitly presentation-invariant circuits. In 1996 10th International Workshop, Annual Conference on Computer Science Logic (CSL), pages 369-384. Springer, Berlin, Heidelberg, 1997.
M. Vardi. The complexity of relational query languages (extended abstract). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, pages 137-146, New York, NY, USA, 1982. ACM.
Anuj Dawar and Gregory Wilsenach
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode