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