# A Gentle Introduction to Applications of Algorithmic Metatheorems for Space and Circuit Classes
## 2 The Concepts and Ideas Behind Courcelle's Theorem
### The Proof Ideas for Courcelle's Theorem  
With all the ingredients prepared, we can now have a closer look at Courcelle's Theorem, which has already been mentioned repeatedly. It states:  
**Courcelle's Theorem**.: _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 linear time._  
**Proof Ideas**.: Suppose (a string encoding of) a graph \(\mathcal{G}=(V,E^{\mathcal{G}})\) is given as an input. The first step is to determine a tree decomposition, that is, to find a strategy for the \(k+1\) detectives. One can find such a strategy in time \(n^{O(k)}\) by iteratively \"cutting off\" escapes routes for [PERSON], but finding such a strategy in _linear_ time is not so easy. Indeed, the theorem stating that this is, indeed, possible has a dedicated name: it is Bodlaender's Theorem [13]. In the following, we will see further examples where the \"really difficult part\" of an algorithmic metatheorem is finding the tree decomposition.  
Suppose we have determined a width-\(k\) tree decomposition \((T,B)\) of \(\mathcal{G}\). We face the problem that \(\phi\) refers to \(\mathcal{G}\), but our recursion should use \(T\) instead. One can proceed in different ways at this point, but one elegant way of solving the problem is to _modify_\(\phi\) so that it refers to \(T\) instead of \(\mathcal{G}\): Very roughly speaking, when \(\phi\) refers to a variable \(x\) standing for a vertex \(v\) of \(\mathcal{G}\), we instead use a second-order variable \(X\) that stands for the subset of \(T\)'s nodes whose bags contain \(v\); and when \(\phi\) uses the atomic formula \"\(E(x,y)\)\" to test whether there is an edge between \(x\) and \(y\) in \(\mathcal{G}\), we instead test whether there is a node \(n\) contained in both \(X\) and \(Y\) that contains the edge. The modification yields a new monadic second-order formula \(\phi^{\prime}\) with the property \(\mathcal{G}\models\phi\iff\mathcal{T}\models\phi^{\prime}\) where \(\mathcal{T}\) is (a logical structure encoding) \(T\) together with additional labels representing information about the bag structure. As an example, for the concrete case of \(\phi\) expressing that \(G\) is 3-colorable, \(\phi^{\prime}\) expresses something like \"there exists a way of assigning the three colors to the \(k+1\) vertices of each bag \(B(n)\) such that the assignment is consistent across all bags containing the same original vertex and nodes whose bags contain the two endpoints \(u\) and \(v\) of an edge of \(G\) must assign different colors to \(u\) and \(v^{\prime\prime}\).  
The last step is to determine in linear time whether \(\mathcal{T}\models\phi^{\prime}\) holds. We use a _tree automaton_ for this: this is a finite automaton that starts its work at the leafs of a tree in some initial state and whose state at a given node depends on the states reached at the node's children and on the label of the node. Whether the automaton accepts or rejects an input tree depends on the state reached at theroot. The automaton for deciding \(\mathcal{T}\models\phi^{\prime}\) can be constructed by induction on the structure of \(\phi^{\prime}\): atomic formulas just test whether nodes have certain labels; the logical conjunction corresponds to taking the product automaton; the negation corresponds to taking the complement automaton; and a monadic existential quantification corresponds to _guessing_ a labeling using nondeterminism.  
Note that both the transformation of \(\phi\) into a formula \(\phi^{\prime}\) and also that of \(\phi^{\prime}\) into a tree automaton can be done \"in advance\": they do not depend on the input, only on \(\phi\) and \(k\). During an actual run of the algorithm, we \"just\" need to compute a tree decomposition and then run a tree automaton on it.