# What is the complexity of the set of closed boolean tautologies assuming well formed formulae?

Let's define two CFGs:

S  ::= 0 | 1 | (S+S) | (S*S)
S' ::= 0 | 1 |  S+S  |  S*S  | (S)


And two languages:

M = { w | S generates w, and w evaluates to 1 }
M' = { w | S' generates w, and w evaluates to 1 }

In both cases, evaluating is done by interpreting + as logical or, * as logical and, and in the case of M' by being careful about * having higher precedence than +.

Suppose w is in S, and u is in S'. My questions are:

1. Is there a finite automaton (or a regex) that can decide wheter w is in M?
2. Is there a finite automaton (or a regex) that can decide wheter u is in M'?
3. Suppose S ::= 0 | 1 | +SS | *SS. (Prefix notation) Does this change the answer to question 1?

I'm aware that without knowing whether w is in S, deciding if w is in M isn't solvable by finite automata due to pumping lemma (we'd have an issue with parentheses), similarly for u, S' and M'. However, knowing that w is in S (and u is in S') might make the problem significantly easier.

Note: if the answer is yes, please write the grammar/regex/proof sketch/explanation in spoiler tags. :)

The answer to all three questions is negative. Consider e.g. the prefix version (3), and assume for contradiction that it is decidable by a (wlog deterministic) automaton $A$ with $m$ states. Consider the strings

\begin{align} u_k&={+}^{m-k}{*}{+}^k,\\ v_l&=1^{l+1}0^{m-l+1}. \end{align}

Notice that $u_kv_l$ is a well-formed Boolean sentence for every $0\le k\le m$, $0\le l\le m+1$, and it is easy to see that $u_kv_l$ evaluates to $1$ iff $k<l$. By the pigeonhole principle, there are $0\le k<l\le m$ such that $u_k$ and $u_l$ land in the same state of $A$, thus $u_kv_l$ and $u_lv_l$ are both accepted or both rejected. However, the former evaluates to $1$, and the latter to $0$.

For infix formulas (questions 1,2), one can use in a similar way formulas of the form

$$(0+((0+\cdots((0+((1+((0+\cdots((0+0)*1))*1))\dots*1))*0))*1))\dots*1)).$$

The argument in fact shows that any deterministic automaton evaluating well-formed Boolean sentences of length $n$ must have size $\Omega(n)$, or in other words, any online algorithm for evaluation of such sentences needs space at least $\Omega(\log n)$. This bound is tight: as shown by Buss, it is possible to evaluate Boolean sentences in infix notation in online space $O(\log d)$, where $d$ is the depth of the formula (i.e., maximum nesting of brackets). (The paper advertises it as an online $O(\log\log n)$-space algorithm for evaluation of balanced formulas, using the fact that these have depth $d=\log n$.)

On the other hand, as also shown by Buss, Boolean sentence evaluation (in either prefix or infix notation) can be done in ALOGTIME, aka uniform $\mathrm{NC}^1$, and it is in fact complete for this class under DLOGTIME many-one reductions. Since regular languages with unsolvable syntactic monoid (for example, $\bigl((a|b)^3(ab^*a|b)\bigr)^*$) are also $\mathrm{NC}^1$-complete, it follows that one can reduce Boolean sentence evaluation in DLOGTIME to a regular language.