Symmetric Circuits for Rank Logic

TL;DR

This paper characterizes fixed-point logic with rank (FPR) using symmetric circuits with rank gates, extending the circuit-logic correspondence known for fixed-point logic with counting (FPC).

Contribution

It develops a new framework for circuits with non-symmetric gates, enabling a circuit characterization of FPR, which was previously not established.

Findings

Provides a circuit characterization for FPR.

Develops a framework for circuits with non-symmetric gates.

Extends the circuit-logic correspondence to FPR.

Abstract

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 PTime, but not known to be properly contained. 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). In the case of FPC, the proof of equivalence of circuits and logic rests heavily on the assumption that individual gates compute such symmetric functions and so novel techniques are required to make this work for FPR.