What is wrong with this $\mathsf{L} \subseteq \mathsf{L}-$uniform $\mathsf{NC}^1$ argument? The following is not believed to be true:


  $\mathsf{L} \subseteq \mathsf{L}-\mbox{uniform } \mathsf{NC}^1$


Can you help me see where the argument breaks down?

The directed reachability problem is complete for $\mathsf{L}$. 
I argue that it is in $\mathsf{L}$-uniform $\mathsf{NC^1}$.



The directed reachability problem over configuration graphs of
deterministic log-space Turing Machine is complete for $\mathsf{L}$.

The directed reachability problem is in $\mathsf{MSO}_2$:


  given $s$ and $t$, 
  let $P$ represent the free $\mathsf{MSO}$ variable for the edges in the path. 
  We need to verify that $P$ contains a directed path from $s$ to $t$ 
  which can be done by verifying that the in-degree and out-degree (in $P$)
  of every vertex incident on an edge in $P$ is $1$ except for $s$ and $t$ 
  which have in-degree,out-degree = $0,1$ and $1,0$ respectively.


Every forest is a graph of tree-width $1$. 
In particular the configuration graph of 
a deterministic log-space Turing Machine is a bounded tree-width structure.

From Elberfeld, Jakoby, and Tantau's
Logspace versions of the theorems of Bodlaender and Courcelle:


  $\mathsf{MSO}$ formula over bounded tree-width structures 
  can be evaluated in log-space.


The proof goes something like this:
For a given structure size $n$,
a bound on the tree-width of the structures $w$, and
a $\mathsf{MSO}$ formula $\varphi$ with vocabulary $\tau$,
construct (in $\mathsf{L}$) construct a $\#\mathsf{NC}^1$ circuit $C$.

The circuit $C$ given a structure $M$ of size $n$ and tree-width at most $w$,
counts the number of "satisfying" assignments of $\varphi$ on $M$.

(The histogram tabulating 
the number of assignments to the free second order variables in $\varphi$
parameterized on the sizes of the sets of values taken by the the variables).

I think the circuit $C$ only depends on the vocabulary $\tau$, 
the tree-width bound $d$, and the size of structure $n$.

The proof proceeds by evaluating the circuit in $\#\mathsf{NC}^1 \subseteq \mathsf{L}$ but we don't need that part.

For us it suffices to observe that from Nondeterministic $\mathsf{NC^1}$ Computation 
by Caussinus-Mackenzie-Therien-Vollmer:


  every $\#\mathsf{NC}^1$-circuit can be interpreted as 
  counting the number of proof-trees of a $\mathsf{NC}^1$-circuit.


Thus the corresponding circuit outputs $1$ iff 
the input structure satisfies the $\mathsf{MSO}$ formula.

From the above it seems that log-space is at least in logspace-uniform $\mathsf{NC}^1$
In fact, the circuit depends on the input structure, not only on the input structure size. We take a tree-decomposition of the graph with additional colours and turn it into a convolution tree. The evaluation of the formula on this tree is reduced to computing the value of the convolution tree. To compute the value of the tree, it is turned into an arithmetic circuit. Hence we do not get one circuit for each input size as required for $NC^1$, but rather one circuit for each single input.