# A Gentle Introduction to Applications of Algorithmic Metatheorems for Space and Circuit Classes
## 4 An Algorithmic Metatheorem for Log-Depth Circuits and Its Applications  
The proofs of both versions versions of Courcelle's Theorem, the classical version and the logspace version, proceeded in four steps:  
1. Compute a tree decomposition \((T,B)\) of the input graph \(G\). 2. Transform the formula \(\phi\) into a formula \(\phi^{\prime}\). 3. Transform the formula \(\phi^{\prime}\) into a tree automaton \(A\). 4. Run the tree automaton \(A\) on \(T\). In both versions, the algorithmically \"really difficult\" part was the very first step: the computation of the tree decomposition. The next two steps were algorithmically \"trivial\" in the sense that nothing happens during a run of the algorithm--the transformations are done beforehand and the results get \"hardwired\" into the algorithm. Running the tree automaton on a tree is much easier than computing the tree composition, so the last step usually contributes little to the complexity of the algorithms. However, what happens if we make life easier for our algorithms (which seems only fair, considering that we also made life easier for our student) by _providing a tree decomposition of the graph as part of the input?_ This takes the first step out of the picture and we get an algorithmic metatheorem where the algorithmic complexity hinges (only) on the complexity of evaluating a tree automaton on an input tree, and it was mentioned earlier that [PERSON] showed [15] in 1987 that this can be done using an NC\({}^{1}\)-circuit, yielding the following theorem:  
**Theorem 9** ([PERSON], [PERSON], [PERSON], 2012, [21]). : _Let \(\phi\) be a formula in monadic second-order logic and let \(k\geq 1\) be a number. Then, the language \(\{(\mathcal{G},T,B)\mid\mathcal{G}\models\phi\text{ and }(T,B)\text{ is a tree decomposition of }\mathcal{G}\text{ of width }k\}\) can be decided by an NC\({}^{1}\)-circuit family._As for logarithmic space, let me give readers less familiar with the class NC\({}^{1}\) a one paragraph review: it is a language class containing problems that can be decided by very shallow circuits, namely circuits of depth \(O(\log n)\) for inputs of length \(n\). In the circuits, the usual logical gates (and, or, negation) may be used and these gates must have _bounded fan-in_, meaning that the and-gates and or-gates may only take two inputs at a time. These kinds of circuits are a good model of _fast parallel computations_ since the gates of a circuit obviously all work in parallel, and, because of the small depth of the circuit, we only have to wait for at most \(O(\log n)\) units of time for a decision when we feed an input into the circuit. The problem of evaluating a propositional formula for a given assignment of values to the variables (known as the Boolean formula evaluation problem, BF in short) can be shown to be complete for the class NC\({}^{1}\). Other problems included in this class are addition, multiplication, and even division. The class NC\({}^{1}\) is a subclass of L and, if it is a proper subclass (as many people believe), problems complete for L like the even or odd cycle problems from the previous section are no elements of NC\({}^{1}\). The new requirement we added to Theorem 4.1, namely that the input graph should be accompanied by a tree decomposition, seems to ruin the whole purpose of the theorem: if the difficult part of proving [PERSON]'s Theorem is determining the tree decomposition, then what use could a theorem have that blithely assumes that the tree decomposition is part of the input? It turns out that there are two situations where we _do_ have tree decompositions \"handy\". First, even though I claimed in the introduction that considering trees as input is boring and problems only get interesting when the graphs have larger tree width, there _are_ problems on trees that are of interest, and the nice thing about trees is that they are already \"their own tree decompositions\". Thus, when our input graphs are trees, we can apply the theorem.