# A Gentle Introduction to Applications of Algorithmic Metatheorems for Space and Circuit Classes
## 3 An Algorithmic Metatheorem for Logspace and Its Applications
### Applications: Low-Hanging Fruits  
The logspace version of Courcelle's Theorem has two kinds of applications, which I like to call the \"low-hanging fruits\" and the \"high-hanging fruits\". The low-hanging ones are results that we get more or less \"for free\" by taking any problem to which the classical version of Courcelle's Theorem is known to apply and then rephrasing the result in this new setting. As an example, here is a typical lemma you can find in a textbook:  
**Lemma 2**.: _For each \(k\), the set \(\{G\mid G\) has tree width at most \(k\) and \(G\) is \(3\)-colorable\(\}\) can be decided in linear time._  
Proof.: The property \"\(G\) is \(3\)-colorable\" can be described by a monadic second-order formula. By Courcelle's Theorem, we get the claim.  
Such lemmas transfer very easily to the logspace setting:  
**Lemma 3**.: _For each \(k\), the set \(\{G\mid G\) has tree width at most \(k\) and \(G\) is \(3\)-colorable\(\}\) can be decided in logarithmic space._  
Proof.: The property \"\(G\) is \(3\)-colorable\" can _still_ be described by a monadic second-order formula. By the logspace version of [PERSON]'s Theorem, we get the claim.  
The transfer works very well for \(3\)-colorability and many other problems, but what about the introductory problem of this paper, the vertex cover problem? You may have noticed that I did not present a monadic second-order formula describing this problem (yet). At first sight, such a formula is easy to obtain: \(\exists C\forall x\forall y\big{(}E(x,y)\to(C(x)\lor C(y))\big{)}\) reads aloud \"there is a vertex cover \(C\) such that for all edges \((x,y)\in E^{\mathcal{G}}\) one of the two endpoints lies in \(C\)\". However, this is not really what we want: we do not wish to know whether a vertex cover _exists_ (of course it does, just take all vertices), but would like to know whether a vertex cover of a _certain size_ exists. This means that \(C\) must be a _free_ monadic second-order variable (we remove the quantifier at the beginning of the formula) and we would like to know whether we can choose an assignment to this free variable that, firstly, makes the formula true and, secondly, has a certain size \(s\) that is part of the input. Fortunately, it turns out that both [PERSON]'s Theorem and its logspace version can be modified so that they also apply to this situation. Let me state the logspace version explicitly:  
**Theorem 4** ([PERSON], [PERSON], [PERSON], 2010, [5]).: _Let \(\phi(X)\) be a formula in monadic second-order logic with a free monadic second-order variable \(X\) and let \(k\geq 1\) be a number. Then, the language \(\{(\mathcal{G},s)\mid\mathcal{G}\models\phi(C)\) for some \(C\subseteq V\) with \(|C|=s\), and \(\mathcal{G}\) has tree width at most \(k\}\) can be decided in logarithmic space._  
Using this more general version, the list of problems that are \"low-hanging fruits\" becomes rather long: it includes all of the problems in the long list quoted earlier from [PERSON]'s paper; indeed, it is difficult to find a problem that can _not_ be described in monadic second-order logic. The graph isomorphism problem is one such exception--and, fittingly, the complexity of deciding whether two graphs of bounded tree width are isomorphic was settled only in 2016, see [17].