<p>Professor Immerman kindly answered this by email:</p>

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

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

<hr>

<h3>Other logics equivalent to <span class="math-container">$\mathsf{NC}^1$</span>:</h3>

<ul>
<li><p>FO with monoidal quantifiers (Barrington, Immerman, Straubing, 1990: On uniformity within NC1)</p></li>
<li><p>FO with "relational primitive recursion" and the BIT relation (Compton, Laflamme, 1990: An algebra and a logic for NC1)</p></li>
<li><p>FO with width-5 transitive closure (Immerman, 1987: Expressibility as a Complexity Measure: Results and Directions)</p></li>
</ul>

CC BY-SA 4.0
2020-04-23T17:26:39.597Z
2020-04-23T17:26:39.597Z
Caleb Stanford
<p>According to <a href="https://people.cs.umass.edu/~immerman/descriptive_complexity.html" rel="nofollow noreferrer">Immerman's Descriptive Complexity diagram</a>, there is a logic called <span class="math-container">$\mathsf{FO(REGULAR)}$</span> which captures <span class="math-container">$\mathsf{NC}^1$</span>. However, I can't find the reference where this logic is defined. Does anyone know the definition? And what paper originally proved this result?</p>

<hr>

<p>Unlike the classes <span class="math-container">$\mathsf{AC}^i$</span> which are captured by iterated quantifiers (<span class="math-container">$\mathsf{FO}[\log^i(n)]$</span>), it is interesting that <span class="math-container">$\mathsf{NC}^1$</span> 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.</p>

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

<ul>
<li><em>An algebra and a logic for NC1.</em> Kevin J. Compton and Claude Laflamme, 1990.</li>
</ul>

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

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

CC BY-SA 4.0
2020-04-16T06:44:43.250Z
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
CC BY-SA 4.0
2020-04-16T08:09:46.040Z
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
CC BY-SA 4.0
2020-04-16T13:12:53.803Z
@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
<cc.complexity-theory><reference-request><lo.logic><circuit-complexity><descriptive-complexity>
What is FO(REGULAR)? (The descriptive complexity equivalent of NC1)
Caleb Stanford
# What is FO(REGULAR)? (The descriptive complexity equivalent of NC1)

(Asked by: username_0 on 2020-04-16)

According to [Immerman's Descriptive Complexity diagram](https://people.cs.umass.edu/~immerman/descriptive_complexity.html), 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.)

**Tags:** cc.complexity-theory, reference-request, lo.logic, circuit-complexity, descriptive-complexity

> **Comments:**
> **username_1**: 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.  
> **username_1**: 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$).  
> **username_0**: @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.  

---

## 1 answers

### Answer by username_0 on 2020-04-23. Score: 2 | Accepted answer

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)


---

