A Model-Theoretic Characterization of Constant-Depth Arithmetic Circuits

TL;DR

This paper provides a novel model-theoretic characterization of the class AC^0 of functions computed by constant-depth arithmetic circuits, linking it to first-order model checking games, and extends this approach to characterize TC^0.

Contribution

It introduces the first model-theoretic characterization of AC^0 and relates it to first-order model checking games, also characterizing TC^0.

Findings

Functions in AC^0 correspond to counting winning strategies in model checking games.

Provides a new perspective on arithmetic circuit classes through model theory.

Characterizes TC^0 using similar model-theoretic techniques.

Abstract

We study the class $\textrm{AC}^0$ of functions computed by constant-depth polynomial-size arithmetic circuits of unbounded fan-in addition and multiplication gates. No model-theoretic characterization for arithmetic circuit classes is known so far. Inspired by Immerman's characterization of the Boolean class $\textrm{AC}^0$, we remedy this situation and develop such a characterization of $\textrm{AC}^0$. Our characterization can be interpreted as follows: Functions in $\textrm{AC}^0$ are exactly those functions counting winning strategies in first-order model checking games. A consequence of our results is a new model-theoretic characterization of $\textrm{TC}^0$, the class of languages accepted by constant-depth polynomial-size majority circuits.