# A Gentle Introduction to Applications of Algorithmic Metatheorems for Space and Circuit Classes
## 5 An Algorithmic Metatheorem for Constant-Depth Circuits and Its Applications
### Bounded Tree Depth  
Theorem 12 is not the \"final word\" on the complexity of the unary subset sum problem. First, observe that it is trivial to compute tree decompositions for the graphs that we construct in the theorem. This means that the hard part of [PERSON]'s Theorem--the computation of the tree decompositions--does not need to be performed and Theorem 9 applies (or, rather, an NC\({}^{1}\)-analogue of Theorem 4), yielding unary-subset-sum\(\in\)NC\({}^{1}\). Second, the graphs constructed in the proof of Theorem 12 (the collections of stars) have a special property: not only do two detectives suffice to corner [PERSON] on a star, no matter how large the star, the two detectives can always corner him in _two steps_. In other words, we do not only have a strategy for catching [PERSON] with a bounded number of detectives, but also in a bounded number of steps. Graphs with this property are said to have bounded tree _depth:_  
**Definition 14**. : A class \(C\) of graphs has _bounded tree depth_ if there is a constant \(d\) such that all graphs \(G\in C\) have a tree decomposition of width at most \(d\) and depth at most \(d\). Examples of graphs of bounded tree depth include, of course, all trees of constant depth, while long paths do not have bounded tree depth (any fixed number of detectives need \(\Omega(\log n)\) steps to catch [PERSON] on a path of length \(n\)). In particular, if we replace the stars constructed in the previous theorem by paths, each of length \(a_{i}\), the resulting graphs could still be used with the algorithmic metatheorems from the previous two sections (they have bounded tree width, namely 1), but would not have bounded tree depth any longer. The obvious question at this point is: Why is the depth of a tree decompositions important? Let us recall (for the last time) the four steps involved in proving Courcelle's Theorem:  
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\). As in the previous sections, the second and third points do not contribute to the runtime and let us ignore the first point for a moment. What is left is running a tree automaton on a tree _of constant depth_. Intuitively, this can be done in a highly parallel manner and takes very little time: in the first step, we compute in parallel the automaton's states at the leafs; in the second step, we consider the nodes having only leaves as children and compute, once more in parallel, the states the automaton reaches there; in the third step, we consider the nodes a level higher up; and so on. After a _constant_ number of steps, we will have reached the root and know whether the automaton accepts the input tree. Regarding the first step, the computation of the tree decomposition of constant depth, it turns out that a strategy for cornering [PERSON] in a constant number of steps can itself be found in a constant number of parallel steps: as in the proof for the logspace version of Courcelle's Theorem, we consider all possible ways that the detectives can be positioned and draw an edge from one bag to another when the second bag \"corners [PERSON] better\" than the first one. In the logspace setting, the difficult part was extracting a tree decomposition from this graph since a logspace machine cannot \"remember its choices\" along paths in this graph; but, in our setting, all paths have _constant length_ and, thus, extracting the tree decomposition from the graph is not particularly difficult. To sum up, we get an algorithmic metatheorem stating that all monadic second-order logic properties of graphs of bounded tree depth can be solved in _constant parallel time:_  
**Theorem 15** ([PERSON], [PERSON], 2012, [21]). : _Let \(d\geq 1\) be a number._  
1. _Let_ \(\phi\) _be a formula in monadic second-order logic.