# What is FO(REGULAR)? (The descriptive complexity equivalent of NC1)

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.)

• 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 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. Apr 16, 2020 at 6:44
• 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$). Apr 16, 2020 at 8: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. Apr 16, 2020 at 13:12

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)