5

According to Immerman's Descriptive Complexity diagram, there is a logic called $\mathsf{FO(REGULAR)}$ which captures $\mathsf{NC}^1$. However, I can't find the reference where this logic is defined. Does anyone know the definition? And what paper originally proved this result?

Unlike the classes $\mathsf{AC}^i$ which are captured by iterated quantifiers ($\mathsf{FO}[\log^i(n)]$), it is interesting that $\mathsf{NC}^1$ would require extending the language with a new construct. I might imagine that it is some form of querying for membership in a regular language, but this is only a guess.

My copy of Descriptive Complexity (Immerman 1999) doesn't seem to mention the result (maybe I need the newer version). The best I can find is the paper

  • An algebra and a logic for NC1. Kevin J. Compton and Claude Laflamme, 1990.

which gives a logical characterization of $\mathsf{NC}^1$, but an apparently different one: it is called $\mathsf{FO} + \mathsf{RPR} + \mathsf{BIT}$ (first order logic extended with "relational primitive recursion" and the BIT relation, which gives binary representations of integers).

My interest in this is that I want a "natural" logic that extends both FOL and regular languages, and $\mathsf{NC}^1$ is the most immediate class to try. (Other possible choices are $\mathsf{L}$, $\mathsf{NL}$, and $\mathsf{NC}$, but these extensions would be less conservative.)

Caleb Stanford
  • 872
  • 5
  • 15
  • 2
    Well, $\mathrm{NC}^1$ is the $\mathrm{AC}^0$-closure (i.e., FO-closure) of the class of regular languages, and one can even fix a specific regular language that is $\mathrm{NC}^1$-complete under FO-reductions (or even DLOGTIME reductions), see https://cstheory.stackexchange.com/questions/33487/regular-versus-tc0. Hence the obvious guess is that FO(REGULAR) just denotes FO with extra predicates that decide membership in this complete regular language. – Emil Jeřábek Apr 16 '20 at 06:44
  • 3
    If you want a natural logic capturing $\mathrm{NC}^1$, you should look at FO with monoidal quantifiers (Barrington, Immerman, Straubing: On uniformity within $NC^1$). – Emil Jeřábek Apr 16 '20 at 08:09
  • @EmilJeřábek Thanks for the references! It makes sense that monoidal quantifiers would capture $\mathsf{NC}^1$, since evaluating a monoid is exactly the same as querying a regular language. – Caleb Stanford Apr 16 '20 at 13:12

1 Answers1

1

Professor Immerman kindly answered this by email:

The definition of FO(REGULAR) is the set of all decision problems that are reducible to some regular language via first-order reductions.

Additionally, since the word problem for $S_5$ (which is a regular language) is complete for $\mathsf{NC}^1$ under FO reductions, this means that FO(REGULAR) can be defined equivalently as the set of decision problems that are reducible to $S_5$.

Other logics equivalent to $\mathsf{NC}^1$:

  • FO with monoidal quantifiers (Barrington, Immerman, Straubing, 1990: On uniformity within NC1)

  • FO with "relational primitive recursion" and the BIT relation (Compton, Laflamme, 1990: An algebra and a logic for NC1)

  • FO with width-5 transitive closure (Immerman, 1987: Expressibility as a Complexity Measure: Results and Directions)

Caleb Stanford
  • 872
  • 5
  • 15