5
$\begingroup$

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

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Apr 16, 2020 at 6:44
  • 3
    $\begingroup$ 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$). $\endgroup$
    – Emil Jeřábek
    Apr 16, 2020 at 8:09
  • $\begingroup$ @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. $\endgroup$
    – Caleb Stanford
    Apr 16, 2020 at 13:12

1 Answer 1

Reset to default
1
$\begingroup$

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)

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.