# A Gentle Introduction to Applications of Algorithmic Metatheorems for Space and Circuit Classes
## 3 An Algorithmic Metatheorem for Logspace and Its Applications  
When one is only interested in the deterministic, sequential time complexity of problems, one cannot really improve on [PERSON]'s Theorem: in _sub_linear time, we cannot even _read_ the whole input, let alone do computations depending on all parts of it. However, we may also ask how quickly a problem can be solved _in parallel_ or how much _space_ is needed or even how much _energy_ is necessary--or inquire about any number of further resources. Concerning parallel time, by rephrasing the lengthy Theorem 4.4 of [PERSON] quoted earlier using the ideas of the previous section (namely, to replace the endless list of problems by the phrase \"problems describable in monadic second-order logic\") and having another look at the proof of the theorem, one can show that [PERSON]'s Theorem also holds when we replace \"linear time\" by \"polylogarithmic parallel time.\" In other words, there is a \"parallel time version\" of [PERSON]'s Theorem. Naturally (at least, readers familiar with classical computational complexity theory will find this natural), when a problem can be solved quickly in parallel, it can also typically be solved with very little space. This leads to the question of whether we can modify the arguments used by [PERSON] to establish a \"logspace version\" of [PERSON]'s Theorem. The answer is \"yes\", but finding the proof took until 2010:  
**Theorem 1** ([PERSON], [PERSON], 2010, [5]). : _Let \(\phi\) be a formula in monadic second-order logic and let \(k\geq 1\) be a number. Then, the language \(\{\mathcal{G}\mid\mathcal{G}\models\phi\text{ and }\mathcal{G}\text{ has tree width at most }k\}\) can be decided in logarithmic space._  
Before we have a look at the proof ideas in a moment, let me just give you a one-paragraph refresher of logarithmic space: In this machine model, the input is \"read only\" (like a \"cd-rom\", although our first-year student probably has never heard of them) and the amount of read-write memory available is \(O(\log n)\) when the input has length \(n\). This extremely small amount of memory can equivalently be thought of as a constant number of \"pointers\" or \"one-symbol windows\" into the input. Despite being a very restricted model, one can do addition, multiplication, and even division in logarithmic space, evaluate Boolean formulas, solve the reachability problem on undirected graphs, and even test whether a graph is planar. Problems that cannot be solved in logarithmic space--unless, of course, certain complexity class collapses occur--include the reachability problem for directed graphs, evaluating Boolean circuits (instead of formulas), or the 2-sat problem (the satisfiability problem for propositional formulas in conjuctive normal form where all clauses have at most two literals). All problems that can be solved in logarithmic space can be solved in logarithmic parallel time (for appropriate models of parallel time) and also in polynomial (but not necessarily in linear) sequential time. **Proof Ideas. ** Recall that the proof of [PERSON]'s Theorem from the previous section 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 \(A\) on \(T\). Clearly, the second and third step work exactly the same way in the logspace setting as in the linear time setting (or, for that matter, in any other setting) since these transformations are independent of the input and can be done in advance. The fourth step, running the tree automaton, is essentially just an elaborate version of evaluating a Boolean formula tree (only, instead of passing the two possible results \"true\" or \"false\" towards the root, we pass states) and it is well-known that this can be done in logarithmic space; indeed, it can be done in NC1, a subclass of logarithmic space, as was shown by [PERSON] [15] already in 1987.