Rabin's Tree Theorem - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-22T18:23:49Z http://mathoverflow.net/feeds/question/97158 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/97158/rabins-tree-theorem Rabin's Tree Theorem Daniel Osterman 2012-05-16T21:06:08Z 2012-05-17T11:54:45Z <p>I've been reading Rabin's article on decidability in Barwise's text, and I came across Rabin's discussion of the decidability proof of his tree theory: the second-order theory with two successor functions. The text mentions that the proof is hard and very technical owing to many extensions of automata theory, and I was wondering if someone might be able to sketch it out.</p> <p>Thanks!</p> http://mathoverflow.net/questions/97158/rabins-tree-theorem/97169#97169 Answer by D K for Rabin's Tree Theorem D K 2012-05-16T23:59:55Z 2012-05-17T00:16:50Z <p>Here is a very sketchy answer, but it should give the first idea of the proof.</p> <p>Basically, even on words (structures with one successor), you can decide if an MSO (Monadic Second Order) sentence accepts a model by translating the sentence to an equivalent automaton, and then you just need to find an accepting path in this automaton, which is easy.</p> <p>What Rabin did is develop a model of automaton running on infinite tree, together with a way to translate MSO sentences to equivalent automata. Then, in the same way, deciding if the MSO sentence accepts a model is reduced to finding a "path" (which is generalized to a tree structure in some way) in the equivalent automaton.</p> http://mathoverflow.net/questions/97158/rabins-tree-theorem/97198#97198 Answer by Andres Caicedo for Rabin's Tree Theorem Andres Caicedo 2012-05-17T07:46:31Z 2012-05-17T07:46:31Z <p>This is a nice result, but you are right that the known proofs are rather elaborate. Below, I just give the briefest of sketches, but it gives a glimpse of the ideas involved. The game theoretic approach is elegant, even if it takes a bit of time to understand the relevant notions. </p> <p>An excellent reference is the book "The classical decision problem", by Börger, Grädel, and Gurevich (Springer, 1997). You can find the proof in II.7.1. </p> <p>I lectured on it in Caltech a few centuries ago (2007). If you do not have access to the book, you may want to take a look at homework sets 5 and 6 at this <a href="http://caicedoteaching.wordpress.com/previous-courses/computability-theory-decidability-caltech-spring-2007/" rel="nofollow">link</a>. There, you will find a sketch of the so called Forgetful Determinacy theorem of Gurevich and Harrington. This is the key technical result. Here, I'll just state it.</p> <p>(The theorem comes from Gurevich-Harrington, "Trees, automatas, and games". 14th annual ACM Symposium on Theory of Computation, 60-65, 1982. The presentation in the book follows Zeitman, "Unforgettable forgetful determinacy", Journal of Logic and Computation, vol 4, 273-283 (1994).)</p> <blockquote> <p><strong>Theorem (Forgetful determinacy for tree automata).</strong> If $A$ is a $\Sigma$-tree automaton and $F$ is a $\Sigma$-tree, one of the players ($A$ or Pathfinder) has a winning strategy in $\Gamma(A,F)$ that is <em>forgetful</em> in the sense that whenever $p$, $q$ are positions from which the winner moves, $$LAR(p)=LAR(q),$$ and $$\mbox{Node(p)-residue of F=Node(q)-residue of F},$$ then $f(p)=f(q)$.</p> </blockquote> <p>(Here, the node of a position is simply the node in the binary tree that is being played. Given a $\Sigma$-tree $F$, the $v$-residue of $F$ is the $\Sigma$-tree $F_v$ coming from $F$ by only considering the tree from $v$ on, that is, $F_v(w)=F(vw)$. I define the other relevant notions below.)</p> <p>Using this, it is relatively easy to check that the "Emptiness problem" is decidable for tree automata: There is an algorithm that, given a $\Sigma$-automaton $A$, decides whether there is a $\Sigma$-tree that $A$ accepts. </p> <p>Similarly, but this takes a bit of work and is really the whole point, Forgetful Determinacy implies that there is an algorithm that to each $\Sigma$-automaton $A$ assigns a $\Sigma$-automaton $C$ with the property that $C$ accepts a $\Sigma$-tree iff $A$ rejects it. (This is the "Complementation Theorem".)</p> <p>Using this, it is a simple matter of induction in formulas to prove decidability, since one can effectively associate to each monadic formula $\phi(X_1,\dots,X_n)$ (of second-order theory with two successors) a $\Sigma$-automaton $A$ for <code>$\Sigma=\{0,1\}^n$</code>, with the property that, for any collections $W_1,\dots,W_n$ of binary words, the automaton $A$ accepts the tree $T$ they define iff $T^2$ satisfies $\phi(W_1,\dots,W_n)$, where $T^2$ is the structure given by the full binary tree with the two successor functions. </p> <hr> <p>Let me briefly review the relevant definitions, following the book closely. I'm just quoting the notes of my younger self, so there may be a bit of irrelevancy, for which I apologize. </p> <p>Let $MOVE$ be a finite alphabet. An <em>arena</em> $A$ is a colored bipartite multi-digraph in the following sense:</p> <ol> <li><p>The <em>vertices</em> of $A$ are divided into two disjoint sets, <em>east</em> vertices and <em>west</em> vertices. There are no <em>edges</em> between east vertices or between west vertices. There may be <em>several</em> edges between an east and a west vertices, or between a west and an east vertices (so edges have <em>directions</em>, which is why we call the object a digraph, and there may be several edges between the same vertices, which is why we call it a multi-digraph).</p></li> <li><p>There is a distinguished vertex, the <em>start vertex</em>. Every vertex is <em>reachable</em> from the start vertex (i.e., for any $v$ there is a finite sequence $v_0,\dots,v_n$ where $v_0$ is the start vertex, $v_n=v$ and for each $i\lt n$ there is an edge going from $v_i$ to $v_{i+1}$). Any vertex has at least one outgoing edge.</p></li> <li><p>The edges are labeled by elements of $MOVE$ in such a way that no two <em>outgoing</em> edges from the same vertex have the same label.</p></li> <li><p>There is a finite set $S$ of <em>colors</em> that partition the set of vertices. We denote by $C^s$ the vertices with color $s$.</p></li> </ol> <p>A <strong>game</strong> on $A$ is played between two players 0 and 1 who alternate choosing an outgoing edge from the current vertex, starting from the start vertex. So a play of the game defines an infinite <em>path</em> through $A$ (we allow for the possibility of revisiting vertices). A <em>position</em> $p$ is a finite directed path through $A$ from the start vertex, so it is uniquely described by a word in $MOVE^*$, with which we identify $p$. Given a position $p$, the labels of the edges leading out of the last vertex of $p$ are the <em>possible moves</em> at $p$. A <em>play</em> is an $\omega$-sequence $P\in MOVE^\omega$ such that each initial segment is a position. The set of plays over $A$ is $PLAY(A)$.</p> <p>A <strong>graph game</strong> is a triple $\Gamma=(A,\varepsilon,W_\varepsilon)$ where $A$ is an arena, $\varepsilon\in{0,1}$ (denoting the player that goes first) and $W_\varepsilon$, the <em>winning set</em> for player $\varepsilon$, is a Boolean combination of the sets ${}[C^s]$ where ${}[C^s]$ is the set of plays that infinitely often pass through a vertex of color $s$.</p> <p>Player $\varepsilon$ wins a play $P$ of $\Gamma$ iff $P\in W_\varepsilon$. Otherwise, player $1-\varepsilon$ wins the play $P$.</p> <p>Notice that if the start vertex is an east (resp., a west) vertex then, playing $\Gamma$, player $\varepsilon$'s turns to move are always at east (resp., west) vertices. Call the set of these vertices $V_{\varepsilon}$ and the set of remaining vertices $V_{1-\varepsilon}$.</p> <p>A <strong>forgetful strategy</strong> $f$ for player <code>$\delta\in\{0,1\}$</code> in $\Gamma$ is a function $f:V_\delta\to{\mathcal P}(MOVE)$ that to each $v\in V_\delta$ assigns a non-empty set of possible moves from $v$. (The strategy is forgetful since it depends only on $v$ and not on how $v$ was reached.)</p> <p>The <em>latest appearance record</em> $LAR(p)$ of a position $p$ is an ordering of the colors. We define $LAR$ inductively, with $LAR(start)$ being an ordering whose last color is that of the start vertex. If a position $q$ is obtained from a position $p$ by adjoining an edge to a vertex of color $s$, then $LAR(q)$ is obtained from $LAR(p)$ by moving $s$ to the last place. The coloring of an arena $A$ is <em>forgetful</em> if any two positions at the same vertex have the same $LAR$, in which case we can simply talk of the $LAR$ at a vertex $v$ (rather than at a position $p$ whose last vertex is $v$).</p> <p>What one actually shows is the following:</p> <blockquote> <p><strong>Theorem (Forgetful determinacy).</strong> Let $\Gamma=(A,\varepsilon,W_\varepsilon)$ be a graph game with a forgetful coloring of the arena $A$. Then one of the players has a forgetful winning strategy in $\Gamma$.</p> </blockquote> <p>One then uses this result to prove the version I stated earlier. For this, let $\Gamma(A,F)$ be a game on a $\Sigma$-tree $F$ between a $\Sigma$-tree automaton $A$ and Pathfinder. Define from this a graph game whose alphabet consists of the states of $A$ and names for the two directions left and right. (So $A$ starts the game and chooses a state according to its initial table, Pathfinder responds by choosing the name of a direction, then $A$ chooses a state, etc.)</p> <p>All positions $p$ where $A$ makes a move have the same default color. If $A$ chooses a state $s$ at $p$ then the color of position $ps$ is $s$. (One needs to check that this coloring is forgetful.)</p> <p>One then has that either $A$ or Pathfinder has a forgetful winning strategy in $\Gamma(A,F)$, by "transfering" the strategy that the forgetful determinacy theorem guarantees.</p>